Limit properties relating to the (co)yoneda embedding. #
We calculate the colimit of Y ↦ (X ⟶ Y)
, which is just PUnit
.
(This is used in characterising cofinal functors.)
We also show the (co)yoneda embeddings preserve limits and jointly reflect them.
@[simp]
theorem
CategoryTheory.Coyoneda.colimitCocone_ι_app
{C : Type v}
[CategoryTheory.SmallCategory C]
(X : Cᵒᵖ)
(X_1 : C)
(a : (CategoryTheory.coyoneda.obj X).obj X_1)
:
(CategoryTheory.Coyoneda.colimitCocone X).ι.app X_1 a = id PUnit.unit
@[simp]
theorem
CategoryTheory.Coyoneda.colimitCocone_pt
{C : Type v}
[CategoryTheory.SmallCategory C]
(X : Cᵒᵖ)
:
def
CategoryTheory.Coyoneda.colimitCocone
{C : Type v}
[CategoryTheory.SmallCategory C]
(X : Cᵒᵖ)
:
CategoryTheory.Limits.Cocone (CategoryTheory.coyoneda.obj X)
The colimit cocone over coyoneda.obj X
, with cocone point PUnit
.
Instances For
@[simp]
theorem
CategoryTheory.Coyoneda.colimitCoconeIsColimit_desc
{C : Type v}
[CategoryTheory.SmallCategory C]
(X : Cᵒᵖ)
(s : CategoryTheory.Limits.Cocone (CategoryTheory.coyoneda.obj X))
:
∀ (x : (CategoryTheory.Coyoneda.colimitCocone X).pt),
CategoryTheory.Limits.IsColimit.desc C inst✝ (Type v) CategoryTheory.types (CategoryTheory.coyoneda.obj X)
(CategoryTheory.Coyoneda.colimitCocone X) (CategoryTheory.Coyoneda.colimitCoconeIsColimit X) s x = C.app inst✝ (Type v) CategoryTheory.types (CategoryTheory.coyoneda.obj X)
((CategoryTheory.Functor.const C).obj s.pt) s.ι X.unop (CategoryTheory.CategoryStruct.id X.unop)
def
CategoryTheory.Coyoneda.colimitCoconeIsColimit
{C : Type v}
[CategoryTheory.SmallCategory C]
(X : Cᵒᵖ)
:
The proposed colimit cocone over coyoneda.obj X
is a colimit cocone.
Instances For
instance
CategoryTheory.Coyoneda.instHasColimitTypeTypesObjOppositeToQuiverToCategoryStructOppositeFunctorToQuiverToCategoryStructCategoryToPrefunctorCoyoneda
{C : Type v}
[CategoryTheory.SmallCategory C]
(X : Cᵒᵖ)
:
CategoryTheory.Limits.HasColimit (CategoryTheory.coyoneda.obj X)
noncomputable def
CategoryTheory.Coyoneda.colimitCoyonedaIso
{C : Type v}
[CategoryTheory.SmallCategory C]
(X : Cᵒᵖ)
:
CategoryTheory.Limits.colimit (CategoryTheory.coyoneda.obj X) ≅ PUnit.{v + 1}
The colimit of coyoneda.obj X
is isomorphic to PUnit
.
Instances For
instance
CategoryTheory.yonedaPreservesLimits
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(X : C)
:
CategoryTheory.Limits.PreservesLimits (CategoryTheory.yoneda.obj X)
The yoneda embedding yoneda.obj X : Cᵒᵖ ⥤ Type v
for X : C
preserves limits.
instance
CategoryTheory.coyonedaPreservesLimits
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(X : Cᵒᵖ)
:
CategoryTheory.Limits.PreservesLimits (CategoryTheory.coyoneda.obj X)
The coyoneda embedding coyoneda.obj X : C ⥤ Type v
for X : Cᵒᵖ
preserves limits.
def
CategoryTheory.yonedaJointlyReflectsLimits
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : Type w)
[CategoryTheory.SmallCategory J]
(K : CategoryTheory.Functor J Cᵒᵖ)
(c : CategoryTheory.Limits.Cone K)
(t : (X : C) → CategoryTheory.Limits.IsLimit ((CategoryTheory.yoneda.obj X).mapCone c))
:
The yoneda embeddings jointly reflect limits.
Instances For
def
CategoryTheory.coyonedaJointlyReflectsLimits
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : Type w)
[CategoryTheory.SmallCategory J]
(K : CategoryTheory.Functor J C)
(c : CategoryTheory.Limits.Cone K)
(t : (X : Cᵒᵖ) → CategoryTheory.Limits.IsLimit ((CategoryTheory.coyoneda.obj X).mapCone c))
:
The coyoneda embeddings jointly reflect limits.
Instances For
instance
CategoryTheory.yonedaFunctorPreservesLimits
{D : Type u}
[CategoryTheory.SmallCategory D]
:
CategoryTheory.Limits.PreservesLimits CategoryTheory.yoneda
instance
CategoryTheory.coyonedaFunctorPreservesLimits
{D : Type u}
[CategoryTheory.SmallCategory D]
:
CategoryTheory.Limits.PreservesLimits CategoryTheory.coyoneda
instance
CategoryTheory.yonedaFunctorReflectsLimits
{D : Type u}
[CategoryTheory.SmallCategory D]
:
CategoryTheory.Limits.ReflectsLimits CategoryTheory.yoneda
instance
CategoryTheory.coyonedaFunctorReflectsLimits
{D : Type u}
[CategoryTheory.SmallCategory D]
:
CategoryTheory.Limits.ReflectsLimits CategoryTheory.coyoneda