Commit 2024-12-20 17:08 7f72da4f

View on Github →

feat(CategoryTheory): the left lifting property is stable under transfinite composition (#20119) After #19135 is merged, it will be possible to phrase this in terms of MorphismProperty.llp and get better looking statements.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/SmallObject/TransfiniteCompositionLifting.lean

added def CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.map

added theorem CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.sq

added theorem CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w

added structure CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct

added theorem CategoryTheory.HasLiftingProperty.transfiniteComposition.hasLift

added theorem CategoryTheory.HasLiftingProperty.transfiniteComposition.hasLiftingProperty_ι_app_bot

added def CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctor

added theorem CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom_fac

added theorem CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.map_lift