Commit 2025-01-23 09:23 8fac96b5

View on Github →

chore(CategoryTheory/Subpresheaf): split files (#20978) This PR only moves definitions and lemmas into two new files Subpresheaf.Sieves and Subpresheaf.Image in order to prepare for the development of new API.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Sites/Subsheaf.lean

Modified Mathlib/CategoryTheory/Subpresheaf/Basic.lean

deleted def CategoryTheory.Subpresheaf.familyOfElementsOfSection

deleted theorem CategoryTheory.Subpresheaf.family_of_elements_compatible

deleted def CategoryTheory.Subpresheaf.lift

deleted theorem CategoryTheory.Subpresheaf.lift_ι

deleted def CategoryTheory.Subpresheaf.sieveOfSection

deleted def CategoryTheory.imagePresheaf

deleted theorem CategoryTheory.imagePresheaf_comp_le

deleted theorem CategoryTheory.imagePresheaf_id

deleted def CategoryTheory.toImagePresheaf

deleted theorem CategoryTheory.toImagePresheaf_ι

Created Mathlib/CategoryTheory/Subpresheaf/Image.lean

added def CategoryTheory.Subpresheaf.lift

added theorem CategoryTheory.Subpresheaf.lift_ι

added def CategoryTheory.imagePresheaf

added theorem CategoryTheory.imagePresheaf_comp_le

added theorem CategoryTheory.imagePresheaf_id

added def CategoryTheory.toImagePresheaf

added theorem CategoryTheory.toImagePresheaf_ι

Created Mathlib/CategoryTheory/Subpresheaf/Sieves.lean

added def CategoryTheory.Subpresheaf.familyOfElementsOfSection

added theorem CategoryTheory.Subpresheaf.family_of_elements_compatible

added def CategoryTheory.Subpresheaf.sieveOfSection