Commit 2023-04-05 13:39 50dc55de

View on Github →

feat: port CategoryTheory.Sites.Sheaf (#3244)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Sites/Sheaf.lean

added def CategoryTheory.Presheaf.IsSheaf'

added def CategoryTheory.Presheaf.IsSheaf.amalgamate

added theorem CategoryTheory.Presheaf.IsSheaf.amalgamate_map

added theorem CategoryTheory.Presheaf.IsSheaf.hom_ext

added def CategoryTheory.Presheaf.IsSheaf

added def CategoryTheory.Presheaf.conesEquivSieveCompatibleFamily

added def CategoryTheory.Presheaf.firstMap

added def CategoryTheory.Presheaf.firstObj

added def CategoryTheory.Presheaf.forkMap

added def CategoryTheory.Presheaf.homEquivAmalgamation

added def CategoryTheory.Presheaf.isLimitOfIsSheaf

added theorem CategoryTheory.Presheaf.isLimit_iff_isSheafFor

added theorem CategoryTheory.Presheaf.isLimit_iff_isSheafFor_presieve

added theorem CategoryTheory.Presheaf.isSeparated_iff_subsingleton

added def CategoryTheory.Presheaf.isSheafForIsSheafFor'

added theorem CategoryTheory.Presheaf.isSheaf_iff_isLimit

added theorem CategoryTheory.Presheaf.isSheaf_iff_isLimit_pretopology

added theorem CategoryTheory.Presheaf.isSheaf_iff_isSheaf'

added theorem CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget

added theorem CategoryTheory.Presheaf.isSheaf_iff_multiequalizer

added theorem CategoryTheory.Presheaf.isSheaf_iff_multifork

added theorem CategoryTheory.Presheaf.isSheaf_of_isTerminal

added theorem CategoryTheory.Presheaf.isSheaf_of_iso_iff

added def CategoryTheory.Presheaf.secondMap

added def CategoryTheory.Presheaf.secondObj

added theorem CategoryTheory.Presheaf.subsingleton_iff_isSeparatedFor

added theorem CategoryTheory.Presheaf.w

added def CategoryTheory.Presieve.FamilyOfElements.SieveCompatible.cone

added theorem CategoryTheory.Sheaf.Hom.add_app

added theorem CategoryTheory.Sheaf.Hom.mono_of_presheaf_mono

added structure CategoryTheory.Sheaf.Hom

added theorem CategoryTheory.Sheaf.hom_ext

added def CategoryTheory.Sheaf.isTerminalOfBotCover

added structure CategoryTheory.Sheaf

added theorem CategoryTheory.isSheaf_iff_isSheaf_of_type

added def CategoryTheory.sheafEquivSheafOfTypes

added def CategoryTheory.sheafOver

added def CategoryTheory.sheafToPresheaf

Modified Mathlib/CategoryTheory/Sites/SheafOfTypes.lean