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} [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 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} [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.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.functorMapSrc {C : Type u} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X Y : C} (πX : X ⟶ S) (πY : Y ⟶ S) (φ : X ⟶ Y) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C] (hφ : CategoryStruct.comp φ πY = πX) : ∐ functorObjSrcFamily f πX ⟶ ∐ 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} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X Y : C} (πX : X ⟶ S) (πY : Y ⟶ S) (φ : X ⟶ Y) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C] (hφ : CategoryStruct.comp φ πY = πX) (i : I) (t : A i ⟶ X) (b : B i ⟶ S) (w : CategoryStruct.comp t πX = CategoryStruct.comp (f i) b) (t' : A i ⟶ Y) (fac : CategoryStruct.comp t φ = t') : CategoryStruct.comp (Limits.Sigma.ι (functorObjSrcFamily f πX) { i := i, t := t, b := b, w := w }) (functorMapSrc f πX πY φ hφ) = 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 X Y : C} (πX : X ⟶ S) (πY : Y ⟶ S) (φ : X ⟶ Y) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C] (hφ : CategoryStruct.comp φ πY = πX) (i : I) (t : A i ⟶ X) (b : B i ⟶ S) (w : CategoryStruct.comp t πX = CategoryStruct.comp (f i) b) (t' : A i ⟶ Y) (fac : CategoryStruct.comp t φ = 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 πX πY φ hφ) 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 X Y : C} (πX : X ⟶ S) (πY : Y ⟶ S) (φ : X ⟶ Y) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C] (hφ : CategoryStruct.comp φ πY = πX) : CategoryStruct.comp (functorMapSrc f πX πY φ hφ) (functorObjTop f πY) = CategoryStruct.comp (functorObjTop f πX) φ

@[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 X Y : C} (πX : X ⟶ S) (πY : Y ⟶ S) (φ : X ⟶ Y) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C] (hφ : CategoryStruct.comp φ πY = πX) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (functorMapSrc f πX πY φ hφ) (CategoryStruct.comp (functorObjTop f πY) h) = CategoryStruct.comp (functorObjTop f πX) (CategoryStruct.comp φ 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 X Y : C} (πX : X ⟶ S) (πY : Y ⟶ S) (φ : X ⟶ Y) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C] (hφ : CategoryStruct.comp φ πY = πX) : ∐ functorObjTgtFamily f πX ⟶ ∐ 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} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X Y : C} (πX : X ⟶ S) (πY : Y ⟶ S) (φ : X ⟶ Y) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C] (hφ : CategoryStruct.comp φ πY = πX) (i : I) (t : A i ⟶ X) (b : B i ⟶ S) (w : CategoryStruct.comp t πX = CategoryStruct.comp (f i) b) (t' : A i ⟶ Y) (fac : CategoryStruct.comp t φ = t') : CategoryStruct.comp (Limits.Sigma.ι (functorObjTgtFamily f πX) { i := i, t := t, b := b, w := w }) (functorMapTgt f πX πY φ hφ) = 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 X Y : C} (πX : X ⟶ S) (πY : Y ⟶ S) (φ : X ⟶ Y) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C] (hφ : CategoryStruct.comp φ πY = πX) (i : I) (t : A i ⟶ X) (b : B i ⟶ S) (w : CategoryStruct.comp t πX = CategoryStruct.comp (f i) b) (t' : A i ⟶ Y) (fac : CategoryStruct.comp t φ = 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 πX πY φ hφ) 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 X Y : C} (πX : X ⟶ S) (πY : Y ⟶ S) (φ : X ⟶ Y) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C] (hφ : CategoryStruct.comp φ πY = πX) : CategoryStruct.comp (functorObjLeft f πX) (functorMapTgt f πX πY φ hφ) = CategoryStruct.comp (functorMapSrc f πX πY φ hφ) (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 X Y : C} (πX : X ⟶ S) (πY : Y ⟶ S) (φ : X ⟶ Y) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C] (hφ : CategoryStruct.comp φ πY = πX) [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 : 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} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X Y : C} (πX : X ⟶ S) (πY : Y ⟶ S) (φ : X ⟶ Y) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C] (hφ : CategoryStruct.comp φ πY = πX) [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] [Limits.HasPushout (functorObjTop f πY) (functorObjLeft f πY)] : CategoryStruct.comp (functorMap f πX πY φ hφ) (πFunctorObj f πY) = πFunctorObj f πX

@[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 X Y : C} (πX : X ⟶ S) (πY : Y ⟶ S) (φ : X ⟶ Y) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C] (hφ : CategoryStruct.comp φ πY = πX) [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] [Limits.HasPushout (functorObjTop f πY) (functorObjLeft f πY)] {Z : C} (h : S ⟶ Z) : CategoryStruct.comp (functorMap f πX πY φ hφ) (CategoryStruct.comp (πFunctorObj f πY) h) = CategoryStruct.comp (πFunctorObj f πX) 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 πX πX (CategoryStruct.id 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 X Y : C} (πX : X ⟶ S) (πY : Y ⟶ S) (φ : X ⟶ Y) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C] (hφ : CategoryStruct.comp φ πY = πX) [Limits.HasPushout (functorObjTop f πX) (functorObjLeft f πX)] [Limits.HasPushout (functorObjTop f πY) (functorObjLeft f πY)] : CategoryStruct.comp (ιFunctorObj f πX) (functorMap f πX πY φ hφ) = CategoryStruct.comp φ (ι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 X Y : C} (πX : X ⟶ S) (πY : Y ⟶ S) (φ : X ⟶ Y) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C] (hφ : CategoryStruct.comp φ πY = πX) [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 πX πY φ hφ) h) = CategoryStruct.comp φ (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

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) (S : C) [Limits.HasPushouts C] [∀ {X : C} (πX : X ⟶ S), Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] : Functor (Over S) (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} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) (S : C) [Limits.HasPushouts C] [∀ {X : C} (πX : X ⟶ S), Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] {π₁ π₂ : Over S} (φ : π₁ ⟶ π₂) : (functor f S).map φ = Over.homMk (functorMap f π₁.hom π₂.hom φ.left ⋯) ⋯

@[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) (S : C) [Limits.HasPushouts C] [∀ {X : C} (πX : X ⟶ S), Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] (π : Over S) : (functor f S).obj π = Over.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) (S : C) [Limits.HasPushouts C] [∀ {X : C} (πX : X ⟶ S), Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] : Functor.id (Over S) ⟶ 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} [Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) (S : C) [Limits.HasPushouts C] [∀ {X : C} (πX : X ⟶ S), Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] (w : Over S) : (ε f S).app w = Over.homMk (ιFunctorObj f w.hom) ⋯