Commit 2025-02-11 05:58 66c4d099

View on Github →

feat(CategoryTheory/SmallObject): llp is stable under transfinite composition (#21682) We deduce from previous results (#20119) that if W : MorphismProperty C, then the class W.llp of morphisms which satisfy the left lifting property with respect to W is stable under transfinite composition.

Estimated changes

Modified Mathlib/CategoryTheory/MorphismProperty/Basic.lean

modified theorem CategoryTheory.MorphismProperty.iSup_iff

Modified Mathlib/CategoryTheory/MorphismProperty/TransfiniteComposition.lean

added def CategoryTheory.MorphismProperty.transfiniteCompositions

added theorem CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le_transfiniteCompositions

added theorem CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_monotone

added theorem CategoryTheory.MorphismProperty.transfiniteCompositions_iff

Modified Mathlib/CategoryTheory/SmallObject/TransfiniteCompositionLifting.lean

added theorem CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le_llp_rlp

added theorem CategoryTheory.MorphismProperty.transfiniteCompositions_le_llp_rlp