Construction for the small object argument

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

∐ functorObjSrcFamily f πX ⟶       X

            |                      |
            |                      |
            v                      v

∐ functorObjTgtFamily f πX ⟶ functorObj f S π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 S πX : X ⟶ functorObj f πX is part of a natural transformation SmallObject.ε f S : 𝟭 (Over S) ⟶ 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).

TODO

• Show that ιFunctorObj f πX : X ⟶ functorObj f πX has the left lifting property with respect to the class of morphisms that have the right lifting property with respect to the morphisms f i.

References

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

structure CategoryTheory.SmallObject.FunctorObjIndex {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A : I → C} {B : I → C} (f : (i : I) → A i ⟶ B i) {S : C} {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 : CategoryTheory.CategoryStruct.comp self.t πX = CategoryTheory.CategoryStruct.comp (f self.i) self.b

@[simp]

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

@[simp]

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

@[reducible, inline]

abbrev CategoryTheory.SmallObject.functorObjSrcFamily {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A : I → C} {B : I → C} (f : (i : I) → A i ⟶ B i) {S : C} {X : C} (πX : X ⟶ S) (x : CategoryTheory.SmallObject.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} [CategoryTheory.Category.{v, u} C] {I : Type w} {A : I → C} {B : I → C} (f : (i : I) → A i ⟶ B i) {S : C} {X : C} (πX : X ⟶ S) (x : CategoryTheory.SmallObject.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} [CategoryTheory.Category.{v, u} C] {I : Type w} {A : I → C} {B : I → C} (f : (i : I) → A i ⟶ B i) {S : C} {X : C} (πX : X ⟶ S) (x : CategoryTheory.SmallObject.FunctorObjIndex f πX) : CategoryTheory.SmallObject.functorObjSrcFamily f πX x ⟶ CategoryTheory.SmallObject.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} [CategoryTheory.Category.{v, u} C] {I : Type w} {A : I → C} {B : I → C} (f : (i : I) → A i ⟶ B i) {S : C} {X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] : ∐ CategoryTheory.SmallObject.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} [CategoryTheory.Category.{v, u} C] {I : Type w} {A : I → C} {B : I → C} (f : (i : I) → A i ⟶ B i) {S : C} {X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] : ∐ CategoryTheory.SmallObject.functorObjSrcFamily f πX ⟶ ∐ CategoryTheory.SmallObject.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} [CategoryTheory.Category.{v, u} C] {I : Type w} {A : I → C} {B : I → C} (f : (i : I) → A i ⟶ B i) {S : C} {X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] : C

The functor SmallObject.functor f S : Over S ⥤ Over S 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} [CategoryTheory.Category.{v, u} C] {I : Type w} {A : I → C} {B : I → C} (f : (i : I) → A i ⟶ B i) {S : C} {X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] : X ⟶ CategoryTheory.SmallObject.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} [CategoryTheory.Category.{v, u} C] {I : Type w} {A : I → C} {B : I → C} (f : (i : I) → A i ⟶ B i) {S : C} {X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] : ∐ CategoryTheory.SmallObject.functorObjTgtFamily f πX ⟶ CategoryTheory.SmallObject.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} [CategoryTheory.Category.{v, u} C] {I : Type w} {A : I → C} {B : I → C} (f : (i : I) → A i ⟶ B i) {S : C} {X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.ιFunctorObj f πX) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorObjLeft f πX) (CategoryTheory.SmallObject.ρFunctorObj f πX)

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

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

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

@[reducible, inline]

noncomputable abbrev CategoryTheory.SmallObject.π'FunctorObj {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A : I → C} {B : I → C} (f : (i : I) → A i ⟶ B i) {S : C} {X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] : ∐ CategoryTheory.SmallObject.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} [CategoryTheory.Category.{v, u} C] {I : Type w} {A : I → C} {B : I → C} (f : (i : I) → A i ⟶ B i) {S : C} {X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] : CategoryTheory.SmallObject.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} [CategoryTheory.Category.{v, u} C] {I : Type w} {A : I → C} {B : I → C} (f : (i : I) → A i ⟶ B i) {S : C} {X : C} (πX : X ⟶ S) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.ρFunctorObj f πX) (CategoryTheory.SmallObject.πFunctorObj f πX) = CategoryTheory.SmallObject.π'FunctorObj f πX

@[simp]

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

@[simp]

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

@[simp]

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

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

The canonical morphism ∐ (functorObjSrcFamily f πX) ⟶ ∐ (functorObjSrcFamily f πY) induced by a morphism in φ : X ⟶ Y such that φ ≫ πX = πY.

Equations

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

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

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

@[simp]

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

@[simp]

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

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

The canonical morphism ∐ functorObjTgtFamily f πX ⟶ ∐ functorObjTgtFamily f πY induced by a morphism in φ : X ⟶ Y such that φ ≫ πX = πY.

Equations

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

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

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

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

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

The functor SmallObject.functor f S : Over S ⥤ Over 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} [CategoryTheory.Category.{v, u} C] {I : Type w} {A : I → C} {B : I → C} (f : (i : I) → A i ⟶ B i) {S : C} {X : C} {Y : C} (πX : X ⟶ S) (πY : Y ⟶ S) (φ : X ⟶ Y) [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY)) C] (hφ : CategoryTheory.CategoryStruct.comp φ πY = πX) [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX) (CategoryTheory.SmallObject.functorObjLeft f πX)] [CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πY) (CategoryTheory.SmallObject.functorObjLeft f πY)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorMap f πX πY φ hφ) (CategoryTheory.SmallObject.πFunctorObj f πY) = CategoryTheory.SmallObject.πFunctorObj f πX

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

The functor Over S ⥤ Over S 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

Equations

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

@[simp]

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

@[simp]

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

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

The canonical natural transformation 𝟭 (Over S) ⟶ functor f S.

Equations

• CategoryTheory.SmallObject.ε f S = { app := fun (w : CategoryTheory.Over S) => CategoryTheory.Over.homMk (CategoryTheory.SmallObject.ιFunctorObj f w.hom) ⋯, naturality := ⋯ }

@[simp]

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