Commit 2024-12-22 09:55 112e2afa

View on Github →

feat(CategoryTheory): left and right lifting properties (#19135) Defines left/right lifting property wrt a MorphismProperty and shows basic closure properties (retracts, pullback/pushout, composition etc.).

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/CommSq.lean

Modified Mathlib/CategoryTheory/LiftingProperties/Basic.lean

added theorem CategoryTheory.RetractArrow.leftLiftingProperty

added theorem CategoryTheory.RetractArrow.rightLiftingProperty

Created Mathlib/CategoryTheory/LiftingProperties/Limits.lean

added theorem CategoryTheory.IsPullback.hasLiftingProperty

added theorem CategoryTheory.IsPushout.hasLiftingProperty

Created Mathlib/CategoryTheory/MorphismProperty/LiftingProperty.lean

added def CategoryTheory.MorphismProperty.llp

added theorem CategoryTheory.MorphismProperty.llp_IsStableUnderCoproductsOfShape

added theorem CategoryTheory.MorphismProperty.llp_isStableUnderRetracts

added def CategoryTheory.MorphismProperty.rlp

added theorem CategoryTheory.MorphismProperty.rlp_IsStableUnderProductsOfShape

added theorem CategoryTheory.MorphismProperty.rlp_isStableUnderRetracts

Modified Mathlib/CategoryTheory/MorphismProperty/Limits.lean

added theorem CategoryTheory.MorphismProperty.IsStableUnderColimitsOfShape.colim_map

added def CategoryTheory.MorphismProperty.IsStableUnderColimitsOfShape

added theorem CategoryTheory.MorphismProperty.IsStableUnderCoproductsOfShape.mk

modified theorem CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape.mk

added theorem CategoryTheory.MorphismProperty.isStableUnderCoproductsOfShape_of_isStableUnderFiniteCoproducts