Commit 2025-02-15 18:13 3e03c00e

View on Github →

feat(CategoryTheory/SmallObject): the functorial factorization (#21911) The main results in the small object argument are obtained in this PR. If I : MorphismProperty C has a cardinal that is suitable for the small object argument, then any morphism in C can be factored functorialy as a morphism in I.rlp.llp followed by a morphism in I.rlp.

Estimated changes

Modified Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean

added theorem CategoryTheory.SmallObject.hasFunctorialFactorization

added theorem CategoryTheory.SmallObject.hasRightLiftingProperty_πObj

added theorem CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_left

added theorem CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_right_right_comp

added theorem CategoryTheory.SmallObject.iterationFunctorObjObjRightIso_ιIteration_app_right

added theorem CategoryTheory.SmallObject.llp_rlp_ιObj

added theorem CategoryTheory.SmallObject.objMap_comp

added theorem CategoryTheory.SmallObject.objMap_id

added theorem CategoryTheory.SmallObject.prop_iterationFunctor_map_succ

added theorem CategoryTheory.SmallObject.rlp_πObj

added theorem CategoryTheory.SmallObject.transfiniteCompositionsOfShape_ιObj

added theorem CategoryTheory.SmallObject.ιFunctorObj_eq

added theorem CategoryTheory.SmallObject.ιObj_naturality

added theorem CategoryTheory.SmallObject.ιObj_πObj

added theorem CategoryTheory.SmallObject.πFunctorObj_eq

added theorem CategoryTheory.SmallObject.πObj_naturality

added theorem CategoryTheory.SmallObject.πObj_ιIteration_app_right

Modified Mathlib/CategoryTheory/SmallObject/TransfiniteCompositionLifting.lean

added theorem CategoryTheory.MorphismProperty.retracts_transfiniteComposition_pushouts_coproducts_le_llp_rlp

added theorem CategoryTheory.MorphismProperty.retracts_transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp

added theorem CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp

added theorem CategoryTheory.MorphismProperty.transfiniteCompositions_pushouts_coproducts_le_llp_rlp