Commit 2025-09-18 18:51 4f7d34ed

View on Github →

feat(CategoryTheory/MorphismProperty): define ind P (#29380) Given a morphism property P, we define a morphism property ind P that is satisfied for f : X ⟶ Y if Y is a filtered colimit of Yᵢ and fᵢ : X ⟶ Yᵢ satisfy P. We show that ind is idempotent under certain compactness assumptions.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Limits/Presentation.lean

added def CategoryTheory.Limits.ColimitPresentation.reindex

Modified Mathlib/CategoryTheory/MorphismProperty/Comma.lean

added def CategoryTheory.MorphismProperty.over

added def CategoryTheory.MorphismProperty.overObj

added theorem CategoryTheory.MorphismProperty.overObj_iff

added theorem CategoryTheory.MorphismProperty.over_iff

added def CategoryTheory.MorphismProperty.under

added def CategoryTheory.MorphismProperty.underObj

added theorem CategoryTheory.MorphismProperty.underObj_iff

added theorem CategoryTheory.MorphismProperty.under_iff

Created Mathlib/CategoryTheory/MorphismProperty/Ind.lean

added theorem CategoryTheory.MorphismProperty.exists_hom_of_isFinitelyPresentable

added def CategoryTheory.MorphismProperty.ind

added theorem CategoryTheory.MorphismProperty.ind_iff_ind_underMk

added theorem CategoryTheory.MorphismProperty.ind_ind

added theorem CategoryTheory.MorphismProperty.ind_underObj_pushout

added theorem CategoryTheory.MorphismProperty.le_ind

added theorem CategoryTheory.MorphismProperty.underObj_ind_eq_ind_underObj

Created Mathlib/CategoryTheory/ObjectProperty/Ind.lean

added def CategoryTheory.ObjectProperty.ind

added theorem CategoryTheory.ObjectProperty.ind_ind

added theorem CategoryTheory.ObjectProperty.le_ind

Modified Mathlib/CategoryTheory/Presentable/Finite.lean

added def CategoryTheory.MorphismProperty.isFinitelyPresentable

added def CategoryTheory.ObjectProperty.isFinitelyPresentable

Created Mathlib/CategoryTheory/WithTerminal/Lemmas.lean