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.

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

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 := ⋯ } }

theorem CategoryTheory.Coyoneda.colimitCocone_pt {C : Type u} [Category C] (X : Opposite C) : Eq (colimitCocone X).pt PUnit

theorem CategoryTheory.Coyoneda.colimitCocone_ι_app {C : Type u} [Category C] (X : Opposite C) (X_1 : C) (a : (coyoneda.obj X).obj X_1) : Eq ((colimitCocone X).ι.app X_1 a) (id PUnit.unit)

def CategoryTheory.Coyoneda.colimitCoconeIsColimit {C : Type u} [Category C] (X : Opposite C) : Limits.IsColimit (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.

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

theorem CategoryTheory.Coyoneda.instHasColimitObjOppositeFunctorTypeCoyoneda {C : Type u} [Category C] (X : Opposite C) : Limits.HasColimit (coyoneda.obj X)

noncomputable def CategoryTheory.Coyoneda.colimitCoyonedaIso {C : Type u} [Category C] (X : Opposite C) : Iso (Limits.colimit (coyoneda.obj X)) PUnit

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

Equations

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

def CategoryTheory.Limits.coneOfSectionCompYoneda {C : Type u} [Category C] {J : Type w} [Category J] (F : Functor J (Opposite C)) (X : C) (s : (F.comp (yoneda.obj X)).sections.Elem) : Cone F

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 }

theorem CategoryTheory.Limits.coneOfSectionCompYoneda_π {C : Type u} [Category C] {J : Type w} [Category J] (F : Functor J (Opposite C)) (X : C) (s : (F.comp (yoneda.obj X)).sections.Elem) : Eq (coneOfSectionCompYoneda F X s).π (DFunLike.coe (compYonedaSectionsEquiv F X) s)

theorem CategoryTheory.Limits.coneOfSectionCompYoneda_pt {C : Type u} [Category C] {J : Type w} [Category J] (F : Functor J (Opposite C)) (X : C) (s : (F.comp (yoneda.obj X)).sections.Elem) : Eq (coneOfSectionCompYoneda F X s).pt { unop := X }

theorem CategoryTheory.yoneda_preservesLimit {C : Type u} [Category C] {J : Type w} [Category J] (F : Functor J (Opposite C)) (X : C) : Limits.PreservesLimit F (yoneda.obj X)

theorem CategoryTheory.yoneda_preservesLimitsOfShape {C : Type u} [Category C] (J : Type w) [Category J] (X : C) : Limits.PreservesLimitsOfShape J (yoneda.obj X)

def CategoryTheory.yonedaJointlyReflectsLimits {C : Type u} [Category C] {J : Type w} [Category J] (F : Functor J (Opposite C)) (c : Limits.Cone F) (hc : (X : C) → Limits.IsLimit ((yoneda.obj X).mapCone c)) : 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} [Category C] {J : Type w} [Category J] {F : Functor J C} (c : Cocone F) : Equiv (IsColimit c) ((X : C) → IsLimit ((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.

def CategoryTheory.Limits.coneOfSectionCompCoyoneda {C : Type u} [Category C] {J : Type w} [Category J] (F : Functor J C) (X : Opposite C) (s : (F.comp (coyoneda.obj X)).sections.Elem) : Cone F

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 }

theorem CategoryTheory.Limits.coneOfSectionCompCoyoneda_pt {C : Type u} [Category C] {J : Type w} [Category J] (F : Functor J C) (X : Opposite C) (s : (F.comp (coyoneda.obj X)).sections.Elem) : Eq (coneOfSectionCompCoyoneda F X s).pt (Opposite.unop X)

theorem CategoryTheory.Limits.coneOfSectionCompCoyoneda_π {C : Type u} [Category C] {J : Type w} [Category J] (F : Functor J C) (X : Opposite C) (s : (F.comp (coyoneda.obj X)).sections.Elem) : Eq (coneOfSectionCompCoyoneda F X s).π (DFunLike.coe (compCoyonedaSectionsEquiv F (Opposite.unop X)) s)

theorem CategoryTheory.coyoneda_preservesLimit {C : Type u} [Category C] {J : Type w} [Category J] (F : Functor J C) (X : Opposite C) : Limits.PreservesLimit F (coyoneda.obj X)

theorem CategoryTheory.coyonedaPreservesLimitsOfShape {C : Type u} [Category C] (J : Type w) [Category J] (X : Opposite C) : Limits.PreservesLimitsOfShape J (coyoneda.obj X)

def CategoryTheory.coyonedaJointlyReflectsLimits {C : Type u} [Category C] {J : Type w} [Category J] (F : Functor J C) (c : Limits.Cone F) (hc : (X : Opposite C) → Limits.IsLimit ((coyoneda.obj X).mapCone c)) : 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} [Category C] {J : Type w} [Category J] {F : Functor J C} (c : Cone F) : Equiv (IsLimit c) ((X : Opposite C) → IsLimit ((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.

theorem CategoryTheory.yoneda_preservesLimits {C : Type u} [Category C] (X : C) : Limits.PreservesLimitsOfSize (yoneda.obj X)

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

theorem CategoryTheory.coyoneda_preservesLimits {C : Type u} [Category C] (X : Opposite C) : Limits.PreservesLimitsOfSize (coyoneda.obj X)

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

theorem CategoryTheory.yonedaFunctor_preservesLimits {C : Type u} [Category C] : Limits.PreservesLimitsOfSize yoneda

theorem CategoryTheory.coyonedaFunctor_preservesLimits {C : Type u} [Category C] : Limits.PreservesLimitsOfSize coyoneda

theorem CategoryTheory.yonedaFunctor_reflectsLimits {C : Type u} [Category C] : Limits.ReflectsLimitsOfSize yoneda

theorem CategoryTheory.coyonedaFunctor_reflectsLimits {C : Type u} [Category C] : Limits.ReflectsLimitsOfSize coyoneda

theorem CategoryTheory.Functor.representable_preservesLimit {C : Type u} [Category C] (F : Functor (Opposite C) (Type v)) [F.IsRepresentable] {J : Type u_1} [Category J] (G : Functor J (Opposite C)) : Limits.PreservesLimit G F

theorem CategoryTheory.Functor.representable_preservesLimitsOfShape {C : Type u} [Category C] (F : Functor (Opposite C) (Type v)) [F.IsRepresentable] (J : Type u_1) [Category J] : Limits.PreservesLimitsOfShape J F

theorem CategoryTheory.Functor.representable_preservesLimits {C : Type u} [Category C] (F : Functor (Opposite C) (Type v)) [F.IsRepresentable] : Limits.PreservesLimitsOfSize F

theorem CategoryTheory.Functor.corepresentable_preservesLimit {C : Type u} [Category C] (F : Functor C (Type v)) [F.IsCorepresentable] {J : Type u_1} [Category J] (G : Functor J C) : Limits.PreservesLimit G F

theorem CategoryTheory.Functor.corepresentable_preservesLimitsOfShape {C : Type u} [Category C] (F : Functor C (Type v)) [F.IsCorepresentable] (J : Type u_1) [Category J] : Limits.PreservesLimitsOfShape J F

theorem CategoryTheory.Functor.corepresentable_preservesLimits {C : Type u} [Category C] (F : Functor C (Type v)) [F.IsCorepresentable] : Limits.PreservesLimitsOfSize F