Commit 2025-01-27 09:49 d17e5f6e

View on Github →

feat(CategoryTheory/Subpresheaf): preimage/image/range of subpresheaves (#21047)

Estimated changes

Modified Mathlib/CategoryTheory/Sites/LocallyInjective.lean

Modified Mathlib/CategoryTheory/Sites/LocallySurjective.lean

Modified Mathlib/CategoryTheory/Sites/Subsheaf.lean

added def CategoryTheory.Sheaf.image

added def CategoryTheory.Sheaf.imageι

added def CategoryTheory.Sheaf.toImage

added theorem CategoryTheory.Sheaf.toImage_ι

added def CategoryTheory.Subpresheaf.toRangeSheafify

deleted def CategoryTheory.imageSheaf

deleted def CategoryTheory.imageSheafι

deleted def CategoryTheory.toImagePresheafSheafify

deleted def CategoryTheory.toImageSheaf

deleted theorem CategoryTheory.toImageSheaf_ι

Modified Mathlib/CategoryTheory/Subpresheaf/Basic.lean

added theorem CategoryTheory.Subpresheaf.le_def

Modified Mathlib/CategoryTheory/Subpresheaf/Image.lean

added theorem CategoryTheory.Subpresheaf.epi_iff_range_eq_top

added def CategoryTheory.Subpresheaf.fromPreimage

added theorem CategoryTheory.Subpresheaf.fromPreimage_ι

added def CategoryTheory.Subpresheaf.image

added theorem CategoryTheory.Subpresheaf.image_comp

added theorem CategoryTheory.Subpresheaf.image_le_iff

added theorem CategoryTheory.Subpresheaf.image_top

modified def CategoryTheory.Subpresheaf.lift

modified theorem CategoryTheory.Subpresheaf.lift_ι

added def CategoryTheory.Subpresheaf.preimage

added theorem CategoryTheory.Subpresheaf.preimage_comp

added theorem CategoryTheory.Subpresheaf.preimage_eq_top_iff

added theorem CategoryTheory.Subpresheaf.preimage_id

added theorem CategoryTheory.Subpresheaf.preimage_image_of_epi

added def CategoryTheory.Subpresheaf.range

added theorem CategoryTheory.Subpresheaf.range_comp

added theorem CategoryTheory.Subpresheaf.range_comp_le

added theorem CategoryTheory.Subpresheaf.range_id

added theorem CategoryTheory.Subpresheaf.range_toRange

added theorem CategoryTheory.Subpresheaf.range_ι

added def CategoryTheory.Subpresheaf.toRange

added theorem CategoryTheory.Subpresheaf.toRange_app_val

added theorem CategoryTheory.Subpresheaf.toRange_ι

deleted def CategoryTheory.imagePresheaf

deleted theorem CategoryTheory.imagePresheaf_comp_le

deleted theorem CategoryTheory.imagePresheaf_id

deleted def CategoryTheory.toImagePresheaf

deleted theorem CategoryTheory.toImagePresheaf_ι

Modified Mathlib/CategoryTheory/Subpresheaf/Sieves.lean