EXPLAINING GABRIEL ZISMAN LOCALIZATION TO THE COMPUTER

pages

English

Documents

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

pages

English

Ebook

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Publié par

pefav

Nombre de lectures

Langue

English

ar X iv :m at h. CT /0 50 64 71 v 1 2 3 Ju n 20 05 EXPLAINING GABRIEL-ZISMAN LOCALIZATION TO THE COMPUTER CARLOS SIMPSON Contents 1. Introduction 1 2. The general localization construction 5 3. The computer formulation 7 3.1. Category theory 7 3.2. The free category 8 3.3. Quotient categories 10 3.4. Construction of the localization 11 4. Calculus of left (or right) fractions 13 5. Formalizing the left-fraction construction 19 6. Further formalizations 22 References 23 1. Introduction We formalize the localization of categories, as in the book of Gabriel and Zisman [9], with the Coq computer proof assistant. The purpose of this preprint is to provide some discussion of this work. On the other hand, the computer files themselves are attached to the companion preprint “Files for Gabriel-Zisman localization”. The text of that preprint consists mainly of the definitions and statements of results from the computer files (in other words it is equal to the files with the proofs removed), plus some instructions for compiling the files. There are several reasons for choosing this project. A certain amount of basic category theory was done in the files attached to my previous paper on this subject [30]. Thus it is natural to look for some further topics to do in category theory.

left-fraction construction

details has

up another

localization

written up

category

localization appeared

Voir

Publié par

pefav

Nombre de lectures

Langue

English

EXPLAININGGABRIEL-ZISMANLOCALIZATIONTOTHECOMPUTERCARLOSSIMPSONContents1.Introduction2.Thegenerallocalizationconstruction3.Thecomputerformulation3.1.Categorytheory3.2.Thefreecategory3.3.Quotientcategories3.4.Constructionofthelocalization4.Calculusofleft(orright)fractions5.Formalizingtheleft-fractionconstruction6.FurtherformalizationsReferences157780111319122321.IntroductionWeformalizethelocalizationofcategories,asinthebookofGabrielandZisman[9],withtheCoqcomputerproofassistant.Thepurposeofthispreprintistoprovidesomediscussionofthiswork.Ontheotherhand,thecomputerﬁlesthemselvesareattachedtothecompanionpreprint“FilesforGabriel-Zismanlocalization”.Thetextofthatpreprintconsistsmainlyofthedeﬁnitionsandstatementsofresultsfromthecomputerﬁles(inotherwordsitisequaltotheﬁleswiththeproofsremoved),plussomeinstructionsforcompilingtheﬁles.Thereareseveralreasonsforchoosingthisproject.Acertainamountofbasiccategorytheorywasdoneintheﬁlesattachedtomypreviouspaperonthissubject[30].Thusitisnaturaltolookforsomefurthertopicstodoincategorytheory.Along-rangegoalistobeabletodothetheoryandpracticeofclosedmodelcategories.AglanceatQuillen[23]suggeststhatthenotionoflocalizationofcategoriesa`laGabriel-ZismanisanimportantcomponentofthestatementsofsomeofQuillen’smainresults.AlsoinphilosophicaltermsitisclearthatQuillenwasinﬂuencedbyGabrielandZisman,soitisreasonabletothinkthatdoingacomputerformalizationoftheirconstructionoflocalizationwouldbeagoodwarm-upexercise.Keywordsandphrases.Category,Functor,Localization,Calculusoffractions,Proofassistant,Computerproofveriﬁcation.1

2C.SIMPSONAlittlebitofinvestigationintothebibliographicalreferencesforthisconstructionhasalsoturnedupanotherinterestingreasontoformalizeitonthecomputer.Itturnsoutthatthefulldetailsoftheconstruction(andspeciallyofthecalculusoffractionsconstruction)haveneverreallyappearedinprint.Oratleast,asearchforthesedetailshasnotturnedupanyreference.Ofcourseitwouldn’tbesurprisingtoﬁndacompletereferencesomewhere—youmightsaythatthiswouldbetheexpectednormalcy.Nonethelessitseemsprettyclearthatthevastmajorityoftheverynumerousmathematicianswhousethistheoryeverydayhaven’tinfactreadatextwiththefulldetailswrittendown.Thenotionoflocalizationofacategoryisfoundationalforsomeofthemostpopulartoolsusedbymathematicianstoday:thehomotopycategory(ofspaces,simplicialsets,orotherthings),andthederivedcategory(ofanabeliancategory,cominginvariousﬂavors).Itissurprisingthatthetheoryissohardtoﬁndwrittendowninitsintegrality.Thismightcontributeaspartofanexplanationforwhythetheoriesofhomotopycategoriesandderivedcategoriesaresomuchusedandconsideredas“blackboxes”.Onepossiblepointofviewwouldbetosaythatfewhavebotheredtotrytopublishthefulldetailsoftheconstruction,becauseinacertainsensethatjustwouldn’tbeworthit:writingsomethingdownpresupposesthattherewouldbesomebodyinterestedinreadingit;andwritingdownthefulldetailsofanargumentwhichisinessencestraightforward,presupposesthatahumanreaderwoulddesireto,andbecapableof,verifyinginameaningfulwaythatthewrittentextreallydidcontainallofthedetails.Factorssuchasthetotalcostofpublicationalsopushtowardsleavingoutmuchofthistypeofargument.Intryingtowriteupthepresentnoteexplainingthecomputerproof,itbecameevidentthatonehadtoagreewiththeotherpublishedtextsonthis:thefulldetailsoftheargumentjustaren’tsuﬃcientlyinterestingtojustifytheratherextensivelinguisticeﬀortwhichwouldberequiredtoaccuratelyconveythemtoahumanreader,norinterestingenoughforthereadertobotherreadingsuchanexplanation.Andthisiswithafundamentalpieceofcategorytheorymorethan40yearsold.Thearrivalofthepossibilitythatthe“reader”mightbeacomputerchangesthiscalculation.Thecomputerisaperfectlistenerforanexplanationthatcanbegivenasasortofﬂowoflittlearguments,sometimeswithanecessaryglobalstrategybehindthem,butalwayswithlotsofthingstoremember,lotsofreferentialnotationstorefertovariousobjects,andsoforth.Thepurposeofthepresentpreprintistodiscussourcomputerformulation,bothofthegenerallocalizationconstructionandthespecialconstructionwhenthereisacalculusoffractions.Wedon’tpretendtogiveallthedetailsinthetext—indeedwestopataboutthesameplaceaspreviousauthorshave.However,thedetailsarenecessarilyallthereinthecomputerﬁles[31].Historically,thenotionoflocalizationappearedinformallyinasomewhatdiﬀerentformintheToˆhokupaperofGrothendieck[11]whereheformalizes(tosomeextent)languagewhichheattributestoSerre[27]ofworkinginacategory“modulo”asubcategory.AfterGabriel-Zisman,thequestionoflocalizationofcategorieshasbeentreatedinanumberofreferences.Severalpeoplewerehelpfulinpointingoutsomeoftheseinresponsetorequestspostedtothetopologyandcategory-theorymailinglists.ThereferencesincludebooksbyL.andN.Popescu[19][20],H.Schubert[25],andF.Borceux[3].Curiouslyenough

Voir

Univers
Ebooks
Livres audio
Presse
Podcasts
BD
Documents

EXPLAINING GABRIEL ZISMAN LOCALIZATION TO THE COMPUTER

YouScribe

Le catalogue

Le service

Les conditions