Cardinals that are suitable for the small object argument

In this file, given a class of morphisms I : MorphismProperty C and a regular cardinal κ : Cardinal.{w}, we define a typeclass IsCardinalForSmallObjectArgument I κ which requires certain smallness properties (I is w-small, C is locally w-small), the existence of certain colimits (pushouts, coproducts of size w, and the condition HasIterationOfShape κ.ord.toType C about the existence of colimits indexed by limit ordinal smaller than or equal to κ.ord), and the technical assumption that if A is the a morphism in I, then the functor Hom(A, _) should commute with the filtering colimits corresponding to relative I-cell complexes. (This last condition shall hold when κ is the successor of an infinite cardinal c such that all these objects A are c-presentable, see Mathlib/CategoryTheory/Presentable/Basic.lean.)

Given I : MorphismProperty C, we shall say that I permits the small object argument if there exists κ such that IsCardinalForSmallObjectArgument I κ holds. See the file Mathlib/CategoryTheory/SmallObject/Basic.lean for the definition of this typeclass HasSmallObjectArgument and an outline of the proof.

Main results

Assuming IsCardinalForSmallObjectArgument I κ, any morphism f : X ⟶ Y is factored as ιObj I κ f ≫ πObj I κ f = f. It is shown that ιObj I κ f is a relative I-cell complex (see SmallObject.relativeCellComplexιObj) and that πObj I κ f has the right lifting property with respect to I (see SmallObject.rlp_πObj). This construction is obtained by iterating to the power κ.ord.toType the functor Arrow C ⥤ Arrow C defined in the file Mathlib/CategoryTheory/SmallObject/Construction.lean. This factorization is functorial in f and gives the property HasFunctorialFactorization I.rlp.llp I.rlp. Finally, the lemma llp_rlp_of_isCardinalForSmallObjectArgument (and its primed version) shows that the morphisms in I.rlp.llp are exactly the retracts of the transfinite compositions (of shape κ.ord.toType) of pushouts of coproducts of morphisms in I.

References

• https://ncatlab.org/nlab/show/small+object+argument

class CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] : Prop

Given I : MorphismProperty C and a regular cardinal κ : Cardinal.{w}, this property asserts the technical conditions which allow to proceed to the small object argument by doing a construction by transfinite induction indexed by the well ordered type κ.ord.toType.

• isSmall : IsSmall.{w, v, u} I
• locallySmall : LocallySmall.{w, v, u} C
• hasPushouts : Limits.HasPushouts C
• hasCoproducts : Limits.HasCoproducts C
• hasIterationOfShape : Limits.HasIterationOfShape κ.ord.toType C
• preservesColimit {A B X Y : C} (i : A ⟶ B) : I i → ∀ (f : X ⟶ Y) (hf : HomotopicalAlgebra.RelativeCellComplex (fun (x : κ.ord.toType) => I.homFamily) f), Limits.PreservesColimit hf.F (coyoneda.obj (Opposite.op A))

theorem CategoryTheory.SmallObject.isSmall {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] : MorphismProperty.IsSmall.{w, v, u} I

theorem CategoryTheory.SmallObject.locallySmall {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] : LocallySmall.{w, v, u} C

theorem CategoryTheory.SmallObject.hasIterationOfShape {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] : Limits.HasIterationOfShape κ.ord.toType C

theorem CategoryTheory.SmallObject.hasPushouts {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] : Limits.HasPushouts C

theorem CategoryTheory.SmallObject.hasCoproducts {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] : Limits.HasCoproducts C

theorem CategoryTheory.SmallObject.preservesColimit {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] {A B X Y : C} (i : A ⟶ B) (hi : I i) (f : X ⟶ Y) (hf : HomotopicalAlgebra.RelativeCellComplex (fun (x : κ.ord.toType) => I.homFamily) f) : Limits.PreservesColimit hf.F (coyoneda.obj (Opposite.op A))

theorem CategoryTheory.SmallObject.hasColimitsOfShape_discrete {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] (X Y : C) (p : X ⟶ Y) : Limits.HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C

noncomputable def CategoryTheory.SmallObject.succStruct {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] : SuccStruct (Functor (Arrow C) (Arrow C))

The successor structure on Arrow C ⥤ Arrow C corresponding to the iterations of the natural transformation ε : 𝟭 (Arrow C) ⟶ SmallObject.functor I.homFamily (see the file SmallObject.Construction).

noncomputable def CategoryTheory.SmallObject.attachCellsOfSuccStructProp {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] {F G : Functor (Arrow C) (Arrow C)} {φ : F ⟶ G} (h : (succStruct I κ).prop φ) (f : Arrow C) : HomotopicalAlgebra.AttachCells I.homFamily (φ.app f).left

For the successor structure succStruct I κ on Arrow C ⥤ Arrow C, the morphism from an object to its successor induces morphisms in C which consists in attaching I-cells.

def CategoryTheory.SmallObject.propArrow {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) : MorphismProperty (Arrow C)

The class of morphisms in Arrow C which on the left side are pushouts of coproducts of morphisms in I, and which are isomorphisms on the right side.

theorem CategoryTheory.SmallObject.succStruct_prop_le_propArrow {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] : (succStruct I κ).prop ≤ (propArrow I).functorCategory (Arrow C)

noncomputable def CategoryTheory.SmallObject.iterationFunctor {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] : Functor κ.ord.toType (Functor (Arrow C) (Arrow C))

The functor κ.ord.toType ⥤ Arrow C ⥤ Arrow C corresponding to the iterations of the successor structure succStruct I κ.

noncomputable def CategoryTheory.SmallObject.iteration {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] : Functor (Arrow C) (Arrow C)

The colimit of iterationFunctor I κ.

noncomputable def CategoryTheory.SmallObject.ιIteration {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] : Functor.id (Arrow C) ⟶ iteration I κ

The natural "inclusion" 𝟭 (Arrow C) ⟶ iteration I κ.

noncomputable def CategoryTheory.SmallObject.transfiniteCompositionOfShapeSuccStructPropιIteration {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] : (succStruct I κ).prop.TransfiniteCompositionOfShape κ.ord.toType (ιIteration I κ)

The morphism ιIteration I κ is a transfinite composition of shape κ.ord.toType of morphisms satisfying (succStruct I κ).prop.

@[simp]

theorem CategoryTheory.SmallObject.transfiniteCompositionOfShapeSuccStructPropιIteration_F {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] : (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).F = iterationFunctor I κ

noncomputable def CategoryTheory.SmallObject.transfiniteCompositionOfShapeιIterationAppRight {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] (f : Arrow C) : (MorphismProperty.isomorphisms C).TransfiniteCompositionOfShape κ.ord.toType ((ιIteration I κ).app f).right

For any f : Arrow C, the map ((ιIteration I κ).app f).right is a transfinite composition of isomorphisms.

instance CategoryTheory.SmallObject.instIsIsoRightAppArrowιIteration {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] (f : Arrow C) : IsIso ((ιIteration I κ).app f).right

instance CategoryTheory.SmallObject.instIsIsoRightAppArrowMapToTypeOrdFunctorIterationFunctor {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] {j₁ j₂ : κ.ord.toType} (φ : j₁ ⟶ j₂) (f : Arrow C) : IsIso (((iterationFunctor I κ).map φ).app f).right

noncomputable def CategoryTheory.SmallObject.iterationObjRightIso {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] (f : Arrow C) : f.right ≅ ((iteration I κ).obj f).right

For any f : Arrow C, the object ((iteration I κ).obj f).right identifies to f.right.

@[simp]

theorem CategoryTheory.SmallObject.iterationObjRightIso_hom {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] (f : Arrow C) : (iterationObjRightIso I κ f).hom = ((ιIteration I κ).app f).right

noncomputable def CategoryTheory.SmallObject.iterationFunctorObjObjRightIso {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] (f : Arrow C) (j : κ.ord.toType) : (((iterationFunctor I κ).obj j).obj f).right ≅ f.right

For any f : Arrow C and j : κ.ord.toType, the object (((iterationFunctor I κ).obj j).obj f).right identifies to f.right.

@[simp]

theorem CategoryTheory.SmallObject.iterationFunctorObjObjRightIso_ιIteration_app_right {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] (f : Arrow C) (j : κ.ord.toType) : CategoryStruct.comp (iterationFunctorObjObjRightIso I κ f j).hom ((ιIteration I κ).app f).right = (transfiniteCompositionOfShapeιIterationAppRight I κ f).incl.app j

@[simp]

theorem CategoryTheory.SmallObject.iterationFunctorObjObjRightIso_ιIteration_app_right_assoc {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] (f : Arrow C) (j : κ.ord.toType) {Z : C} (h : ((iteration I κ).obj f).right ⟶ Z) : CategoryStruct.comp (iterationFunctorObjObjRightIso I κ f j).hom (CategoryStruct.comp ((ιIteration I κ).app f).right h) = CategoryStruct.comp ((transfiniteCompositionOfShapeιIterationAppRight I κ f).incl.app j) h

theorem CategoryTheory.SmallObject.prop_iterationFunctor_map_succ {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] (j : κ.ord.toType) : (succStruct I κ).prop ((iterationFunctor I κ).map (homOfLE ⋯))

noncomputable def CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] (f : Arrow C) (j : κ.ord.toType) : Arrow.mk (((iterationFunctor I κ).map (homOfLE ⋯)).app f) ≅ Arrow.mk ((ε I.homFamily).app (((iterationFunctor I κ).obj j).obj f))

For any f : Arrow C and j : κ.ord.toType, the morphism ((iterationFunctor I κ).map (homOfLE (Order.le_succ j))).app f identifies to a morphism given by SmallObject.ε I.homFamily.

@[simp]

theorem CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_left {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] (f : Arrow C) (j : κ.ord.toType) : (iterationFunctorMapSuccAppArrowIso I κ f j).hom.left = CategoryStruct.id (Arrow.mk (((iterationFunctor I κ).map (homOfLE ⋯)).app f)).left

@[simp]

theorem CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_right_right_comp {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] (f : Arrow C) (j : κ.ord.toType) : CategoryStruct.comp (iterationFunctorMapSuccAppArrowIso I κ f j).hom.right.right (((iterationFunctor I κ).map (homOfLE ⋯)).app f).right = CategoryStruct.id (Arrow.mk (((iterationFunctor I κ).map (homOfLE ⋯)).app f)).right.right

@[simp]

theorem CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_right_right_comp_assoc {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] (f : Arrow C) (j : κ.ord.toType) {Z : C} (h : (((iterationFunctor I κ).obj (Order.succ j)).obj f).right ⟶ Z) : CategoryStruct.comp (iterationFunctorMapSuccAppArrowIso I κ f j).hom.right.right (CategoryStruct.comp (((iterationFunctor I κ).map (homOfLE ⋯)).app f).right h) = h

noncomputable def CategoryTheory.SmallObject.obj {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] {X Y : C} (f : X ⟶ Y) : C

The intermediate object in the factorization given by the small object argument.

noncomputable def CategoryTheory.SmallObject.ιObj {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] {X Y : C} (f : X ⟶ Y) : X ⟶ obj I κ f

The "inclusion" morphism in the factorization given by the the small object argument.

noncomputable def CategoryTheory.SmallObject.πObj {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] {X Y : C} (f : X ⟶ Y) : obj I κ f ⟶ Y

The "projection" morphism in the factorization given by the the small object argument.

@[simp]

theorem CategoryTheory.SmallObject.πObj_ιIteration_app_right {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp (πObj I κ f) ((ιIteration I κ).app (Arrow.mk f)).right = ((iteration I κ).obj (Arrow.mk f)).hom

@[simp]

theorem CategoryTheory.SmallObject.πObj_ιIteration_app_right_assoc {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] {X Y : C} (f : X ⟶ Y) {Z : C} (h : ((iteration I κ).obj (Arrow.mk f)).right ⟶ Z) : CategoryStruct.comp (πObj I κ f) (CategoryStruct.comp ((ιIteration I κ).app (Arrow.mk f)).right h) = CategoryStruct.comp ((iteration I κ).obj (Arrow.mk f)).hom h

@[simp]

theorem CategoryTheory.SmallObject.ιObj_πObj {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp (ιObj I κ f) (πObj I κ f) = f

@[simp]

theorem CategoryTheory.SmallObject.ιObj_πObj_assoc {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] {X Y : C} (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (ιObj I κ f) (CategoryStruct.comp (πObj I κ f) h) = CategoryStruct.comp f h

noncomputable def CategoryTheory.SmallObject.relativeCellComplexιObj {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] {X Y : C} (f : X ⟶ Y) : HomotopicalAlgebra.RelativeCellComplex (fun (x : κ.ord.toType) => I.homFamily) (ιObj I κ f)

The morphism ιObj I κ f is a relative I-cell complex.

theorem CategoryTheory.SmallObject.transfiniteCompositionsOfShape_ιObj {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] {X Y : C} (f : X ⟶ Y) : (MorphismProperty.coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape κ.ord.toType (ιObj I κ f)

theorem CategoryTheory.SmallObject.llp_rlp_ιObj {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] {X Y : C} (f : X ⟶ Y) : I.rlp.llp (ιObj I κ f)

noncomputable def CategoryTheory.SmallObject.relativeCellComplexιObjFObjSuccIso {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] {X Y : C} (f : X ⟶ Y) (j : κ.ord.toType) : (relativeCellComplexιObj I κ f).F.obj (Order.succ j) ≅ functorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom

When ιObj I κ f is considered as a relative I-cell complex, the object at the jth step is obtained by applying the construction SmallObject.functorObj.

theorem CategoryTheory.SmallObject.ιFunctorObj_eq {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] {X Y : C} (f : X ⟶ Y) (j : κ.ord.toType) : ιFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom = CategoryStruct.comp ((relativeCellComplexιObj I κ f).F.map (homOfLE ⋯)) (relativeCellComplexιObjFObjSuccIso I κ f j).hom

theorem CategoryTheory.SmallObject.πFunctorObj_eq {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] {X Y : C} (f : X ⟶ Y) (j : κ.ord.toType) : πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom = CategoryStruct.comp (relativeCellComplexιObjFObjSuccIso I κ f j).inv (CategoryStruct.comp ((relativeCellComplexιObj I κ f).incl.app (Order.succ j)) (CategoryStruct.comp (πObj I κ f) (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).inv))

theorem CategoryTheory.SmallObject.hasRightLiftingProperty_πObj {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] {X Y A B : C} (i : A ⟶ B) (hi : I i) (f : X ⟶ Y) : HasLiftingProperty i (πObj I κ f)

theorem CategoryTheory.SmallObject.rlp_πObj {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] {X Y : C} (f : X ⟶ Y) : I.rlp (πObj I κ f)

noncomputable def CategoryTheory.SmallObject.objMap {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] {f g : Arrow C} (φ : f ⟶ g) : obj I κ f.hom ⟶ obj I κ g.hom

The functoriality of the intermediate object in the factorization of the small object argument.

@[simp]

theorem CategoryTheory.SmallObject.objMap_id {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] (f : Arrow C) : objMap I κ (CategoryStruct.id f) = CategoryStruct.id (obj I κ f.hom)

@[simp]

theorem CategoryTheory.SmallObject.objMap_comp {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] {f g h : Arrow C} (φ : f ⟶ g) (ψ : g ⟶ h) : objMap I κ (CategoryStruct.comp φ ψ) = CategoryStruct.comp (objMap I κ φ) (objMap I κ ψ)

theorem CategoryTheory.SmallObject.objMap_comp_assoc {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] {f g h : Arrow C} (φ : f ⟶ g) (ψ : g ⟶ h) {Z : C} (h✝ : obj I κ h.hom ⟶ Z) : CategoryStruct.comp (objMap I κ (CategoryStruct.comp φ ψ)) h✝ = CategoryStruct.comp (objMap I κ φ) (CategoryStruct.comp (objMap I κ ψ) h✝)

@[simp]

theorem CategoryTheory.SmallObject.ιObj_naturality {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] {f g : Arrow C} (φ : f ⟶ g) : CategoryStruct.comp (ιObj I κ f.hom) (objMap I κ φ) = CategoryStruct.comp φ.left (ιObj I κ g.hom)

@[simp]

theorem CategoryTheory.SmallObject.ιObj_naturality_assoc {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] {f g : Arrow C} (φ : f ⟶ g) {Z : C} (h : obj I κ g.hom ⟶ Z) : CategoryStruct.comp (ιObj I κ f.hom) (CategoryStruct.comp (objMap I κ φ) h) = CategoryStruct.comp φ.left (CategoryStruct.comp (ιObj I κ g.hom) h)

@[simp]

theorem CategoryTheory.SmallObject.πObj_naturality {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] {f g : Arrow C} (φ : f ⟶ g) : CategoryStruct.comp (objMap I κ φ) (πObj I κ g.hom) = CategoryStruct.comp (πObj I κ f.hom) φ.right

@[simp]

theorem CategoryTheory.SmallObject.πObj_naturality_assoc {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] {f g : Arrow C} (φ : f ⟶ g) {Z : C} (h : g.right ⟶ Z) : CategoryStruct.comp (objMap I κ φ) (CategoryStruct.comp (πObj I κ g.hom) h) = CategoryStruct.comp (πObj I κ f.hom) (CategoryStruct.comp φ.right h)

noncomputable def CategoryTheory.SmallObject.functorialFactorizationData {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] : I.rlp.llp.FunctorialFactorizationData I.rlp

The functorial factorization ιObj I κ f ≫ πObj I κ f.hom = f with ιObj I κ f in I.rlp.llp and πObj I κ f.hom in I.rlp.

@[simp]

theorem CategoryTheory.SmallObject.functorialFactorizationData_Z_map {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] {X✝ Y✝ : Arrow C} (φ : X✝ ⟶ Y✝) : (functorialFactorizationData I κ).Z.map φ = objMap I κ φ

@[simp]

theorem CategoryTheory.SmallObject.functorialFactorizationData_p_app {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] (f : Arrow C) : (functorialFactorizationData I κ).p.app f = πObj I κ f.hom

@[simp]

theorem CategoryTheory.SmallObject.functorialFactorizationData_i_app {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] (f : Arrow C) : (functorialFactorizationData I κ).i.app f = ιObj I κ f.hom

@[simp]

theorem CategoryTheory.SmallObject.functorialFactorizationData_Z_obj {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] (f : Arrow C) : (functorialFactorizationData I κ).Z.obj f = obj I κ f.hom

theorem CategoryTheory.SmallObject.hasFunctorialFactorization {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] : I.rlp.llp.HasFunctorialFactorization I.rlp

theorem CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument' {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] : I.rlp.llp = ((MorphismProperty.coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape κ.ord.toType).retracts

If κ is a suitable cardinal for the small object argument for I : MorphismProperty C, then the class I.rlp.llp is exactly the class of morphisms that are retracts of transfinite compositions (of shape κ.ord.toType) of pushouts of coproducts of maps in I.

theorem CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument {C : Type u} [Category.{v, u} C] (I : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [OrderBot κ.ord.toType] [I.IsCardinalForSmallObjectArgument κ] : I.rlp.llp = (MorphismProperty.transfiniteCompositions.{w, v, u} (MorphismProperty.coproducts.{w, v, u} I).pushouts).retracts

If κ is a suitable cardinal for the small object argument for I : MorphismProperty C, then the class I.rlp.llp is exactly the class of morphisms that are retracts of transfinite compositions of pushouts of coproducts of maps in I.