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 πXhas the left lifting property with respect to the class of morphisms that have the right lifting property with respect to the morphismsf 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
Instances For
@[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
Instances For
@[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
Instances For
@[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)
:
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
@[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]
:
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
@[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]
:
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}
[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
Instances For
@[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)]
:
The canonical morphism X ⟶ functorObj f πX.
Equations
- CategoryTheory.SmallObject.ιFunctorObj f πX = CategoryTheory.Limits.pushout.inl
Instances For
@[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)]
:
The canonical morphism ∐ (functorObjTgtFamily f πX) ⟶ functorObj f πX.
Equations
- CategoryTheory.SmallObject.ρFunctorObj f πX = CategoryTheory.Limits.pushout.inr
Instances For
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.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)]
:
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)
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)
@[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]
:
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
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)]
:
The canonical projection on the base object.
Equations
Instances For
@[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)
:
@[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)]
:
@[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)
:
@[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)]
:
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)
(hφ : CategoryTheory.CategoryStruct.comp φ πY = πX)
[CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C]
[CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY)) C]
:
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
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)
(hφ : CategoryTheory.CategoryStruct.comp φ πY = πX)
[CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C]
[CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY)) C]
(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
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)
(hφ : CategoryTheory.CategoryStruct.comp φ πY = πX)
[CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C]
[CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY)) C]
(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 := ⋯ }
@[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)
(hφ : CategoryTheory.CategoryStruct.comp φ πY = πX)
[CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C]
[CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY)) C]
{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)
@[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)
(hφ : CategoryTheory.CategoryStruct.comp φ πY = πX)
[CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C]
[CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY)) C]
:
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)
(hφ : CategoryTheory.CategoryStruct.comp φ πY = πX)
[CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C]
[CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY)) C]
:
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
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)
(hφ : CategoryTheory.CategoryStruct.comp φ πY = πX)
[CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C]
[CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY)) C]
(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.ι_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)
(hφ : CategoryTheory.CategoryStruct.comp φ πY = πX)
[CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C]
[CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY)) C]
(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.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)
(hφ : CategoryTheory.CategoryStruct.comp φ πY = πX)
[CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C]
[CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY)) C]
:
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)
(hφ : CategoryTheory.CategoryStruct.comp φ πY = πX)
[CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C]
[CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY)) C]
[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)]
:
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.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)
(hφ : CategoryTheory.CategoryStruct.comp φ πY = πX)
[CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C]
[CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY)) C]
[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)
:
@[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)
(hφ : CategoryTheory.CategoryStruct.comp φ πY = πX)
[CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C]
[CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY)) C]
[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)]
:
@[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)]
:
@[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)
(hφ : CategoryTheory.CategoryStruct.comp φ πY = πX)
[CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C]
[CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY)) C]
[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)
:
@[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)
(hφ : CategoryTheory.CategoryStruct.comp φ πY = πX)
[CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C]
[CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY)) C]
[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)]
:
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
@[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.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]
:
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
@[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) ⋯
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]
:
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 := ⋯ }