Construction for the small object argument

Given a family of morphisms f i : A i ⟶ B i in a category C, we define a functor SmallObject.functor f : Arrow S ⥤ Arrow S which sends an object given by arrow πX : X ⟶ S to the pushout functorObj f πX:

∐ functorObjSrcFamily f πX ⟶       X

            |                      |
            |                      |
            v                      v

∐ functorObjTgtFamily f πX ⟶ functorObj f πX

where the morphism on the left is a coproduct (of copies of maps f i) indexed by a type FunctorObjIndex f πX which parametrizes the diagrams of the form

A i ⟶ X
 |    |
 |    |
 v    v
B i ⟶ S

The morphism ιFunctorObj f πX : X ⟶ functorObj f πX is part of a natural transformation SmallObject.ε f : 𝟭 (Arrow C) ⟶ functor f S. The main idea in this construction is that for any commutative square as above, there may not exist a lifting B i ⟶ X, but the construction provides a tautological morphism B i ⟶ functorObj f πX (see SmallObject.ιFunctorObj_extension).

References

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

structure CategoryTheory.SmallObject.FunctorObjIndex {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) : Type (max v w)

Given a family of morphisms f i : A i ⟶ B i and a morphism πX : X ⟶ S, this type parametrizes the commutative squares with a morphism f i on the left and πX in the right.

• i : I

  an element in the index type

• t : A self.i ⟶ X

  the top morphism in the square

• b : B self.i ⟶ S

  the bottom morphism in the square

• w : CategoryStruct.comp self.t πX = CategoryStruct.comp (f self.i) self.b

@[simp]

theorem CategoryTheory.SmallObject.FunctorObjIndex.w_assoc {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} {f : (i : I) → A i ⟶ B i} {S X : C} {πX : X ⟶ S} (self : FunctorObjIndex f πX) {Z : C} (h : S ⟶ Z) : CategoryStruct.comp self.t (CategoryStruct.comp πX h) = CategoryStruct.comp (f self.i) (CategoryStruct.comp self.b h)

@[reducible, inline]

abbrev CategoryTheory.SmallObject.functorObjSrcFamily {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) (x : FunctorObjIndex f πX) : C

The family of objects A x.i parametrized by x : FunctorObjIndex f πX.

Equations

• CategoryTheory.SmallObject.functorObjSrcFamily f πX x = A x.i

@[reducible, inline]

abbrev CategoryTheory.SmallObject.functorObjTgtFamily {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) (x : FunctorObjIndex f πX) : C

The family of objects B x.i parametrized by x : FunctorObjIndex f πX.

Equations

• CategoryTheory.SmallObject.functorObjTgtFamily f πX x = B x.i

@[reducible, inline]

abbrev CategoryTheory.SmallObject.functorObjLeftFamily {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) (x : FunctorObjIndex f πX) : functorObjSrcFamily f πX x ⟶ functorObjTgtFamily f πX x

The family of the morphisms f x.i : A x.i ⟶ B x.i parametrized by x : FunctorObjIndex f πX.

Equations

• CategoryTheory.SmallObject.functorObjLeftFamily f πX x = f x.i

@[reducible, inline]

noncomputable abbrev CategoryTheory.SmallObject.functorObjTop {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] : ∐ functorObjSrcFamily f πX ⟶ X

The top morphism in the pushout square in the definition of pushoutObj f πX.

Equations

• CategoryTheory.SmallObject.functorObjTop f πX = CategoryTheory.Limits.Sigma.desc fun (x : CategoryTheory.SmallObject.FunctorObjIndex f πX) => x.t

@[reducible, inline]

noncomputable abbrev CategoryTheory.SmallObject.functorObjLeft {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjTgtFamily f πX

The left morphism in the pushout square in the definition of pushoutObj f πX.

Equations

• CategoryTheory.SmallObject.functorObjLeft f πX = CategoryTheory.Limits.Sigma.map (CategoryTheory.SmallObject.functorObjLeftFamily f πX)

@[reducible, inline]

noncomputable abbrev CategoryTheory.SmallObject.functorObj {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] : C

The functor SmallObject.functor f : Arrow C ⥤ Arrow C that is part of the small object argument for a family of morphisms f, on an object given as a morphism πX : X ⟶ S.

Equations

• CategoryTheory.SmallObject.functorObj f πX = CategoryTheory.Limits.pushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)

@[reducible, inline]

noncomputable abbrev CategoryTheory.SmallObject.ιFunctorObj {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] : X ⟶ functorObj f πX

The canonical morphism X ⟶ functorObj f πX.

Equations

• CategoryTheory.SmallObject.ιFunctorObj f πX = CategoryTheory.Limits.pushout.inl (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)

@[reducible, inline]

noncomputable abbrev CategoryTheory.SmallObject.ρFunctorObj {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] : ∐ functorObjTgtFamily f πX ⟶ functorObj f πX

The canonical morphism ∐ (functorObjTgtFamily f πX) ⟶ functorObj f πX.

Equations

• CategoryTheory.SmallObject.ρFunctorObj f πX = CategoryTheory.Limits.pushout.inr (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)

theorem CategoryTheory.SmallObject.functorObj_comm {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] : CategoryStruct.comp (functorObjTop f πX) (ιFunctorObj f πX) = CategoryStruct.comp (functorObjLeft f πX) (ρFunctorObj f πX)

theorem CategoryTheory.SmallObject.functorObj_comm_assoc {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] {Z : C} (h : functorObj f πX ⟶ Z) : CategoryStruct.comp (functorObjTop f πX) (CategoryStruct.comp (ιFunctorObj f πX) h) = CategoryStruct.comp (functorObjLeft f πX) (CategoryStruct.comp (ρFunctorObj f πX) h)

theorem CategoryTheory.SmallObject.functorObj_isPushout {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] : IsPushout (functorObjTop f πX) (functorObjLeft f πX) (ιFunctorObj f πX) (ρFunctorObj f πX)

theorem CategoryTheory.SmallObject.FunctorObjIndex.comm {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] (x : FunctorObjIndex f πX) : CategoryStruct.comp (f x.i) (CategoryStruct.comp (Limits.Sigma.ι (functorObjTgtFamily f πX) x) (ρFunctorObj f πX)) = CategoryStruct.comp x.t (ιFunctorObj f πX)

theorem CategoryTheory.SmallObject.FunctorObjIndex.comm_assoc {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] (x : FunctorObjIndex f πX) {Z : C} (h : functorObj f πX ⟶ Z) : CategoryStruct.comp (f x.i) (CategoryStruct.comp (Limits.Sigma.ι (functorObjTgtFamily f πX) x) (CategoryStruct.comp (ρFunctorObj f πX) h)) = CategoryStruct.comp x.t (CategoryStruct.comp (ιFunctorObj f πX) h)

@[reducible, inline]

noncomputable abbrev CategoryTheory.SmallObject.π'FunctorObj {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] : ∐ functorObjTgtFamily f πX ⟶ S

The canonical projection on the base object.

Equations

• CategoryTheory.SmallObject.π'FunctorObj f πX = CategoryTheory.Limits.Sigma.desc fun (x : CategoryTheory.SmallObject.FunctorObjIndex f πX) => x.b

noncomputable def CategoryTheory.SmallObject.πFunctorObj {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] : functorObj f πX ⟶ S

The canonical projection on the base object.

Equations

• CategoryTheory.SmallObject.πFunctorObj f πX = CategoryTheory.Limits.pushout.desc πX (CategoryTheory.SmallObject.π'FunctorObj f πX) ⋯

@[simp]

theorem CategoryTheory.SmallObject.ρFunctorObj_π {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] : CategoryStruct.comp (ρFunctorObj f πX) (πFunctorObj f πX) = π'FunctorObj f πX

@[simp]

theorem CategoryTheory.SmallObject.ρFunctorObj_π_assoc {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] {Z : C} (h : S ⟶ Z) : CategoryStruct.comp (ρFunctorObj f πX) (CategoryStruct.comp (πFunctorObj f πX) h) = CategoryStruct.comp (π'FunctorObj f πX) h

@[simp]

theorem CategoryTheory.SmallObject.ιFunctorObj_πFunctorObj {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] : CategoryStruct.comp (ιFunctorObj f πX) (πFunctorObj f πX) = πX

@[simp]

theorem CategoryTheory.SmallObject.ιFunctorObj_πFunctorObj_assoc {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] {Z : C} (h : S ⟶ Z) : CategoryStruct.comp (ιFunctorObj f πX) (CategoryStruct.comp (πFunctorObj f πX) h) = CategoryStruct.comp πX h

noncomputable def CategoryTheory.SmallObject.attachCellsιFunctorObj {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] : HomotopicalAlgebra.AttachCells f (ιFunctorObj f πX)

The morphism ιFunctorObj f πX : X ⟶ functorObj f πX is obtained by attaching f-cells.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.SmallObject.attachCellsιFunctorObj_ι {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] : (attachCellsιFunctorObj f πX).ι = FunctorObjIndex f πX

@[simp]

theorem CategoryTheory.SmallObject.attachCellsιFunctorObj_g₁ {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] : (attachCellsιFunctorObj f πX).g₁ = functorObjTop f πX

@[simp]

theorem CategoryTheory.SmallObject.attachCellsιFunctorObj_isColimit₂ {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] : (attachCellsιFunctorObj f πX).isColimit₂ = Limits.coproductIsCoproduct fun (i : FunctorObjIndex f πX) => B i.i

@[simp]

theorem CategoryTheory.SmallObject.attachCellsιFunctorObj_isColimit₁ {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] : (attachCellsιFunctorObj f πX).isColimit₁ = Limits.coproductIsCoproduct fun (i : FunctorObjIndex f πX) => A i.i

@[simp]

theorem CategoryTheory.SmallObject.attachCellsιFunctorObj_cofan₂ {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] : (attachCellsιFunctorObj f πX).cofan₂ = Limits.Cofan.mk (∐ fun (i : FunctorObjIndex f πX) => B i.i) (Limits.Sigma.ι fun (i : FunctorObjIndex f πX) => B i.i)

@[simp]

theorem CategoryTheory.SmallObject.attachCellsιFunctorObj_g₂ {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] : (attachCellsιFunctorObj f πX).g₂ = ρFunctorObj f πX

@[simp]

theorem CategoryTheory.SmallObject.attachCellsιFunctorObj_π {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] (x : FunctorObjIndex f πX) : (attachCellsιFunctorObj f πX).π x = x.i

@[simp]

theorem CategoryTheory.SmallObject.attachCellsιFunctorObj_m {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] : (attachCellsιFunctorObj f πX).m = functorObjLeft f πX

@[simp]

theorem CategoryTheory.SmallObject.attachCellsιFunctorObj_cofan₁ {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] : (attachCellsιFunctorObj f πX).cofan₁ = Limits.Cofan.mk (∐ fun (i : FunctorObjIndex f πX) => A i.i) (Limits.Sigma.ι fun (i : FunctorObjIndex f πX) => A i.i)

instance CategoryTheory.SmallObject.instSmallFunctorObjIndex {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [LocallySmall.{t, v, u} C] [Small.{t, w} I] : Small.{t, max v w} (FunctorObjIndex f πX)

instance CategoryTheory.SmallObject.instSmallιAttachCellsιFunctorObj {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] [LocallySmall.{t, v, u} C] [Small.{t, w} I] : Small.{t, max v w} (attachCellsιFunctorObj f πX).ι

noncomputable def CategoryTheory.SmallObject.attachCellsιFunctorObjOfSmall {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} (πX : X ⟶ S) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] [LocallySmall.{t, v, u} C] [Small.{t, w} I] : HomotopicalAlgebra.AttachCells f (ιFunctorObj f πX)

The morphism ιFunctorObj f πX : X ⟶ functorObj f πX is obtained by attaching f-cells, and the index type can be chosen to be in Type t if the category is t-locally small and the index type for f is t-small.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.SmallObject.functorMapSrc {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : Arrow.mk πX ⟶ Arrow.mk πY) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C] : ∐ functorObjSrcFamily f πX ⟶ ∐ functorObjSrcFamily f πY

The canonical morphism ∐ (functorObjSrcFamily f πX) ⟶ ∐ (functorObjSrcFamily f πY) induced by a morphism Arrow.mk πX ⟶ Arrow.mk πY.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.SmallObject.ι_functorMapSrc {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : Arrow.mk πX ⟶ Arrow.mk πY) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C] (i : I) (t : A i ⟶ X) (b : B i ⟶ S) (w : CategoryStruct.comp t πX = CategoryStruct.comp (f i) b) (b' : B i ⟶ T) (hb' : CategoryStruct.comp b τ.right = b') (t' : A i ⟶ Y) (ht' : CategoryStruct.comp t τ.left = t') : CategoryStruct.comp (Limits.Sigma.ι (functorObjSrcFamily f πX) { i := i, t := t, b := b, w := w }) (functorMapSrc f τ) = Limits.Sigma.ι (functorObjSrcFamily f πY) { i := i, t := t', b := b', w := ⋯ }

theorem CategoryTheory.SmallObject.ι_functorMapSrc_assoc {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : Arrow.mk πX ⟶ Arrow.mk πY) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C] (i : I) (t : A i ⟶ X) (b : B i ⟶ S) (w : CategoryStruct.comp t πX = CategoryStruct.comp (f i) b) (b' : B i ⟶ T) (hb' : CategoryStruct.comp b τ.right = b') (t' : A i ⟶ Y) (ht' : CategoryStruct.comp t τ.left = t') {Z : C} (h : ∐ functorObjSrcFamily f πY ⟶ Z) : CategoryStruct.comp (Limits.Sigma.ι (functorObjSrcFamily f πX) { i := i, t := t, b := b, w := w }) (CategoryStruct.comp (functorMapSrc f τ) h) = CategoryStruct.comp (Limits.Sigma.ι (functorObjSrcFamily f πY) { i := i, t := t', b := b', w := ⋯ }) h

@[simp]

theorem CategoryTheory.SmallObject.functorMapSrc_functorObjTop {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : Arrow.mk πX ⟶ Arrow.mk πY) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C] : CategoryStruct.comp (functorMapSrc f τ) (functorObjTop f πY) = CategoryStruct.comp (functorObjTop f πX) τ.left

@[simp]

theorem CategoryTheory.SmallObject.functorMapSrc_functorObjTop_assoc {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : Arrow.mk πX ⟶ Arrow.mk πY) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C] {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (functorMapSrc f τ) (CategoryStruct.comp (functorObjTop f πY) h) = CategoryStruct.comp (functorObjTop f πX) (CategoryStruct.comp τ.left h)

noncomputable def CategoryTheory.SmallObject.functorMapTgt {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : Arrow.mk πX ⟶ Arrow.mk πY) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C] : ∐ functorObjTgtFamily f πX ⟶ ∐ functorObjTgtFamily f πY

The canonical morphism ∐ functorObjTgtFamily f πX ⟶ ∐ functorObjTgtFamily f πY induced by a morphism Arrow.mk πX ⟶ Arrow.mk πY.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.SmallObject.ι_functorMapTgt {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : Arrow.mk πX ⟶ Arrow.mk πY) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C] (i : I) (t : A i ⟶ X) (b : B i ⟶ S) (w : CategoryStruct.comp t πX = CategoryStruct.comp (f i) b) (b' : B i ⟶ T) (hb' : CategoryStruct.comp b τ.right = b') (t' : A i ⟶ Y) (ht' : CategoryStruct.comp t τ.left = t') : CategoryStruct.comp (Limits.Sigma.ι (functorObjTgtFamily f πX) { i := i, t := t, b := b, w := w }) (functorMapTgt f τ) = Limits.Sigma.ι (functorObjTgtFamily f πY) { i := i, t := t', b := b', w := ⋯ }

theorem CategoryTheory.SmallObject.ι_functorMapTgt_assoc {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : Arrow.mk πX ⟶ Arrow.mk πY) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C] (i : I) (t : A i ⟶ X) (b : B i ⟶ S) (w : CategoryStruct.comp t πX = CategoryStruct.comp (f i) b) (b' : B i ⟶ T) (hb' : CategoryStruct.comp b τ.right = b') (t' : A i ⟶ Y) (ht' : CategoryStruct.comp t τ.left = t') {Z : C} (h : ∐ functorObjTgtFamily f πY ⟶ Z) : CategoryStruct.comp (Limits.Sigma.ι (functorObjTgtFamily f πX) { i := i, t := t, b := b, w := w }) (CategoryStruct.comp (functorMapTgt f τ) h) = CategoryStruct.comp (Limits.Sigma.ι (functorObjTgtFamily f πY) { i := i, t := t', b := b', w := ⋯ }) h

theorem CategoryTheory.SmallObject.functorMap_comm {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : Arrow.mk πX ⟶ Arrow.mk πY) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C] : CategoryStruct.comp (functorObjLeft f πX) (functorMapTgt f τ) = CategoryStruct.comp (functorMapSrc f τ) (functorObjLeft f πY)

noncomputable def CategoryTheory.SmallObject.functorMap {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : Arrow.mk πX ⟶ Arrow.mk πY) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C] [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] [Limits.HasPushout (functorObjTop f πY) (functorObjLeft f πY)] : functorObj f πX ⟶ functorObj f πY

The functor SmallObject.functor f S : Arrow S ⥤ Arrow S that is part of the small object argument for a family of morphisms f, on morphisms.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.SmallObject.functorMap_π {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : Arrow.mk πX ⟶ Arrow.mk πY) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C] [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] [Limits.HasPushout (functorObjTop f πY) (functorObjLeft f πY)] : CategoryStruct.comp (functorMap f τ) (πFunctorObj f πY) = CategoryStruct.comp (πFunctorObj f πX) τ.right

@[simp]

theorem CategoryTheory.SmallObject.functorMap_π_assoc {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : Arrow.mk πX ⟶ Arrow.mk πY) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C] [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] [Limits.HasPushout (functorObjTop f πY) (functorObjLeft f πY)] {Z : C} (h : T ⟶ Z) : CategoryStruct.comp (functorMap f τ) (CategoryStruct.comp (πFunctorObj f πY) h) = CategoryStruct.comp (πFunctorObj f πX) (CategoryStruct.comp τ.right h)

@[simp]

theorem CategoryTheory.SmallObject.functorMap_id {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S : C} (X : C) {πX : X ⟶ S} [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] : functorMap f (CategoryStruct.id (Arrow.mk πX)) = CategoryStruct.id (functorObj f πX)

@[simp]

theorem CategoryTheory.SmallObject.ιFunctorObj_naturality {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : Arrow.mk πX ⟶ Arrow.mk πY) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C] [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] [Limits.HasPushout (functorObjTop f πY) (functorObjLeft f πY)] : CategoryStruct.comp (ιFunctorObj f πX) (functorMap f τ) = CategoryStruct.comp τ.left (ιFunctorObj f πY)

@[simp]

theorem CategoryTheory.SmallObject.ιFunctorObj_naturality_assoc {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : Arrow.mk πX ⟶ Arrow.mk πY) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C] [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] [Limits.HasPushout (functorObjTop f πY) (functorObjLeft f πY)] {Z : C} (h : functorObj f πY ⟶ Z) : CategoryStruct.comp (ιFunctorObj f πX) (CategoryStruct.comp (functorMap f τ) h) = CategoryStruct.comp τ.left (CategoryStruct.comp (ιFunctorObj f πY) h)

theorem CategoryTheory.SmallObject.ιFunctorObj_extension {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} {πX : X ⟶ S} [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] {i : I} (t : A i ⟶ X) (b : B i ⟶ S) (sq : CommSq t (f i) πX b) : ∃ (l : B i ⟶ functorObj f πX), CategoryStruct.comp (f i) l = CategoryStruct.comp t (ιFunctorObj f πX) ∧ CategoryStruct.comp l (πFunctorObj f πX) = b

theorem CategoryTheory.SmallObject.ιFunctorObj_extension' {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C} {πX : X ⟶ S} [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] {X' S' Z' : C} (πX' : X' ⟶ S') (ι' : X' ⟶ Z') (πZ' : Z' ⟶ S') (fac' : CategoryStruct.comp ι' πZ' = πX') (eX : X' ≅ X) (eS : S' ≅ S) (eZ : Z' ≅ functorObj f πX) (commι : CategoryStruct.comp ι' eZ.hom = CategoryStruct.comp eX.hom (ιFunctorObj f πX)) (commπ : CategoryStruct.comp πZ' eS.hom = CategoryStruct.comp eZ.hom (πFunctorObj f πX)) {i : I} (t : A i ⟶ X') (b : B i ⟶ S') (fac : CategoryStruct.comp t πX' = CategoryStruct.comp (f i) b) : ∃ (l : B i ⟶ Z'), CategoryStruct.comp (f i) l = CategoryStruct.comp t ι' ∧ CategoryStruct.comp l πZ' = b

Variant of ιFunctorObj_extension where the diagram involving functorObj f πX is replaced by an isomorphic diagram.

noncomputable def CategoryTheory.SmallObject.functor {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) [Limits.HasPushouts C] [∀ {X S : C} (πX : X ⟶ S), Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] : Functor (Arrow C) (Arrow C)

The functor Arrow C ⥤ Arrow C that is constructed in order to apply the small object argument to a family of morphisms f i : A i ⟶ B i, see the introduction of the file Mathlib/CategoryTheory/SmallObject/Construction.lean

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.SmallObject.functor_map {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) [Limits.HasPushouts C] [∀ {X S : C} (πX : X ⟶ S), Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] {π₁ π₂ : Arrow C} (τ : π₁ ⟶ π₂) : (functor f).map τ = Arrow.homMk (functorMap f τ) τ.right ⋯

@[simp]

theorem CategoryTheory.SmallObject.functor_obj {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) [Limits.HasPushouts C] [∀ {X S : C} (πX : X ⟶ S), Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] (π : Arrow C) : (functor f).obj π = Arrow.mk (πFunctorObj f π.hom)

noncomputable def CategoryTheory.SmallObject.ε {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) [Limits.HasPushouts C] [∀ {X S : C} (πX : X ⟶ S), Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] : Functor.id (Arrow C) ⟶ functor f

The canonical natural transformation 𝟭 (Arrow C) ⟶ functor f.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.SmallObject.ε_app {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) [Limits.HasPushouts C] [∀ {X S : C} (πX : X ⟶ S), Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] (π : Arrow C) : (ε f).app π = Arrow.homMk (ιFunctorObj f π.hom) (CategoryStruct.id ((Functor.id (Arrow C)).obj π).right) ⋯