Commit 2025-10-02 15:01 4dd34c03

View on Github →

feat(CategoryTheory/Limits/MorphismProperty): dualise lemmas on limits (#30127) We also add the object properties induced by morphism properties for Comma, CostructuredArrow and StructuredArrow and use them accordingly.

Estimated changes

Modified Mathlib/CategoryTheory/Limits/MorphismProperty.lean

added theorem CategoryTheory.MorphismProperty.Comma.hasColimit_of_closedUnderColimitsOfShape

added theorem CategoryTheory.MorphismProperty.Comma.hasColimitsOfShape_of_closedUnderColimitsOfShape

Modified Mathlib/CategoryTheory/MorphismProperty/Comma.lean

added def CategoryTheory.MorphismProperty.commaObj

added theorem CategoryTheory.MorphismProperty.commaObj_iff

added def CategoryTheory.MorphismProperty.costructuredArrowObj

added theorem CategoryTheory.MorphismProperty.costructuredArrowObj_iff

added def CategoryTheory.MorphismProperty.structuredArrowObj

added theorem CategoryTheory.MorphismProperty.structuredArrowObj_iff