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} [CategoryTheory.Category.{v, u} 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 u} [CategoryTheory.Category.{v, u} C] (X : Cᵒᵖ) : (CategoryTheory.Coyoneda.colimitCocone X).pt = PUnit.{v + 1}

def CategoryTheory.Coyoneda.colimitCocone {C : Type u} [CategoryTheory.Category.{v, u} C] (X : Cᵒᵖ) : CategoryTheory.Limits.Cocone (CategoryTheory.coyoneda.obj X)

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

Equations

• CategoryTheory.Coyoneda.colimitCocone X = { pt := PUnit.{v + 1} , ι := { app := fun (X_1 : C) (a : (CategoryTheory.coyoneda.obj X).obj X_1) => id PUnit.unit, naturality := ⋯ } }

@[simp]

theorem CategoryTheory.Coyoneda.colimitCoconeIsColimit_desc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : Cᵒᵖ) (s : CategoryTheory.Limits.Cocone (CategoryTheory.coyoneda.obj X)) : ∀ (x : (CategoryTheory.Coyoneda.colimitCocone X).pt), (CategoryTheory.Coyoneda.colimitCoconeIsColimit X).desc s x = s.ι.app (Opposite.unop X) (CategoryTheory.CategoryStruct.id (Opposite.unop X))

def CategoryTheory.Coyoneda.colimitCoconeIsColimit {C : Type u} [CategoryTheory.Category.{v, u} C] (X : Cᵒᵖ) : CategoryTheory.Limits.IsColimit (CategoryTheory.Coyoneda.colimitCocone X)

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.

instance CategoryTheory.Coyoneda.instHasColimitObjOppositeFunctorTypeCoyoneda {C : Type u} [CategoryTheory.Category.{v, u} C] (X : Cᵒᵖ) : CategoryTheory.Limits.HasColimit (CategoryTheory.coyoneda.obj X)

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.Coyoneda.colimitCoyonedaIso {C : Type u} [CategoryTheory.Category.{v, u} C] (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.

@[simp]

theorem CategoryTheory.Limits.coneOfSectionCompYoneda_pt {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] (F : CategoryTheory.Functor J Cᵒᵖ) (X : C) (s : ↑(F.comp (CategoryTheory.yoneda.obj X)).sections) : (CategoryTheory.Limits.coneOfSectionCompYoneda F X s).pt = Opposite.op X

@[simp]

theorem CategoryTheory.Limits.coneOfSectionCompYoneda_π {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] (F : CategoryTheory.Functor J Cᵒᵖ) (X : C) (s : ↑(F.comp (CategoryTheory.yoneda.obj X)).sections) : (CategoryTheory.Limits.coneOfSectionCompYoneda F X s).π = (CategoryTheory.Limits.compYonedaSectionsEquiv F X) s

def CategoryTheory.Limits.coneOfSectionCompYoneda {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] (F : CategoryTheory.Functor J Cᵒᵖ) (X : C) (s : ↑(F.comp (CategoryTheory.yoneda.obj X)).sections) : CategoryTheory.Limits.Cone F

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

Equations

• CategoryTheory.Limits.coneOfSectionCompYoneda F X s = { pt := Opposite.op X, π := (CategoryTheory.Limits.compYonedaSectionsEquiv F X) s }

noncomputable instance CategoryTheory.yonedaPreservesLimit {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] (F : CategoryTheory.Functor J Cᵒᵖ) (X : C) : CategoryTheory.Limits.PreservesLimit F (CategoryTheory.yoneda.obj X)

Equations

• CategoryTheory.yonedaPreservesLimit F X = { preserves := fun {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) => ⋯.some }

noncomputable instance CategoryTheory.yonedaPreservesLimitsOfShape {C : Type u} [CategoryTheory.Category.{v, u} C] (J : Type w) [CategoryTheory.Category.{t, w} J] (X : C) : CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.yoneda.obj X)

Equations

• CategoryTheory.yonedaPreservesLimitsOfShape J X = { preservesLimit := fun {K : CategoryTheory.Functor J Cᵒᵖ} => inferInstance }

def CategoryTheory.yonedaJointlyReflectsLimits {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] (F : CategoryTheory.Functor J Cᵒᵖ) (c : CategoryTheory.Limits.Cone F) (hc : (X : C) → CategoryTheory.Limits.IsLimit ((CategoryTheory.yoneda.obj X).mapCone c)) : CategoryTheory.Limits.IsLimit c

The yoneda embeddings jointly reflect limits.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Limits.Cocone.isColimitYonedaEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) : CategoryTheory.Limits.IsColimit 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.

@[simp]

theorem CategoryTheory.Limits.coneOfSectionCompCoyoneda_π {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] (F : CategoryTheory.Functor J C) (X : Cᵒᵖ) (s : ↑(F.comp (CategoryTheory.coyoneda.obj X)).sections) : (CategoryTheory.Limits.coneOfSectionCompCoyoneda F X s).π = (CategoryTheory.Limits.compCoyonedaSectionsEquiv F (Opposite.unop X)) s

@[simp]

theorem CategoryTheory.Limits.coneOfSectionCompCoyoneda_pt {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] (F : CategoryTheory.Functor J C) (X : Cᵒᵖ) (s : ↑(F.comp (CategoryTheory.coyoneda.obj X)).sections) : (CategoryTheory.Limits.coneOfSectionCompCoyoneda F X s).pt = Opposite.unop X

def CategoryTheory.Limits.coneOfSectionCompCoyoneda {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] (F : CategoryTheory.Functor J C) (X : Cᵒᵖ) (s : ↑(F.comp (CategoryTheory.coyoneda.obj X)).sections) : CategoryTheory.Limits.Cone F

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

Equations

• CategoryTheory.Limits.coneOfSectionCompCoyoneda F X s = { pt := Opposite.unop X, π := (CategoryTheory.Limits.compCoyonedaSectionsEquiv F (Opposite.unop X)) s }

noncomputable instance CategoryTheory.coyonedaPreservesLimit {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] (F : CategoryTheory.Functor J C) (X : Cᵒᵖ) : CategoryTheory.Limits.PreservesLimit F (CategoryTheory.coyoneda.obj X)

Equations

• CategoryTheory.coyonedaPreservesLimit F X = { preserves := fun {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) => ⋯.some }

noncomputable instance CategoryTheory.coyonedaPreservesLimitsOfShape {C : Type u} [CategoryTheory.Category.{v, u} C] (J : Type w) [CategoryTheory.Category.{t, w} J] (X : Cᵒᵖ) : CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.coyoneda.obj X)

Equations

• CategoryTheory.coyonedaPreservesLimitsOfShape J X = { preservesLimit := fun {K : CategoryTheory.Functor J C} => inferInstance }

def CategoryTheory.coyonedaJointlyReflectsLimits {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] (F : CategoryTheory.Functor J C) (c : CategoryTheory.Limits.Cone F) (hc : (X : Cᵒᵖ) → CategoryTheory.Limits.IsLimit ((CategoryTheory.coyoneda.obj X).mapCone c)) : CategoryTheory.Limits.IsLimit c

The coyoneda embeddings jointly reflect limits.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Limits.Cone.isLimitCoyonedaEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : CategoryTheory.Limits.IsLimit 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.

noncomputable instance CategoryTheory.yonedaPreservesLimits {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : CategoryTheory.Limits.PreservesLimitsOfSize.{t, w, v, v, u, v + 1} (CategoryTheory.yoneda.obj X)

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

Equations

• CategoryTheory.yonedaPreservesLimits X = { preservesLimitsOfShape := fun {J : Type w} [CategoryTheory.Category.{t, w} J] => inferInstance }

noncomputable instance CategoryTheory.coyonedaPreservesLimits {C : Type u} [CategoryTheory.Category.{v, u} C] (X : Cᵒᵖ) : CategoryTheory.Limits.PreservesLimitsOfSize.{t, w, v, v, u, v + 1} (CategoryTheory.coyoneda.obj X)

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

Equations

• CategoryTheory.coyonedaPreservesLimits X = { preservesLimitsOfShape := fun {J : Type w} [CategoryTheory.Category.{t, w} J] => inferInstance }

noncomputable instance CategoryTheory.yonedaFunctorPreservesLimits {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Limits.PreservesLimitsOfSize.{t, w, v, max u v, u, max u (v + 1)} CategoryTheory.yoneda

Equations

• CategoryTheory.yonedaFunctorPreservesLimits = CategoryTheory.Limits.preservesLimitsOfEvaluation CategoryTheory.yoneda fun (K : Cᵒᵖ) => let_fun this := inferInstance; this

noncomputable instance CategoryTheory.coyonedaFunctorPreservesLimits {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Limits.PreservesLimitsOfSize.{t, w, v, max u v, u, max u (v + 1)} CategoryTheory.coyoneda

Equations

• CategoryTheory.coyonedaFunctorPreservesLimits = CategoryTheory.Limits.preservesLimitsOfEvaluation CategoryTheory.coyoneda fun (K : C) => let_fun this := inferInstance; this

noncomputable instance CategoryTheory.yonedaFunctorReflectsLimits {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Limits.ReflectsLimitsOfSize.{t, w, v, max u v, u, max u (v + 1)} CategoryTheory.yoneda

Equations

• CategoryTheory.yonedaFunctorReflectsLimits = inferInstance

noncomputable instance CategoryTheory.coyonedaFunctorReflectsLimits {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Limits.ReflectsLimitsOfSize.{t, w, v, max u v, u, max u (v + 1)} CategoryTheory.coyoneda

Equations

• CategoryTheory.coyonedaFunctorReflectsLimits = inferInstance

noncomputable instance CategoryTheory.Functor.representablePreservesLimit {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) [F.Representable] {J : Type u_1} [CategoryTheory.Category.{u_2, u_1} J] (G : CategoryTheory.Functor J Cᵒᵖ) : CategoryTheory.Limits.PreservesLimit G F

Equations

• F.representablePreservesLimit G = CategoryTheory.Limits.preservesLimitOfNatIso G F.reprW

noncomputable instance CategoryTheory.Functor.representablePreservesLimitsOfShape {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) [F.Representable] (J : Type u_1) [CategoryTheory.Category.{u_2, u_1} J] : CategoryTheory.Limits.PreservesLimitsOfShape J F

Equations

• F.representablePreservesLimitsOfShape J = { preservesLimit := fun {K : CategoryTheory.Functor J Cᵒᵖ} => inferInstance }

noncomputable instance CategoryTheory.Functor.representablePreservesLimits {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) [F.Representable] : CategoryTheory.Limits.PreservesLimitsOfSize.{t, w, v, v, u, v + 1} F

Equations

• F.representablePreservesLimits = { preservesLimitsOfShape := fun {J : Type w} [CategoryTheory.Category.{t, w} J] => inferInstance }

noncomputable instance CategoryTheory.Functor.corepresentablePreservesLimit {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type v)) [F.Corepresentable] {J : Type u_1} [CategoryTheory.Category.{u_2, u_1} J] (G : CategoryTheory.Functor J C) : CategoryTheory.Limits.PreservesLimit G F

Equations

• F.corepresentablePreservesLimit G = CategoryTheory.Limits.preservesLimitOfNatIso G F.coreprW

noncomputable instance CategoryTheory.Functor.corepresentablePreservesLimitsOfShape {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type v)) [F.Corepresentable] (J : Type u_1) [CategoryTheory.Category.{u_2, u_1} J] : CategoryTheory.Limits.PreservesLimitsOfShape J F

Equations

• F.corepresentablePreservesLimitsOfShape J = { preservesLimit := fun {K : CategoryTheory.Functor J C} => inferInstance }

noncomputable instance CategoryTheory.Functor.corepresentablePreservesLimits {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type v)) [F.Corepresentable] : CategoryTheory.Limits.PreservesLimitsOfSize.{t, w, v, v, u, v + 1} F

Equations

• F.corepresentablePreservesLimits = { preservesLimitsOfShape := fun {J : Type w} [CategoryTheory.Category.{t, w} J] => inferInstance }