EXPLAINING GABRIEL ZISMAN LOCALIZATION TO THE COMPUTER
24 pages
English

EXPLAINING GABRIEL ZISMAN LOCALIZATION TO THE COMPUTER

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

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

Informations

Publié par
Nombre de lectures 9
Langue English

Exrait

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,thecomputerfilesthemselvesareattachedtothecompanionpreprint“FilesforGabriel-Zismanlocalization”.Thetextofthatpreprintconsistsmainlyofthedefinitionsandstatementsofresultsfromthecomputerfiles(inotherwordsitisequaltothefileswiththeproofsremoved),plussomeinstructionsforcompilingthefiles.Thereareseveralreasonsforchoosingthisproject.Acertainamountofbasiccategorytheorywasdoneinthefilesattachedtomypreviouspaperonthissubject[30].Thusitisnaturaltolookforsomefurthertopicstodoincategorytheory.Along-rangegoalistobeabletodothetheoryandpracticeofclosedmodelcategories.AglanceatQuillen[23]suggeststhatthenotionoflocalizationofcategoriesa`laGabriel-ZismanisanimportantcomponentofthestatementsofsomeofQuillen’smainresults.AlsoinphilosophicaltermsitisclearthatQuillenwasinfluencedbyGabrielandZisman,soitisreasonabletothinkthatdoingacomputerformalizationoftheirconstructionoflocalizationwouldbeagoodwarm-upexercise.Keywordsandphrases.Category,Functor,Localization,Calculusoffractions,Proofassistant,Computerproofverification.1
2C.SIMPSONAlittlebitofinvestigationintothebibliographicalreferencesforthisconstructionhasalsoturnedupanotherinterestingreasontoformalizeitonthecomputer.Itturnsoutthatthefulldetailsoftheconstruction(andspeciallyofthecalculusoffractionsconstruction)haveneverreallyappearedinprint.Oratleast,asearchforthesedetailshasnotturnedupanyreference.Ofcourseitwouldn’tbesurprisingtofindacompletereferencesomewhere—youmightsaythatthiswouldbetheexpectednormalcy.Nonethelessitseemsprettyclearthatthevastmajorityoftheverynumerousmathematicianswhousethistheoryeverydayhaven’tinfactreadatextwiththefulldetailswrittendown.Thenotionoflocalizationofacategoryisfoundationalforsomeofthemostpopulartoolsusedbymathematicianstoday:thehomotopycategory(ofspaces,simplicialsets,orotherthings),andthederivedcategory(ofanabeliancategory,cominginvariousflavors).Itissurprisingthatthetheoryissohardtofindwrittendowninitsintegrality.Thismightcontributeaspartofanexplanationforwhythetheoriesofhomotopycategoriesandderivedcategoriesaresomuchusedandconsideredas“blackboxes”.Onepossiblepointofviewwouldbetosaythatfewhavebotheredtotrytopublishthefulldetailsoftheconstruction,becauseinacertainsensethatjustwouldn’tbeworthit:writingsomethingdownpresupposesthattherewouldbesomebodyinterestedinreadingit;andwritingdownthefulldetailsofanargumentwhichisinessencestraightforward,presupposesthatahumanreaderwoulddesireto,andbecapableof,verifyinginameaningfulwaythatthewrittentextreallydidcontainallofthedetails.Factorssuchasthetotalcostofpublicationalsopushtowardsleavingoutmuchofthistypeofargument.Intryingtowriteupthepresentnoteexplainingthecomputerproof,itbecameevidentthatonehadtoagreewiththeotherpublishedtextsonthis:thefulldetailsoftheargumentjustaren’tsufficientlyinterestingtojustifytheratherextensivelinguisticeffortwhichwouldberequiredtoaccuratelyconveythemtoahumanreader,norinterestingenoughforthereadertobotherreadingsuchanexplanation.Andthisiswithafundamentalpieceofcategorytheorymorethan40yearsold.Thearrivalofthepossibilitythatthe“reader”mightbeacomputerchangesthiscalculation.Thecomputerisaperfectlistenerforanexplanationthatcanbegivenasasortofflowoflittlearguments,sometimeswithanecessaryglobalstrategybehindthem,butalwayswithlotsofthingstoremember,lotsofreferentialnotationstorefertovariousobjects,andsoforth.Thepurposeofthepresentpreprintistodiscussourcomputerformulation,bothofthegenerallocalizationconstructionandthespecialconstructionwhenthereisacalculusoffractions.Wedon’tpretendtogiveallthedetailsinthetext—indeedwestopataboutthesameplaceaspreviousauthorshave.However,thedetailsarenecessarilyallthereinthecomputerfiles[31].Historically,thenotionoflocalizationappearedinformallyinasomewhatdifferentformintheToˆ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
  • Accueil Accueil
  • Univers Univers
  • Ebooks Ebooks
  • Livres audio Livres audio
  • Presse Presse
  • BD BD
  • Documents Documents