Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-05-16 18:39
c6d1b53d
View on Github →
feat: port CategoryTheory.Sites.Subsheaf (
#3997
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/CategoryTheory/Sites/Subsheaf.lean
added
theorem
CategoryTheory.GrothendieckTopology.Subpresheaf.eq_sheafify
added
theorem
CategoryTheory.GrothendieckTopology.Subpresheaf.eq_sheafify_iff
added
theorem
CategoryTheory.GrothendieckTopology.Subpresheaf.eq_top_iff_isIso
added
def
CategoryTheory.GrothendieckTopology.Subpresheaf.familyOfElementsOfSection
added
theorem
CategoryTheory.GrothendieckTopology.Subpresheaf.family_of_elements_compatible
added
def
CategoryTheory.GrothendieckTopology.Subpresheaf.homOfLe
added
theorem
CategoryTheory.GrothendieckTopology.Subpresheaf.homOfLe_ι
added
theorem
CategoryTheory.GrothendieckTopology.Subpresheaf.isSheaf_iff
added
theorem
CategoryTheory.GrothendieckTopology.Subpresheaf.le_sheafify
added
def
CategoryTheory.GrothendieckTopology.Subpresheaf.lift
added
theorem
CategoryTheory.GrothendieckTopology.Subpresheaf.lift_ι
added
theorem
CategoryTheory.GrothendieckTopology.Subpresheaf.nat_trans_naturality
added
def
CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify
added
theorem
CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify_isSheaf
added
theorem
CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify_le
added
theorem
CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify_sheafify
added
def
CategoryTheory.GrothendieckTopology.Subpresheaf.sieveOfSection
added
def
CategoryTheory.GrothendieckTopology.Subpresheaf.toPresheaf
added
theorem
CategoryTheory.GrothendieckTopology.Subpresheaf.to_sheafifyLift
added
theorem
CategoryTheory.GrothendieckTopology.Subpresheaf.to_sheafify_lift_unique
added
def
CategoryTheory.GrothendieckTopology.Subpresheaf.ι
added
structure
CategoryTheory.GrothendieckTopology.Subpresheaf
added
def
CategoryTheory.GrothendieckTopology.imageMonoFactorization
added
def
CategoryTheory.GrothendieckTopology.imagePresheaf
added
theorem
CategoryTheory.GrothendieckTopology.imagePresheaf_comp_le
added
theorem
CategoryTheory.GrothendieckTopology.imagePresheaf_id
added
def
CategoryTheory.GrothendieckTopology.imageSheaf
added
def
CategoryTheory.GrothendieckTopology.imageSheafι
added
def
CategoryTheory.GrothendieckTopology.toImagePresheaf
added
def
CategoryTheory.GrothendieckTopology.toImagePresheafSheafify
added
theorem
CategoryTheory.GrothendieckTopology.toImagePresheaf_ι
added
def
CategoryTheory.GrothendieckTopology.toImageSheaf
added
theorem
CategoryTheory.GrothendieckTopology.toImageSheaf_ι
added
theorem
CategoryTheory.GrothendieckTopology.top_subpresheaf_obj