EXPLAINING GABRIEL ZISMAN LOCALIZATION TO THE COMPUTER

Description

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

Sujets

• Barwick
• Street
• Localization
• Category

Informations

• Publié par: pefav
• Nombre de lectures: 9
• Langue: English

Extrait

EXPLAININGGABRIEL-ZISMANLOCALIZATIONTOTHE COMPUTER CARLOSSIMPSON Contents 1.Introduction 2.Thegenerallocalizationconstruction 3.Thecomputerformulation 3.1.Categorytheory 3.2.Thefreecategory 3.3.Quotientcategories 3.4.Constructionofthelocalization 4.Calculusofleft(orright)fractions 5.Formalizingtheleft-fractionconstruction 6.Furtherformalizations References 1 5 7 7 8 01 11 31 91 22 32 1.Introduction Weformalizethelocalizationofcategories,asinthebookofGabrielandZisman[9], withtheCoqcomputerproofassistant.Thepurposeofthispreprintistoprovidesome discussionofthiswork.Ontheotherhand,thecomputerfilesthemselvesareattachedto thecompanionpreprint“FilesforGabriel-Zismanlocalization”.Thetextofthatpreprint consistsmainlyofthedefinitionsandstatementsofresultsfromthecomputerfiles(inother wordsitisequaltothefileswiththeproofsremoved),plussomeinstructionsforcompiling thefiles. Thereareseveralreasonsforchoosingthisproject.Acertainamountofbasiccategory theorywasdoneinthefilesattachedtomypreviouspaperonthissubject[30].Thusit isnaturaltolookforsomefurthertopicstodoincategorytheory.Along-rangegoalisto beabletodothetheoryandpracticeofclosedmodelcategories.AglanceatQuillen[23] suggeststhatthenotionoflocalizationofcategoriesa`laGabriel-Zismanisanimportant componentofthestatementsofsomeofQuillen’smainresults.Alsoinphilosophicalterms itisclearthatQuillenwasinfluencedbyGabrielandZisman,soitisreasonabletothink thatdoingacomputerformalizationoftheirconstructionoflocalizationwouldbeagood warm-upexercise. Keywordsandphrases.Category,Functor,Localization,Calculusoffractions,Proofassistant,Computer proofverification. 1

2C.SIMPSON Alittlebitofinvestigationintothebibliographicalreferencesforthisconstructionhas alsoturnedupanotherinterestingreasontoformalizeitonthecomputer.Itturnsoutthat thefulldetailsoftheconstruction(andspeciallyofthecalculusoffractionsconstruction) haveneverreallyappearedinprint.Oratleast,asearchforthesedetailshasnotturnedup anyreference.Ofcourseitwouldn’tbesurprisingtofindacompletereferencesomewhere— youmightsaythatthiswouldbetheexpectednormalcy.Nonethelessitseemsprettyclear thatthevastmajorityoftheverynumerousmathematicianswhousethistheoryeveryday haven’tinfactreadatextwiththefulldetailswrittendown. Thenotionoflocalizationofacategoryisfoundationalforsomeofthemostpopulartools usedbymathematicianstoday:thehomotopycategory(ofspaces,simplicialsets,orother things),andthederivedcategory(ofanabeliancategory,cominginvariousflavors).It issurprisingthatthetheoryissohardtofindwrittendowninitsintegrality.Thismight contributeaspartofanexplanationforwhythetheoriesofhomotopycategoriesandderived categoriesaresomuchusedandconsideredas“blackboxes”. Onepossiblepointofviewwouldbetosaythatfewhavebotheredtotrytopublishthe fulldetailsoftheconstruction,becauseinacertainsensethatjustwouldn’tbeworthit: writingsomethingdownpresupposesthattherewouldbesomebodyinterestedinreading it;andwritingdownthefulldetailsofanargumentwhichisinessencestraightforward, presupposesthatahumanreaderwoulddesireto,andbecapableof,verifyinginameaningful waythatthewrittentextreallydidcontainallofthedetails.Factorssuchasthetotalcost ofpublicationalsopushtowardsleavingoutmuchofthistypeofargument. Intryingtowriteupthepresentnoteexplainingthecomputerproof,itbecameevident thatonehadtoagreewiththeotherpublishedtextsonthis:thefulldetailsoftheargument justaren’tsufficientlyinterestingtojustifytheratherextensivelinguisticeffortwhichwould berequiredtoaccuratelyconveythemtoahumanreader,norinterestingenoughforthe readertobotherreadingsuchanexplanation.Andthisiswithafundamentalpieceof categorytheorymorethan40yearsold.Thearrivalofthepossibilitythatthe“reader” mightbeacomputerchangesthiscalculation.Thecomputerisaperfectlistenerforan explanationthatcanbegivenasasortofflowoflittlearguments,sometimeswithanecessary globalstrategybehindthem,butalwayswithlotsofthingstoremember,lotsofreferential notationstorefertovariousobjects,andsoforth. Thepurposeofthepresentpreprintistodiscussourcomputerformulation,bothofthe generallocalizationconstructionandthespecialconstructionwhenthereisacalculusof fractions.Wedon’tpretendtogiveallthedetailsinthetext—indeedwestopataboutthe sameplaceaspreviousauthorshave.However,thedetailsarenecessarilyallthereinthe computerfiles[31]. Historically,thenotionoflocalizationappearedinformallyinasomewhatdifferentform intheToˆhokupaperofGrothendieck[11]whereheformalizes(tosomeextent)language whichheattributestoSerre[27]ofworkinginacategory“modulo”asubcategory. AfterGabriel-Zisman,thequestionoflocalizationofcategorieshasbeentreatedina numberofreferences.Severalpeoplewerehelpfulinpointingoutsomeoftheseinresponse torequestspostedtothetopologyandcategory-theorymailinglists.Thereferencesinclude booksbyL.andN.Popescu[19][20],H.Schubert[25],andF.Borceux[3].Curiouslyenough