Commit 2025-12-11 06:55 b6513d2f

View on Github →

feat(CategoryTheory): more preservation properties of functors (#32423) We consider the preservation of a limit or a colimit as an ObjectProperty in the category of functors.

Estimated changes

Modified Mathlib/CategoryTheory/ObjectProperty/FunctorCategory/PreservesLimits.lean

added theorem CategoryTheory.ObjectProperty.congr_preservesColimit

added theorem CategoryTheory.ObjectProperty.congr_preservesColimitsOfShape

added theorem CategoryTheory.ObjectProperty.congr_preservesLimit

added theorem CategoryTheory.ObjectProperty.congr_preservesLimitsOfShape

added theorem CategoryTheory.ObjectProperty.preservesColimit_iff

added theorem CategoryTheory.ObjectProperty.preservesColimitsOfShape_eq_iSup

added theorem CategoryTheory.ObjectProperty.preservesColimitsOfShape_iff

added theorem CategoryTheory.ObjectProperty.preservesFiniteColimits_iff

added theorem CategoryTheory.ObjectProperty.preservesLimit_iff

added theorem CategoryTheory.ObjectProperty.preservesLimitsOfShape_eq_iSup