Commit 2023-12-27 05:26 c9e4122d

View on Github →

feat(CategoryTheory/Sites): objects which cover the terminal object (#8632) In this PR, given a site (C, J), we introduce the notion of a family of objects Y : I → C which "cover the final object". This notion is used in order to formulate results about global sections of sheaves. It shall also be useful in future PRs in order to formulate descent properties of sheaves.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Sites/CoversTop.lean

added theorem CategoryTheory.GrothendieckTopology.CoversTop.ext

added theorem CategoryTheory.GrothendieckTopology.CoversTop.sections_ext

added def CategoryTheory.GrothendieckTopology.CoversTop

added theorem CategoryTheory.GrothendieckTopology.coversTop_iff_of_isTerminal

added theorem CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible.exists_unique_section

added theorem CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible.familyOfElements_apply

added theorem CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible.familyOfElements_isCompatible

added theorem CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible.section_apply

added def CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible

added def CategoryTheory.Presheaf.FamilyOfElementsOnObjects

Modified Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean

modified theorem CategoryTheory.Equalizer.Presieve.Arrows.sheaf_condition

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

added theorem CategoryTheory.Sieve.mem_ofArrows_iff

added theorem CategoryTheory.Sieve.mem_ofObjects_iff

added theorem CategoryTheory.Sieve.ofArrows_eq_ofObjects

added theorem CategoryTheory.Sieve.ofArrows_le_ofObjects

added theorem CategoryTheory.Sieve.ofArrows_mk

added def CategoryTheory.Sieve.ofObjects

added theorem CategoryTheory.Sieve.pullback_ofObjects_eq_top