Commit 2025-03-09 19:11 f95da8d7

View on Github →

feat(CategoryTheory): finitely generated subpresheaves of types (#21173) We consider (sub)presheaves of types that are generated by finitely many sections.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Subpresheaf/Finite.lean

added theorem CategoryTheory.PresheafIsGeneratedBy.of_epi

added theorem CategoryTheory.PresheafIsGeneratedBy.range

added def CategoryTheory.Subpresheaf.IsFinite.Index

added theorem CategoryTheory.Subpresheaf.IsGeneratedBy.iSup_eq

added theorem CategoryTheory.Subpresheaf.IsGeneratedBy.image

added theorem CategoryTheory.Subpresheaf.IsGeneratedBy.isFinite

added theorem CategoryTheory.Subpresheaf.IsGeneratedBy.mem

added theorem CategoryTheory.Subpresheaf.IsGeneratedBy.ofSection_le

added theorem CategoryTheory.Subpresheaf.IsGeneratedBy.of_equiv

added def CategoryTheory.Subpresheaf.IsGeneratedBy

added theorem CategoryTheory.Subpresheaf.image_isFinite

added theorem CategoryTheory.Subpresheaf.isGeneratedBy_iff

added theorem CategoryTheory.Subpresheaf.isGeneratedBy_of_isFinite

added theorem CategoryTheory.Subpresheaf.range_isFinite

added theorem CategoryTheory.presheafIsFinite_of_epi

added theorem CategoryTheory.presheafIsGeneratedBy_of_isFinite

added theorem CategoryTheory.yoneda_obj_isGeneratedBy

Modified Mathlib/CategoryTheory/Subpresheaf/Image.lean

added theorem CategoryTheory.Subpresheaf.image_iSup

added theorem CategoryTheory.Subpresheaf.range_eq_top