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

TODO #

References #

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

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

        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]

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

          Equations
          Instances For
            @[reducible, inline]

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

            Equations
            Instances For
              @[reducible, inline]

              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
              Instances For
                @[reducible, inline]

                The canonical projection on the base object.

                Equations
                Instances For

                  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.
                  Instances For

                    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.
                    Instances For

                      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.
                      Instances For
                        @[simp]
                        theorem CategoryTheory.SmallObject.functor_map {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {A : IC} {B : IC} (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} (φ : π₁ π₂) :

                        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.
                        Instances For

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

                          Equations
                          Instances For