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
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
the top morphism in the square
the bottom morphism in the square
Instances For
The family of objects A x.i
parametrized by x : FunctorObjIndex f πX
.
Equations
- CategoryTheory.SmallObject.functorObjSrcFamily f πX x = A x.i
Instances For
The family of objects B x.i
parametrized by x : FunctorObjIndex f πX
.
Equations
- CategoryTheory.SmallObject.functorObjTgtFamily f πX x = B x.i
Instances For
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
Instances For
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
Instances For
The left morphism in the pushout square in the definition of pushoutObj f πX
.
Equations
Instances For
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
The canonical morphism X ⟶ functorObj f πX
.
Equations
Instances For
The canonical morphism ∐ (functorObjTgtFamily f πX) ⟶ functorObj f πX
.
Equations
Instances For
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
Instances For
The canonical projection on the base object.
Equations
Instances For
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
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
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
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
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
Variant of ιFunctorObj_extension
where the diagram involving functorObj f πX
is replaced by an isomorphic diagram.
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
The canonical natural transformation 𝟭 (Arrow C) ⟶ functor f
.
Equations
- One or more equations did not get rendered due to their size.