The co-Yoneda embedding is dense

Some of the results of the Yoneda embedding from the file Mathlib/CategoryTheory/Functor/KanExtension/DenseAtYoneda.lean are dualised here for the co-Yoneda embedding.

References

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

@[implicit_reducible]

noncomputable def CategoryTheory.Functor.Elements.shrinkCoyonedaCocone {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (P : Functor C (Type w)) : Limits.Cocone ((π P).op.comp shrinkCoyoneda.{w, v, u})

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

Equations

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

@[simp]

theorem CategoryTheory.Functor.Elements.shrinkCoyonedaCocone_pt {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (P : Functor C (Type w)) : (shrinkCoyonedaCocone P).pt = P

@[simp]

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

theorem CategoryTheory.Functor.Elements.shrinkYoneda_map_app_shrinkCoyonedaCocone_ι_app_app {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (P : Functor C (Type w)) {X Y : C} (f : X ⟶ Y) (u : P.Elementsᵒᵖ) : CategoryStruct.comp ((shrinkYoneda.{w, v, u}.map f).app ((π P).op.obj u)) (((shrinkCoyonedaCocone P).ι.app u).app Y) = CategoryStruct.comp (((shrinkCoyonedaCocone P).ι.app u).app X) (P.map f)

theorem CategoryTheory.Functor.Elements.shrinkYoneda_map_app_shrinkCoyonedaCocone_ι_app_app_assoc {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (P : Functor C (Type w)) {X Y : C} (f : X ⟶ Y) (u : P.Elementsᵒᵖ) {Z : Type w} (h : (((const P.Elementsᵒᵖ).obj (shrinkCoyonedaCocone P).pt).obj u).obj Y ⟶ Z) : CategoryStruct.comp ((shrinkYoneda.{w, v, u}.map f).app ((π P).op.obj u)) (CategoryStruct.comp (((shrinkCoyonedaCocone P).ι.app u).app Y) h) = CategoryStruct.comp (((shrinkCoyonedaCocone P).ι.app u).app X) (CategoryStruct.comp (P.map f) h)

noncomputable def CategoryTheory.Functor.Elements.isColimitShrinkCoyonedaCoconeObj {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 (shrinkCoyonedaCocone P))

For any functor P : C ⥤ Type w, the cocone shrinkCoyonedaCocone P becomes a colimit after applying the evaluation functor at any X : C.

Equations

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

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

Any functor P : C ⥤ Type w is a colimit of corepresentable functors (defined using shrinkCoyoneda) 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.

noncomputable def CategoryTheory.Functor.Elements.shrinkYonedaCompWhiskeringLeftObjπCompColimIso {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (P : Functor C (Type w)) [Limits.HasColimitsOfShape P.Elementsᵒᵖ (Type w)] : shrinkYoneda.{w, v, u}.comp (((whiskeringLeft P.Elementsᵒᵖ Cᵒᵖ (Type w)).obj (π P).op).comp Limits.colim) ≅ P

If F : C ⥤ Type w and C is locally w-small, then F identifies to the composition shrinkYoneda ⋙ (Functor.whiskeringLeft _ _ _).obj (CategoryOfElements.π F).op ⋙ colim.

Equations

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

theorem CategoryTheory.Functor.Elements.shrinkYonedaCompWhiskeringLeftObjπCompColimIso_inv_app_apply {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (P : Functor C (Type w)) [Limits.HasColimitsOfShape P.Elementsᵒᵖ (Type w)] (u : P.Elements) : (ConcreteCategory.hom ((shrinkYonedaCompWhiskeringLeftObjπCompColimIso P).inv.app u.obj)) u.val = (ConcreteCategory.hom (Limits.colimit.ι ((π P).op.comp (shrinkYoneda.{w, v, u}.obj u.obj)) (Opposite.op u))) (shrinkYonedaObjObjEquiv.symm (CategoryStruct.id (Opposite.unop ((π P).op.obj (Opposite.op u)))))

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

instance CategoryTheory.instIsDenseOppositeFunctorTypeCoyoneda {C : Type u} [Category.{v, u} C] : coyoneda.IsDense

noncomputable def CategoryTheory.denseAtShrinkCoyoneda {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (P : Functor C (Type w)) : shrinkCoyoneda.{w, v, u}.DenseAt P

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

Equations

• CategoryTheory.denseAtShrinkCoyoneda P = CategoryTheory.shrinkCoyoneda.{?u.3, ?u.2, ?u.1}.denseAt P

noncomputable def CategoryTheory.denseAtCoyoneda {C : Type u} [Category.{v, u} C] (P : Functor C (Type v)) : coyoneda.DenseAt P

The functor coyoneda : Cᵒᵖ ⥤ C ⥤ Type v is dense at any P : C ⥤ Type v: the functor P identifies to the colimit of the canonical cocone of corepresentable functors indexed by the category CostructuredArrow coyoneda P.

Equations

• CategoryTheory.denseAtCoyoneda P = CategoryTheory.coyoneda.denseAt P