Commit 2025-02-09 19:36 3d193da9

View on Github →

feat(CategoryTheory/MorphismProperty): more API for limits and retracts (#21596)

Estimated changes

Modified Mathlib/CategoryTheory/MorphismProperty/Limits.lean

added theorem CategoryTheory.MorphismProperty.IsStableUnderColimitsOfShape.isomorphisms

added theorem CategoryTheory.MorphismProperty.colimitsOfShape_eq_of_equivalence

added theorem CategoryTheory.MorphismProperty.colimitsOfShape_le_of_final

added theorem CategoryTheory.MorphismProperty.colimitsOfShape_monotone

added theorem CategoryTheory.MorphismProperty.coproducts_of_small

added theorem CategoryTheory.MorphismProperty.le_colimitsOfShape_punit

added theorem CategoryTheory.MorphismProperty.le_coproducts

added theorem CategoryTheory.MorphismProperty.pullbacks_monotone

added theorem CategoryTheory.MorphismProperty.pushouts_monotone

Modified Mathlib/CategoryTheory/MorphismProperty/Retract.lean

added theorem CategoryTheory.MorphismProperty.isStableUnderRetracts_iff_retracts_le

added theorem CategoryTheory.MorphismProperty.le_retracts

added def CategoryTheory.MorphismProperty.retracts

added theorem CategoryTheory.MorphismProperty.retracts_le

added theorem CategoryTheory.MorphismProperty.retracts_monotone