# 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 u} (X : Cᵒᵖ) (X_1 : C) (a : (CategoryTheory.coyoneda.obj X).obj X_1) :
.app X_1 a =
def CategoryTheory.Coyoneda.colimitCocone {C : Type u} (X : Cᵒᵖ) :
CategoryTheory.Limits.Cocone (CategoryTheory.coyoneda.obj X)

The colimit cocone over coyoneda.obj X, with cocone point PUnit.

Equations
• = { pt := PUnit.{?u.30 + 1} , ι := { app := fun (X_1 : C) (a : (CategoryTheory.coyoneda.obj X).obj X_1) => , naturality := } }
Instances For
@[simp]
theorem CategoryTheory.Coyoneda.colimitCoconeIsColimit_desc {C : Type u} (X : Cᵒᵖ) (s : CategoryTheory.Limits.Cocone (CategoryTheory.coyoneda.obj X)) :
∀ (x : ), = s.app

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
noncomputable def CategoryTheory.Coyoneda.colimitCoyonedaIso {C : Type u} (X : Cᵒᵖ) :
CategoryTheory.Limits.colimit (CategoryTheory.coyoneda.obj X) PUnit.{v + 1}

The colimit of coyoneda.obj X is isomorphic to PUnit.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.coneOfSectionCompYoneda_π {C : Type u} {J : Type w} (F : ) (X : C) (s : (F.comp (CategoryTheory.yoneda.obj X)).sections) :
@[simp]
theorem CategoryTheory.Limits.coneOfSectionCompYoneda_pt {C : Type u} {J : Type w} (F : ) (X : C) (s : (F.comp (CategoryTheory.yoneda.obj X)).sections) :
def CategoryTheory.Limits.coneOfSectionCompYoneda {C : Type u} {J : Type w} (F : ) (X : C) (s : (F.comp (CategoryTheory.yoneda.obj X)).sections) :

The cone of F corresponding to an element in (F ⋙ yoneda.obj X).sections.

Equations
• = { pt := , π := }
Instances For
noncomputable instance CategoryTheory.yonedaPreservesLimit {C : Type u} {J : Type w} (F : ) (X : C) :
CategoryTheory.Limits.PreservesLimit F (CategoryTheory.yoneda.obj X)
Equations
• = { preserves := fun {c : } (hc : ) => .some }
noncomputable instance CategoryTheory.yonedaPreservesLimitsOfShape {C : Type u} (J : Type w) (X : C) :
CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.yoneda.obj X)
Equations
• = { preservesLimit := fun {K : } => inferInstance }
def CategoryTheory.yonedaJointlyReflectsLimits {C : Type u} {J : Type w} (F : ) (c : ) (hc : (X : C) → CategoryTheory.Limits.IsLimit ((CategoryTheory.yoneda.obj X).mapCone c)) :

The yoneda embeddings jointly reflect limits.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def CategoryTheory.Limits.Cocone.isColimitYonedaEquiv {C : Type u} {J : Type w} {F : } (c : ) :
((X : C) → CategoryTheory.Limits.IsLimit ((CategoryTheory.yoneda.obj X).mapCone c.op))

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
@[simp]
theorem CategoryTheory.Limits.coneOfSectionCompCoyoneda_π {C : Type u} {J : Type w} (F : ) (X : Cᵒᵖ) (s : (F.comp (CategoryTheory.coyoneda.obj X)).sections) :
@[simp]
theorem CategoryTheory.Limits.coneOfSectionCompCoyoneda_pt {C : Type u} {J : Type w} (F : ) (X : Cᵒᵖ) (s : (F.comp (CategoryTheory.coyoneda.obj X)).sections) :
def CategoryTheory.Limits.coneOfSectionCompCoyoneda {C : Type u} {J : Type w} (F : ) (X : Cᵒᵖ) (s : (F.comp (CategoryTheory.coyoneda.obj X)).sections) :

The cone of F corresponding to an element in (F ⋙ coyoneda.obj X).sections.

Equations
• = { pt := , π := }
Instances For
noncomputable instance CategoryTheory.coyonedaPreservesLimit {C : Type u} {J : Type w} (F : ) (X : Cᵒᵖ) :
CategoryTheory.Limits.PreservesLimit F (CategoryTheory.coyoneda.obj X)
Equations
• = { preserves := fun {c : } (hc : ) => .some }
noncomputable instance CategoryTheory.coyonedaPreservesLimitsOfShape {C : Type u} (J : Type w) (X : Cᵒᵖ) :
CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.coyoneda.obj X)
Equations
• = { preservesLimit := fun {K : } => inferInstance }
def CategoryTheory.coyonedaJointlyReflectsLimits {C : Type u} {J : Type w} (F : ) (c : ) (hc : (X : Cᵒᵖ) → CategoryTheory.Limits.IsLimit ((CategoryTheory.coyoneda.obj X).mapCone c)) :

The coyoneda embeddings jointly reflect limits.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def CategoryTheory.Limits.Cone.isLimitCoyonedaEquiv {C : Type u} {J : Type w} {F : } (c : ) :
((X : Cᵒᵖ) → CategoryTheory.Limits.IsLimit ((CategoryTheory.coyoneda.obj X).mapCone c))

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
noncomputable instance CategoryTheory.yonedaPreservesLimits {C : Type u} (X : C) :

The yoneda embedding yoneda.obj X : Cᵒᵖ ⥤ Type v for X : C preserves limits.

Equations
• = { preservesLimitsOfShape := fun {J : Type ?u.26} [] => inferInstance }

The coyoneda embedding coyoneda.obj X : C ⥤ Type v for X : Cᵒᵖ preserves limits.

Equations
• = { preservesLimitsOfShape := fun {J : Type ?u.26} [] => inferInstance }
Equations
Equations
Equations
• CategoryTheory.yonedaFunctorReflectsLimits = inferInstance
Equations
• CategoryTheory.coyonedaFunctorReflectsLimits = inferInstance
noncomputable instance CategoryTheory.Functor.representablePreservesLimit {C : Type u} (F : ) [F.Representable] {J : Type u_1} [] (G : ) :
Equations
• F.representablePreservesLimit G =
noncomputable instance CategoryTheory.Functor.representablePreservesLimitsOfShape {C : Type u} (F : ) [F.Representable] (J : Type u_1) [] :
Equations
• F.representablePreservesLimitsOfShape J = { preservesLimit := fun {K : } => inferInstance }
noncomputable instance CategoryTheory.Functor.representablePreservesLimits {C : Type u} (F : ) [F.Representable] :
Equations
• F.representablePreservesLimits = { preservesLimitsOfShape := fun {J : Type ?u.36} [] => inferInstance }
noncomputable instance CategoryTheory.Functor.corepresentablePreservesLimit {C : Type u} (F : ) [F.Corepresentable] {J : Type u_1} [] (G : ) :
Equations
• F.corepresentablePreservesLimit G =
noncomputable instance CategoryTheory.Functor.corepresentablePreservesLimitsOfShape {C : Type u} (F : ) [F.Corepresentable] (J : Type u_1) [] :
Equations
• F.corepresentablePreservesLimitsOfShape J = { preservesLimit := fun {K : } => inferInstance }
noncomputable instance CategoryTheory.Functor.corepresentablePreservesLimits {C : Type u} (F : ) [F.Corepresentable] :
Equations
• F.corepresentablePreservesLimits = { preservesLimitsOfShape := fun {J : Type ?u.36} [] => inferInstance }