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.
The colimit cocone over coyoneda.obj X
, with cocone point PUnit
.
Equations
- Eq (CategoryTheory.Coyoneda.colimitCocone X) { pt := PUnit, ι := { app := fun (X_1 : C) (a : (CategoryTheory.coyoneda.obj X).obj X_1) => id PUnit.unit, naturality := ⋯ } }
Instances For
The proposed colimit cocone over coyoneda.obj X
is a colimit cocone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The cone of F
corresponding to an element in (F ⋙ yoneda.obj X).sections
.
Equations
- Eq (CategoryTheory.Limits.coneOfSectionCompYoneda F X s) { pt := { unop := X }, π := DFunLike.coe (CategoryTheory.Limits.compYonedaSectionsEquiv F X) s }
Instances For
The yoneda embeddings jointly reflect limits.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A cocone is colimit iff it becomes limit after the
application of yoneda.obj X
for all X : C
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The cone of F
corresponding to an element in (F ⋙ coyoneda.obj X).sections
.
Equations
- Eq (CategoryTheory.Limits.coneOfSectionCompCoyoneda F X s) { pt := Opposite.unop X, π := DFunLike.coe (CategoryTheory.Limits.compCoyonedaSectionsEquiv F (Opposite.unop X)) s }
Instances For
The coyoneda embeddings jointly reflect limits.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A cone is limit iff it is so after the application of coyoneda.obj X
for all X : Cᵒᵖ
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The yoneda embedding yoneda.obj X : Cᵒᵖ ⥤ Type v
for X : C
preserves limits.
The coyoneda embedding coyoneda.obj X : C ⥤ Type v
for X : Cᵒᵖ
preserves limits.