Documentation

Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

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 #

source
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.

Instances
    source
    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
    source
    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
    source
    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
    source
    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
    source
    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
    source
    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))
    source
    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
    source
    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).

    Equations
    source
    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.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    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.

    Equations
    source
    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)
    source
    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 κ.

    Equations
    source
    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 κ.

    Equations
    source
    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 κ.

    Equations
    source
    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.

    Equations
    source
    @[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 κ
    source
    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.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    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
    source
    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
    source
    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.

    Equations
    source
    @[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
    source
    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.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[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
    source
    @[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
    source
    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 ⋯))
    source
    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.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[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
    source
    @[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
    source
    @[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
    source
    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.

    Equations
    source
    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.

    Equations
    source
    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.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[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
    source
    @[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
    source
    @[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
    source
    @[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
    source
    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.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    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)
    source
    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)
    source
    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.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    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
    source
    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))
    source
    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)
    source
    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)
    source
    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.

    Equations
    source
    @[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)
    source
    @[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 κ ψ)
    source
    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✝)
    source
    @[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)
    source
    @[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)
    source
    @[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
    source
    @[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)
    source
    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.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[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 κ φ
    source
    @[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
    source
    @[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
    source
    @[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
    source
    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
    source
    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.

    source
    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.