The Yoneda embedding is dense

Any presheaf of types is a colimit of representable presheaves. This is stated in two ways for each of the variants of the Yoneda embedding (yoneda, uliftYoneda and shrinkYoneda):

• as the fact that for any P : Cᵒᵖ ⥤ Type _, there is a colimit cocone involving representable presheaves that is indexed by the opposite category of the category of elements of P, see Functor.Elements.isColimitShrinkYonedaCocone for the case of shrinkYoneda.
• when the opposite of the category of elements is replaced by categories of costructured arrows for the Yoneda embedding, we get definitions like denseAtShrinkYoneda, which expresses that the Yoneda embedding is a dense functor, a fact which is also stated using Functor.IsDense instances.

References

• https://ncatlab.org/nlab/show/dense+subcategory

@[implicit_reducible]

noncomputable def CategoryTheory.Functor.Elements.shrinkYonedaCocone {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (P : Functor Cᵒᵖ (Type w)) : Limits.Cocone ((π P).leftOp.comp shrinkYoneda.{w, v, u})

The (colimit) cocone which expresses a presheaf P : Cᵒᵖ ⥤ Type w as as a colimit (indexed by P.Elementsᵒᵖ) of representable presheaves (defined using shrinkYoneda).

Equations

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

@[simp]

theorem CategoryTheory.Functor.Elements.shrinkYonedaCocone_pt {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (P : Functor Cᵒᵖ (Type w)) : (shrinkYonedaCocone P).pt = P

@[simp]

theorem CategoryTheory.Functor.Elements.shrinkYonedaCocone_ι_app {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (P : Functor Cᵒᵖ (Type w)) (x : P.Elementsᵒᵖ) : (shrinkYonedaCocone P).ι.app x = shrinkYonedaEquiv.symm (Opposite.unop x).val

noncomputable def CategoryTheory.Functor.Elements.isColimitShrinkYonedaCoconeObj {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (P : Functor Cᵒᵖ (Type w)) (X : Cᵒᵖ) : Limits.IsColimit (((evaluation Cᵒᵖ (Type w)).obj X).mapCocone (shrinkYonedaCocone P))

Let P : Cᵒᵖ ⥤ Type w be a presheaf. For any X : Cᵒᵖ, the cocone shrinkYonedaCocone P becomes colimit after applying the evaluation functor (Cᵒᵖ ⥤ Type w) ⥤ Type w at X.

Equations

• CategoryTheory.Functor.Elements.isColimitShrinkYonedaCoconeObj P X = ⋯.some

noncomputable def CategoryTheory.Functor.Elements.isColimitShrinkYonedaCocone {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (P : Functor Cᵒᵖ (Type w)) : Limits.IsColimit (shrinkYonedaCocone P)

Any presheaf P is a colimit of representable presheaves (defined using shrinkYoneda) indexed by the opposite category of the category of elements in P.

Equations

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

@[implicit_reducible]

def CategoryTheory.Functor.Elements.yonedaCocone {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type v)) : Limits.Cocone ((π P).leftOp.comp CategoryTheory.yoneda)

The (colimit) cocone which expresses a presheaf P : Cᵒᵖ ⥤ Type v as as a colimit (indexed by P.Elementsᵒᵖ) of representable presheaves (defined using yoneda).

Equations

• CategoryTheory.Functor.Elements.yonedaCocone P = { pt := P, ι := { app := fun (x : P.Elementsᵒᵖ) => CategoryTheory.yonedaEquiv.symm (Opposite.unop x).val, naturality := ⋯ } }

@[simp]

theorem CategoryTheory.Functor.Elements.yonedaCocone_ι_app {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type v)) (x : P.Elementsᵒᵖ) : (yonedaCocone P).ι.app x = yonedaEquiv.symm (Opposite.unop x).val

@[simp]

theorem CategoryTheory.Functor.Elements.yonedaCocone_pt {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type v)) : (yonedaCocone P).pt = P

noncomputable def CategoryTheory.Functor.Elements.isColimitYonedaCoconeObj {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type v)) (X : Cᵒᵖ) : Limits.IsColimit (((evaluation Cᵒᵖ (Type v)).obj X).mapCocone (yonedaCocone P))

Let P : Cᵒᵖ ⥤ Type v be a presheaf. For any X : Cᵒᵖ, the cocone yonedaCocone P becomes colimit after applying the evaluation functor (Cᵒᵖ ⥤ Type w) ⥤ Type w at X.

Equations

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

noncomputable def CategoryTheory.Functor.Elements.isColimitYonedaCocone {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type v)) : Limits.IsColimit (yonedaCocone P)

Any presheaf P is a colimit of representable presheaves (defined using yoneda) indexed by the opposite category of elements in P.

Equations

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

@[implicit_reducible]

def CategoryTheory.Functor.Elements.uliftYonedaCocone {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type (max w v))) : Limits.Cocone ((π P).leftOp.comp uliftYoneda.{w, v, u})

The (colimit) cocone which expresses a presheaf P : Cᵒᵖ ⥤ Type max w v as as a colimit (indexed by P.Elementsᵒᵖ) of representable presheaves (defined using uliftYoneda).

Equations

• CategoryTheory.Functor.Elements.uliftYonedaCocone P = { pt := P, ι := { app := fun (x : P.Elementsᵒᵖ) => CategoryTheory.uliftYonedaEquiv.symm (Opposite.unop x).val, naturality := ⋯ } }

@[simp]

theorem CategoryTheory.Functor.Elements.uliftYonedaCocone_ι_app {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type (max w v))) (x : P.Elementsᵒᵖ) : (uliftYonedaCocone P).ι.app x = uliftYonedaEquiv.symm (Opposite.unop x).val

@[simp]

theorem CategoryTheory.Functor.Elements.uliftYonedaCocone_pt {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type (max w v))) : (uliftYonedaCocone P).pt = P

noncomputable def CategoryTheory.Functor.Elements.isColimitUliftYonedaCoconeObj {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type (max w v))) (X : Cᵒᵖ) : Limits.IsColimit (((evaluation Cᵒᵖ (Type (max w v))).obj X).mapCocone (uliftYonedaCocone P))

Let P : Cᵒᵖ ⥤ Type max w v be a presheaf. For any X : Cᵒᵖ, the cocone uliftYonedaCocone P becomes colimit after applying the evaluation functor (Cᵒᵖ ⥤ Type w) ⥤ Type w at X.

Equations

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

noncomputable def CategoryTheory.Functor.Elements.isColimitUliftYonedaCocone {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type (max w v))) : Limits.IsColimit (uliftYonedaCocone P)

Any presheaf P is a colimit of representable presheaves (defined using uliftYoneda) indexed by the opposite category of elements in P.

Equations

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

instance CategoryTheory.instIsDenseFunctorOppositeTypeShrinkYoneda {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] : shrinkYoneda.{w, v, u}.IsDense

instance CategoryTheory.instIsDenseFunctorOppositeTypeUliftYoneda {C : Type u} [Category.{v, u} C] : uliftYoneda.{w, v, u}.IsDense

instance CategoryTheory.instIsDenseFunctorOppositeTypeYoneda {C : Type u} [Category.{v, u} C] : yoneda.IsDense

noncomputable def CategoryTheory.denseAtShrinkYoneda {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (P : Functor Cᵒᵖ (Type w)) : shrinkYoneda.{w, v, u}.DenseAt P

When C is a locally w-small category, the functor shrinkYoneda : C ⥤ Cᵒᵖ ⥤ Type w is dense at any P : Cᵒᵖ ⥤ Type w: the presheaf P identifies to the colimit of the canonical cocone of representable presheaves indexed by the category CostructuredArrow shrinkYoneda P.

Equations

• CategoryTheory.denseAtShrinkYoneda P = CategoryTheory.shrinkYoneda.{?u.3, ?u.2, ?u.1}.denseAt P

noncomputable def CategoryTheory.denseAtYoneda {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type v)) : yoneda.DenseAt P

The functor yoneda : C ⥤ Cᵒᵖ ⥤ Type v is dense at any P : Cᵒᵖ ⥤ Type v: the presheaf P identifies to the colimit of the canonical cocone of representable presheaves indexed by the category CostructuredArrow yoneda P.

Equations

• CategoryTheory.denseAtYoneda P = CategoryTheory.yoneda.denseAt P

noncomputable def CategoryTheory.denseAtUliftYoneda {C : Type u} [Category.{v, u} C] (P : Functor Cᵒᵖ (Type (max w v))) : uliftYoneda.{w, v, u}.DenseAt P

When C is a category where morphisms are in Type v, the functor uliftYoneda.{w} : C ⥤ Cᵒᵖ ⥤ Type max w v is dense at any P : Cᵒᵖ ⥤ Type max w v: the presheaf P identifies to the colimit of the canonical cocone of representable presheaves indexed by the category CostructuredArrow uliftYoneda P.

Equations

• CategoryTheory.denseAtUliftYoneda P = CategoryTheory.uliftYoneda.{?u.3, ?u.2, ?u.1}.denseAt P

theorem CategoryTheory.Presheaf.final_toCostructuredArrow_comp_pre {C : Type u} [Category.{v, u} C] {I : Type v} [SmallCategory I] (F : Functor I C) {c : Limits.Cocone (F.comp yoneda)} (hc : Limits.IsColimit c) : (c.toCostructuredArrow.comp (CostructuredArrow.pre F yoneda c.pt)).Final

Given a functor F : I ⥤ C, a cocone c on F ⋙ yoneda : I ⥤ Cᵒᵖ ⥤ Type v₁ induces a functor I ⥤ CostructuredArrow yoneda c.pt which maps i : I to the leg yoneda.obj (F.obj i) ⟶ c.pt. If c is a colimit cocone, then that functor is final.

Proposition 2.6.3(ii) in [KS06]