Documentation

Mathlib.CategoryTheory.SmallObject.Construction

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 ifunctorObj f πX (see SmallObject.ιFunctorObj_extension).

References #

structure CategoryTheory.SmallObject.FunctorObjIndex {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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.

Instances For
    @[simp]
    theorem CategoryTheory.SmallObject.FunctorObjIndex.w_assoc {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} {f : (i : I) → A i B i} {S X : C} {πX : X S} (self : FunctorObjIndex f πX) {Z : C} (h : S Z) :
    @[reducible, inline]
    abbrev CategoryTheory.SmallObject.functorObjSrcFamily {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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
    Instances For
      @[reducible, inline]
      abbrev CategoryTheory.SmallObject.functorObjTgtFamily {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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
      Instances For
        @[reducible, inline]
        abbrev CategoryTheory.SmallObject.functorObjLeftFamily {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (f : (i : I) → A i B i) {S X : C} (πX : X S) (x : FunctorObjIndex f πX) :

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

        Equations
        Instances For
          @[reducible, inline]
          noncomputable abbrev CategoryTheory.SmallObject.functorObjTop {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (f : (i : I) → A i B i) {S X : C} (πX : X S) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] :

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

          Equations
          Instances For
            @[reducible, inline]
            noncomputable abbrev CategoryTheory.SmallObject.functorObjLeft {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (f : (i : I) → A i B i) {S X : C} (πX : X S) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] :

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

            Equations
            Instances For
              @[reducible, inline]
              noncomputable abbrev CategoryTheory.SmallObject.functorObj {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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
              Instances For
                @[reducible, inline]
                noncomputable abbrev CategoryTheory.SmallObject.ιFunctorObj {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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
                Instances For
                  @[reducible, inline]
                  noncomputable abbrev CategoryTheory.SmallObject.ρFunctorObj {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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)] :

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

                  Equations
                  Instances For
                    theorem CategoryTheory.SmallObject.functorObj_comm {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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)] :
                    theorem CategoryTheory.SmallObject.functorObj_isPushout {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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)] :
                    @[reducible, inline]
                    noncomputable abbrev CategoryTheory.SmallObject.π'FunctorObj {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (f : (i : I) → A i B i) {S X : C} (πX : X S) [Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] :

                    The canonical projection on the base object.

                    Equations
                    Instances For
                      noncomputable def CategoryTheory.SmallObject.πFunctorObj {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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
                      Instances For
                        @[simp]
                        theorem CategoryTheory.SmallObject.ρFunctorObj_π {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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)] :
                        @[simp]
                        theorem CategoryTheory.SmallObject.ρFunctorObj_π_assoc {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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) :
                        @[simp]
                        theorem CategoryTheory.SmallObject.ιFunctorObj_πFunctorObj {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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)] :
                        @[simp]
                        theorem CategoryTheory.SmallObject.ιFunctorObj_πFunctorObj_assoc {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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) :
                        noncomputable def CategoryTheory.SmallObject.attachCellsιFunctorObj {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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)] :

                        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.
                        Instances For
                          @[simp]
                          theorem CategoryTheory.SmallObject.attachCellsιFunctorObj_ι {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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)] :
                          @[simp]
                          theorem CategoryTheory.SmallObject.attachCellsιFunctorObj_g₁ {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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)] :
                          @[simp]
                          theorem CategoryTheory.SmallObject.attachCellsιFunctorObj_isColimit₂ {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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)] :
                          @[simp]
                          theorem CategoryTheory.SmallObject.attachCellsιFunctorObj_isColimit₁ {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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)] :
                          @[simp]
                          theorem CategoryTheory.SmallObject.attachCellsιFunctorObj_cofan₂ {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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 ((fun (x : FunctorObjIndex f πX) => x.i) i)) (Limits.Sigma.ι fun (i : FunctorObjIndex f πX) => B ((fun (x : FunctorObjIndex f πX) => x.i) i))
                          @[simp]
                          theorem CategoryTheory.SmallObject.attachCellsιFunctorObj_g₂ {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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)] :
                          @[simp]
                          theorem CategoryTheory.SmallObject.attachCellsιFunctorObj_π {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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) :
                          @[simp]
                          theorem CategoryTheory.SmallObject.attachCellsιFunctorObj_m {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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)] :
                          @[simp]
                          theorem CategoryTheory.SmallObject.attachCellsιFunctorObj_cofan₁ {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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 ((fun (x : FunctorObjIndex f πX) => x.i) i)) (Limits.Sigma.ι fun (i : FunctorObjIndex f πX) => A ((fun (x : FunctorObjIndex f πX) => x.i) i))
                          instance CategoryTheory.SmallObject.instSmallFunctorObjIndex {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (f : (i : I) → A i B i) {S X : C} (πX : X S) [LocallySmall.{t, v, u} C] [Small.{t, w} I] :

                          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.
                          Instances For
                            noncomputable def CategoryTheory.SmallObject.functorMapSrc {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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] :

                            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.
                            Instances For
                              theorem CategoryTheory.SmallObject.ι_functorMapSrc {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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 : IC} (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 : IC} (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] :
                              @[simp]
                              theorem CategoryTheory.SmallObject.functorMapSrc_functorObjTop_assoc {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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) :
                              noncomputable def CategoryTheory.SmallObject.functorMapTgt {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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] :

                              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.
                              Instances For
                                theorem CategoryTheory.SmallObject.ι_functorMapTgt {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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 : IC} (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 : IC} (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] :
                                noncomputable def CategoryTheory.SmallObject.functorMap {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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)] :

                                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.
                                Instances For
                                  @[simp]
                                  theorem CategoryTheory.SmallObject.functorMap_π {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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)] :
                                  @[simp]
                                  theorem CategoryTheory.SmallObject.functorMap_π_assoc {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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) :
                                  @[simp]
                                  theorem CategoryTheory.SmallObject.functorMap_id {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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)] :
                                  @[simp]
                                  theorem CategoryTheory.SmallObject.ιFunctorObj_naturality {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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)] :
                                  @[simp]
                                  theorem CategoryTheory.SmallObject.ιFunctorObj_extension {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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) :
                                  theorem CategoryTheory.SmallObject.ιFunctorObj_extension' {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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 : IC} (f : (i : I) → A i B i) [Limits.HasPushouts C] [∀ {X S : C} (πX : X S), Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) 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

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    @[simp]
                                    theorem CategoryTheory.SmallObject.functor_map {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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 : IC} (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) :
                                    noncomputable def CategoryTheory.SmallObject.ε {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (f : (i : I) → A i B i) [Limits.HasPushouts C] [∀ {X S : C} (πX : X S), Limits.HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C] :

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

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      @[simp]
                                      theorem CategoryTheory.SmallObject.ε_app {C : Type u} [Category.{v, u} C] {I : Type w} {A B : IC} (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) :