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