Commit 2023-04-02 23:34 7eee4331

View on Github →

feat: port CategoryTheory.Sites.SheafOfTypes (#3223)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Adjunction/Evaluation.lean

Modified Mathlib/CategoryTheory/Limits/Constructions/FiniteProductsOfBinaryProducts.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Products.lean

Created Mathlib/CategoryTheory/Sites/SheafOfTypes.lean

added theorem CategoryTheory.Equalizer.FirstObj.ext

added def CategoryTheory.Equalizer.FirstObj

added def CategoryTheory.Equalizer.Presieve.SecondObj

added theorem CategoryTheory.Equalizer.Presieve.compatible_iff

added def CategoryTheory.Equalizer.Presieve.firstMap

added def CategoryTheory.Equalizer.Presieve.secondMap

added theorem CategoryTheory.Equalizer.Presieve.sheaf_condition

added theorem CategoryTheory.Equalizer.Presieve.w

added theorem CategoryTheory.Equalizer.Sieve.SecondObj.ext

added def CategoryTheory.Equalizer.Sieve.SecondObj

added theorem CategoryTheory.Equalizer.Sieve.compatible_iff

added theorem CategoryTheory.Equalizer.Sieve.equalizer_sheaf_condition

added def CategoryTheory.Equalizer.Sieve.firstMap

added def CategoryTheory.Equalizer.Sieve.secondMap

added theorem CategoryTheory.Equalizer.Sieve.w

added def CategoryTheory.Equalizer.firstObjEqFamily

added def CategoryTheory.Equalizer.forkMap

added theorem CategoryTheory.Presieve.FamilyOfElements.Compatible.compPresheafMap

added theorem CategoryTheory.Presieve.FamilyOfElements.Compatible.functorPullback

added theorem CategoryTheory.Presieve.FamilyOfElements.Compatible.pullback

added theorem CategoryTheory.Presieve.FamilyOfElements.Compatible.restrict

added theorem CategoryTheory.Presieve.FamilyOfElements.Compatible.sieveExtend

added theorem CategoryTheory.Presieve.FamilyOfElements.Compatible.to_sieveCompatible

added def CategoryTheory.Presieve.FamilyOfElements.Compatible

added theorem CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation.compPresheafMap

added def CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation

added def CategoryTheory.Presieve.FamilyOfElements.PullbackCompatible

added def CategoryTheory.Presieve.FamilyOfElements.SieveCompatible

added def CategoryTheory.Presieve.FamilyOfElements.compPresheafMap

added theorem CategoryTheory.Presieve.FamilyOfElements.compPresheafMap_comp

added theorem CategoryTheory.Presieve.FamilyOfElements.compPresheafMap_id

added theorem CategoryTheory.Presieve.FamilyOfElements.comp_of_compatible

added def CategoryTheory.Presieve.FamilyOfElements.functorPullback

added def CategoryTheory.Presieve.FamilyOfElements.pullback

added def CategoryTheory.Presieve.FamilyOfElements.restrict

added def CategoryTheory.Presieve.FamilyOfElements

added def CategoryTheory.Presieve.IsSeparated

added theorem CategoryTheory.Presieve.IsSeparatedFor.ext

added theorem CategoryTheory.Presieve.IsSeparatedFor.isSheafFor

added def CategoryTheory.Presieve.IsSeparatedFor

added theorem CategoryTheory.Presieve.IsSheaf.isSheafFor

added def CategoryTheory.Presieve.IsSheaf

added theorem CategoryTheory.Presieve.IsSheafFor.functorInclusion_comp_extend

added theorem CategoryTheory.Presieve.IsSheafFor.hom_ext

added theorem CategoryTheory.Presieve.IsSheafFor.isAmalgamation

added theorem CategoryTheory.Presieve.IsSheafFor.isSeparatedFor

added theorem CategoryTheory.Presieve.IsSheafFor.unique_extend

added theorem CategoryTheory.Presieve.IsSheafFor.valid_glue

added def CategoryTheory.Presieve.IsSheafFor

added def CategoryTheory.Presieve.YonedaSheafCondition

added theorem CategoryTheory.Presieve.compatible_iff_sieveCompatible

added theorem CategoryTheory.Presieve.extend_agrees

added theorem CategoryTheory.Presieve.extend_restrict

added theorem CategoryTheory.Presieve.extension_iff_amalgamation

added theorem CategoryTheory.Presieve.isAmalgamation_restrict

added theorem CategoryTheory.Presieve.isAmalgamation_sieveExtend

added theorem CategoryTheory.Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor

added theorem CategoryTheory.Presieve.isSeparatedFor_iff_generate

added theorem CategoryTheory.Presieve.isSeparatedFor_top

added theorem CategoryTheory.Presieve.isSeparated_of_isSheaf

added theorem CategoryTheory.Presieve.isSheafFor_iff_generate

added theorem CategoryTheory.Presieve.isSheafFor_iff_yonedaSheafCondition

added theorem CategoryTheory.Presieve.isSheafFor_iso

added theorem CategoryTheory.Presieve.isSheafFor_singleton_iso

added theorem CategoryTheory.Presieve.isSheafFor_subsieve

added theorem CategoryTheory.Presieve.isSheafFor_subsieve_aux

added theorem CategoryTheory.Presieve.isSheafFor_top_sieve

added theorem CategoryTheory.Presieve.isSheaf_bot

added theorem CategoryTheory.Presieve.isSheaf_iso

added theorem CategoryTheory.Presieve.isSheaf_of_le

added theorem CategoryTheory.Presieve.isSheaf_of_yoneda

added theorem CategoryTheory.Presieve.isSheaf_pretopology

added theorem CategoryTheory.Presieve.is_compatible_of_exists_amalgamation

added def CategoryTheory.Presieve.natTransEquivCompatibleFamily

added theorem CategoryTheory.Presieve.pullbackCompatible_iff

added theorem CategoryTheory.Presieve.restrict_extend

added theorem CategoryTheory.Presieve.restrict_inj

added structure CategoryTheory.SheafOfTypes.Hom

added structure CategoryTheory.SheafOfTypes

added def CategoryTheory.sheafOfTypesBotEquiv

added def CategoryTheory.sheafOfTypesToPresheaf