Colimit of representables

This file constructs an adjunction yonedaAdjunction between (Cᵒᵖ ⥤ Type u) and ℰ given a functor A : C ⥤ ℰ, where the right adjoint sends (E : ℰ) to c ↦ (A.obj c ⟶ E) (provided ℰ has colimits).

This adjunction is used to show that every presheaf is a colimit of representables. This result is also known as the density theorem, the co-Yoneda lemma and the Ninja Yoneda lemma.

Further, the left adjoint colimitAdj.extendAlongYoneda : (Cᵒᵖ ⥤ Type u) ⥤ ℰ satisfies yoneda ⋙ L ≅ A, that is, an extension of A : C ⥤ ℰ to (Cᵒᵖ ⥤ Type u) ⥤ ℰ through yoneda : C ⥤ Cᵒᵖ ⥤ Type u. It is the left Kan extension of A along the yoneda embedding, sometimes known as the Yoneda extension, as proved in extendAlongYonedaIsoKan.

uniqueExtensionAlongYoneda shows extendAlongYoneda is unique amongst cocontinuous functors with this property, establishing the presheaf category as the free cocompletion of a small category.

We also give a direct pedestrian proof that every presheaf is a colimit of representables. This version of the proof is valid for any category C, even if it is not small.

Tags

colimit, representable, presheaf, free cocompletion

References

• [S. MacLane, I. Moerdijk, Sheaves in Geometry and Logic][MM92]
• https://ncatlab.org/nlab/show/Yoneda+extension

@[simp]

theorem CategoryTheory.ColimitAdj.restrictedYoneda_obj_obj {C : Type u₁} [CategoryTheory.SmallCategory C] {ℰ : Type u₂} [CategoryTheory.Category.{u₁, u₂} ℰ] (A : CategoryTheory.Functor C ℰ) (X : ℰ) (X : Cᵒᵖ) : ((CategoryTheory.ColimitAdj.restrictedYoneda A).obj X✝).obj X = (A.obj X.unop ⟶ X✝)

@[simp]

theorem CategoryTheory.ColimitAdj.restrictedYoneda_obj_map {C : Type u₁} [CategoryTheory.SmallCategory C] {ℰ : Type u₂} [CategoryTheory.Category.{u₁, u₂} ℰ] (A : CategoryTheory.Functor C ℰ) (X : ℰ) : ∀ {X_1 Y : Cᵒᵖ} (f : X_1 ⟶ Y) (a : (CategoryTheory.yoneda.obj X).obj (A.op.obj X_1)), ((CategoryTheory.ColimitAdj.restrictedYoneda A).obj X).map f a = CategoryTheory.CategoryStruct.comp (A.map f.unop) a

@[simp]

theorem CategoryTheory.ColimitAdj.restrictedYoneda_map_app {C : Type u₁} [CategoryTheory.SmallCategory C] {ℰ : Type u₂} [CategoryTheory.Category.{u₁, u₂} ℰ] (A : CategoryTheory.Functor C ℰ) : ∀ {X Y : ℰ} (f : X ⟶ Y) (X_1 : Cᵒᵖ) (a : (CategoryTheory.yoneda.obj X).obj (A.op.obj X_1)), ((CategoryTheory.ColimitAdj.restrictedYoneda A).map f).app X_1 a = CategoryTheory.CategoryStruct.comp a f

def CategoryTheory.ColimitAdj.restrictedYoneda {C : Type u₁} [CategoryTheory.SmallCategory C] {ℰ : Type u₂} [CategoryTheory.Category.{u₁, u₂} ℰ] (A : CategoryTheory.Functor C ℰ) : CategoryTheory.Functor ℰ (CategoryTheory.Functor Cᵒᵖ (Type u₁))

The functor taking (E : ℰ) (c : Cᵒᵖ) to the homset (A.obj C ⟶ E). It is shown in L_adjunction that this functor has a left adjoint (provided E has colimits) given by taking colimits over categories of elements. In the case where ℰ = Cᵒᵖ ⥤ Type u and A = yoneda, this functor is isomorphic to the identity.

Defined as in [MM92], Chapter I, Section 5, Theorem 2.

Equations

• CategoryTheory.ColimitAdj.restrictedYoneda A = CategoryTheory.Functor.comp CategoryTheory.yoneda ((CategoryTheory.whiskeringLeft Cᵒᵖ ℰᵒᵖ (Type u₁)).obj A.op)

def CategoryTheory.ColimitAdj.restrictedYonedaYoneda {C : Type u₁} [CategoryTheory.SmallCategory C] : CategoryTheory.ColimitAdj.restrictedYoneda CategoryTheory.yoneda ≅ CategoryTheory.Functor.id (CategoryTheory.Functor Cᵒᵖ (Type u₁))

The functor restrictedYoneda is isomorphic to the identity functor when evaluated at the yoneda embedding.

Equations

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

def CategoryTheory.ColimitAdj.restrictYonedaHomEquiv {C : Type u₁} [CategoryTheory.SmallCategory C] {ℰ : Type u₂} [CategoryTheory.Category.{u₁, u₂} ℰ] (A : CategoryTheory.Functor C ℰ) (P : CategoryTheory.Functor Cᵒᵖ (Type u₁)) (E : ℰ) {c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.π P).leftOp A)} (t : CategoryTheory.Limits.IsColimit c) : (c.pt ⟶ E) ≃ (P ⟶ (CategoryTheory.ColimitAdj.restrictedYoneda A).obj E)

(Implementation). The equivalence of homsets which helps construct the left adjoint to colimitAdj.restrictedYoneda. It is shown in restrictYonedaHomEquivNatural that this is a natural bijection.

Equations

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

theorem CategoryTheory.ColimitAdj.restrictYonedaHomEquiv_natural {C : Type u₁} [CategoryTheory.SmallCategory C] {ℰ : Type u₂} [CategoryTheory.Category.{u₁, u₂} ℰ] (A : CategoryTheory.Functor C ℰ) (P : CategoryTheory.Functor Cᵒᵖ (Type u₁)) (E₁ : ℰ) (E₂ : ℰ) (g : E₁ ⟶ E₂) {c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.π P).leftOp A)} (t : CategoryTheory.Limits.IsColimit c) (k : c.pt ⟶ E₁) : (CategoryTheory.ColimitAdj.restrictYonedaHomEquiv A P E₂ t) (CategoryTheory.CategoryStruct.comp k g) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.ColimitAdj.restrictYonedaHomEquiv A P E₁ t) k) ((CategoryTheory.ColimitAdj.restrictedYoneda A).map g)

(Implementation). Show that the bijection in restrictYonedaHomEquiv is natural (on the right).

noncomputable def CategoryTheory.ColimitAdj.extendAlongYoneda {C : Type u₁} [CategoryTheory.SmallCategory C] {ℰ : Type u₂} [CategoryTheory.Category.{u₁, u₂} ℰ] (A : CategoryTheory.Functor C ℰ) [CategoryTheory.Limits.HasColimits ℰ] : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type u₁)) ℰ

The left adjoint to the functor restrictedYoneda (shown in yonedaAdjunction). It is also an extension of A along the yoneda embedding (shown in isExtensionAlongYoneda), in particular it is the left Kan extension of A through the yoneda embedding.

Equations

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

@[simp]

theorem CategoryTheory.ColimitAdj.extendAlongYoneda_obj {C : Type u₁} [CategoryTheory.SmallCategory C] {ℰ : Type u₂} [CategoryTheory.Category.{u₁, u₂} ℰ] (A : CategoryTheory.Functor C ℰ) [CategoryTheory.Limits.HasColimits ℰ] (P : CategoryTheory.Functor Cᵒᵖ (Type u₁)) : (CategoryTheory.ColimitAdj.extendAlongYoneda A).obj P = CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.π P).leftOp A)

theorem CategoryTheory.ColimitAdj.extendAlongYoneda_obj.hom_ext {C : Type u₁} [CategoryTheory.SmallCategory C] {ℰ : Type u₂} [CategoryTheory.Category.{u₁, u₂} ℰ] (A : CategoryTheory.Functor C ℰ) [CategoryTheory.Limits.HasColimits ℰ] {X : ℰ} {P : CategoryTheory.Functor Cᵒᵖ (Type u₁)} {f : (CategoryTheory.ColimitAdj.extendAlongYoneda A).obj P ⟶ X} {f' : (CategoryTheory.ColimitAdj.extendAlongYoneda A).obj P ⟶ X} (w : ∀ (j : (CategoryTheory.Functor.Elements P)ᵒᵖ), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.π P).leftOp A) j) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.π P).leftOp A) j) f') : f = f'

theorem CategoryTheory.ColimitAdj.extendAlongYoneda_map {C : Type u₁} [CategoryTheory.SmallCategory C] {ℰ : Type u₂} [CategoryTheory.Category.{u₁, u₂} ℰ] (A : CategoryTheory.Functor C ℰ) [CategoryTheory.Limits.HasColimits ℰ] {X : CategoryTheory.Functor Cᵒᵖ (Type u₁)} {Y : CategoryTheory.Functor Cᵒᵖ (Type u₁)} (f : X ⟶ Y) : (CategoryTheory.ColimitAdj.extendAlongYoneda A).map f = CategoryTheory.Limits.colimit.pre (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.π Y).leftOp A) (CategoryTheory.CategoryOfElements.map f).op

noncomputable def CategoryTheory.ColimitAdj.yonedaAdjunction {C : Type u₁} [CategoryTheory.SmallCategory C] {ℰ : Type u₂} [CategoryTheory.Category.{u₁, u₂} ℰ] (A : CategoryTheory.Functor C ℰ) [CategoryTheory.Limits.HasColimits ℰ] : CategoryTheory.ColimitAdj.extendAlongYoneda A ⊣ CategoryTheory.ColimitAdj.restrictedYoneda A

Show extendAlongYoneda is left adjoint to restrictedYoneda.

The construction of [MM92], Chapter I, Section 5, Theorem 2.

Equations

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

def CategoryTheory.ColimitAdj.Elements.initial {C : Type u₁} [CategoryTheory.SmallCategory C] (A : C) : CategoryTheory.Functor.Elements (CategoryTheory.yoneda.obj A)

The initial object in the category of elements for a representable functor. In isInitial it is shown that this is initial.

Equations

• CategoryTheory.ColimitAdj.Elements.initial A = { fst := Opposite.op A, snd := CategoryTheory.CategoryStruct.id (Opposite.op A).unop }

def CategoryTheory.ColimitAdj.isInitial {C : Type u₁} [CategoryTheory.SmallCategory C] (A : C) : CategoryTheory.Limits.IsInitial (CategoryTheory.ColimitAdj.Elements.initial A)

Show that Elements.initial A is initial in the category of elements for the yoneda functor.

Equations

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

noncomputable def CategoryTheory.ColimitAdj.isExtensionAlongYoneda {C : Type u₁} [CategoryTheory.SmallCategory C] {ℰ : Type u₂} [CategoryTheory.Category.{u₁, u₂} ℰ] (A : CategoryTheory.Functor C ℰ) [CategoryTheory.Limits.HasColimits ℰ] : CategoryTheory.Functor.comp CategoryTheory.yoneda (CategoryTheory.ColimitAdj.extendAlongYoneda A) ≅ A

extendAlongYoneda A is an extension of A to the presheaf category along the yoneda embedding. uniqueExtensionAlongYoneda shows it is unique among functors preserving colimits with this property (up to isomorphism).

The first part of [MM92], Chapter I, Section 5, Corollary 4. See Property 1 of .

Equations

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

noncomputable instance CategoryTheory.ColimitAdj.instPreservesColimitsFunctorOppositeOppositeTypeTypesCategoryExtendAlongYoneda {C : Type u₁} [CategoryTheory.SmallCategory C] {ℰ : Type u₂} [CategoryTheory.Category.{u₁, u₂} ℰ] (A : CategoryTheory.Functor C ℰ) [CategoryTheory.Limits.HasColimits ℰ] : CategoryTheory.Limits.PreservesColimits (CategoryTheory.ColimitAdj.extendAlongYoneda A)

See Property 2 of https://ncatlab.org/nlab/show/Yoneda+extension#properties.

Equations

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

@[simp]

theorem CategoryTheory.ColimitAdj.extendAlongYonedaIsoKanApp_hom {C : Type u₁} [CategoryTheory.SmallCategory C] {ℰ : Type u₂} [CategoryTheory.Category.{u₁, u₂} ℰ] (A : CategoryTheory.Functor C ℰ) [CategoryTheory.Limits.HasColimits ℰ] (X : CategoryTheory.Functor Cᵒᵖ (Type u₁)) : (CategoryTheory.ColimitAdj.extendAlongYonedaIsoKanApp A X).hom = CategoryTheory.Limits.colimit.pre (CategoryTheory.Lan.diagram CategoryTheory.yoneda A X) (CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence X).functor

@[simp]

theorem CategoryTheory.ColimitAdj.extendAlongYonedaIsoKanApp_inv {C : Type u₁} [CategoryTheory.SmallCategory C] {ℰ : Type u₂} [CategoryTheory.Category.{u₁, u₂} ℰ] (A : CategoryTheory.Functor C ℰ) [CategoryTheory.Limits.HasColimits ℰ] (X : CategoryTheory.Functor Cᵒᵖ (Type u₁)) : (CategoryTheory.ColimitAdj.extendAlongYonedaIsoKanApp A X).inv = CategoryTheory.Limits.colimit.pre (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.π X).leftOp A) (CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence X).inverse

noncomputable def CategoryTheory.ColimitAdj.extendAlongYonedaIsoKanApp {C : Type u₁} [CategoryTheory.SmallCategory C] {ℰ : Type u₂} [CategoryTheory.Category.{u₁, u₂} ℰ] (A : CategoryTheory.Functor C ℰ) [CategoryTheory.Limits.HasColimits ℰ] (X : CategoryTheory.Functor Cᵒᵖ (Type u₁)) : (CategoryTheory.ColimitAdj.extendAlongYoneda A).obj X ≅ ((CategoryTheory.lan CategoryTheory.yoneda).obj A).obj X

Show that the images of X after extendAlongYoneda and Lan yoneda are indeed isomorphic. This follows from CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence.

Equations

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

@[simp]

theorem CategoryTheory.ColimitAdj.extendAlongYonedaIsoKan_inv_app {C : Type u₁} [CategoryTheory.SmallCategory C] {ℰ : Type u₂} [CategoryTheory.Category.{u₁, u₂} ℰ] (A : CategoryTheory.Functor C ℰ) [CategoryTheory.Limits.HasColimits ℰ] (X : CategoryTheory.Functor Cᵒᵖ (Type u₁)) : (CategoryTheory.ColimitAdj.extendAlongYonedaIsoKan A).inv.app X = CategoryTheory.Limits.colimit.pre (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.π X).leftOp A) (CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence X).inverse

@[simp]

theorem CategoryTheory.ColimitAdj.extendAlongYonedaIsoKan_hom_app {C : Type u₁} [CategoryTheory.SmallCategory C] {ℰ : Type u₂} [CategoryTheory.Category.{u₁, u₂} ℰ] (A : CategoryTheory.Functor C ℰ) [CategoryTheory.Limits.HasColimits ℰ] (X : CategoryTheory.Functor Cᵒᵖ (Type u₁)) : (CategoryTheory.ColimitAdj.extendAlongYonedaIsoKan A).hom.app X = CategoryTheory.Limits.colimit.pre (CategoryTheory.Lan.diagram CategoryTheory.yoneda A X) (CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence X).functor

noncomputable def CategoryTheory.ColimitAdj.extendAlongYonedaIsoKan {C : Type u₁} [CategoryTheory.SmallCategory C] {ℰ : Type u₂} [CategoryTheory.Category.{u₁, u₂} ℰ] (A : CategoryTheory.Functor C ℰ) [CategoryTheory.Limits.HasColimits ℰ] : CategoryTheory.ColimitAdj.extendAlongYoneda A ≅ (CategoryTheory.lan CategoryTheory.yoneda).obj A

Verify that extendAlongYoneda is indeed the left Kan extension along the yoneda embedding.

Equations

• CategoryTheory.ColimitAdj.extendAlongYonedaIsoKan A = CategoryTheory.NatIso.ofComponents (CategoryTheory.ColimitAdj.extendAlongYonedaIsoKanApp A) ⋯

noncomputable def CategoryTheory.ColimitAdj.extendOfCompYonedaIsoLan {C : Type u₁} [CategoryTheory.SmallCategory C] {D : Type u₁} [CategoryTheory.SmallCategory D] (F : CategoryTheory.Functor C D) : CategoryTheory.ColimitAdj.extendAlongYoneda (CategoryTheory.Functor.comp F CategoryTheory.yoneda) ≅ CategoryTheory.lan F.op

extending F ⋙ yoneda along the yoneda embedding is isomorphic to Lan F.op.

Equations

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

@[simp]

theorem CategoryTheory.ColimitAdj.extendOfCompYonedaIsoLan_inv_app_app {C : Type u₁} [CategoryTheory.SmallCategory C] {D : Type u₁} [CategoryTheory.SmallCategory D] (F : CategoryTheory.Functor C D) (X : CategoryTheory.Functor Cᵒᵖ (Type u₁)) (x : Dᵒᵖ) : ∀ (a : CategoryTheory.Limits.colimit (CategoryTheory.Lan.diagram F.op (Opposite.op X).unop x)), ((CategoryTheory.ColimitAdj.extendOfCompYonedaIsoLan F).inv.app X).app x a = CategoryTheory.Limits.colimit.desc (CategoryTheory.Lan.diagram F.op X x) { pt := (CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.π X).leftOp (CategoryTheory.Functor.comp F CategoryTheory.yoneda))).obj x, ι := { app := fun (i : CategoryTheory.CostructuredArrow F.op x) => CategoryTheory.CategoryStruct.comp (((CategoryTheory.Adjunction.equivHomsetRightOfNatIso (CategoryTheory.isoWhiskerRight CategoryTheory.curriedYonedaLemma' ((CategoryTheory.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type u₁)).obj F.op)).symm).symm (((CategoryTheory.ColimitAdj.yonedaAdjunction (CategoryTheory.Functor.comp F CategoryTheory.yoneda)).homEquiv X (CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.π X).leftOp (CategoryTheory.Functor.comp F CategoryTheory.yoneda)))) (CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.π X).leftOp (CategoryTheory.Functor.comp F CategoryTheory.yoneda)))))).app i.left) ((CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.π X).leftOp (CategoryTheory.Functor.comp F CategoryTheory.yoneda))).map i.hom), naturality := ⋯ } } a

@[simp]

theorem CategoryTheory.ColimitAdj.extendOfCompYonedaIsoLan_hom_app {C : Type u₁} [CategoryTheory.SmallCategory C] {D : Type u₁} [CategoryTheory.SmallCategory D] (F : CategoryTheory.Functor C D) (X : CategoryTheory.Functor Cᵒᵖ (Type u₁)) : (CategoryTheory.ColimitAdj.extendOfCompYonedaIsoLan F).hom.app X = (CategoryTheory.coyoneda.preimage ((CategoryTheory.Adjunction.leftAdjointsCoyonedaEquiv (CategoryTheory.Adjunction.ofNatIsoRight (CategoryTheory.Lan.adjunction (Type u₁) F.op) (CategoryTheory.isoWhiskerRight CategoryTheory.curriedYonedaLemma' ((CategoryTheory.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type u₁)).obj F.op)).symm) (CategoryTheory.ColimitAdj.yonedaAdjunction (CategoryTheory.Functor.comp F CategoryTheory.yoneda))).hom.app (Opposite.op X))).unop

@[simp]

theorem CategoryTheory.compYonedaIsoYonedaCompLan_inv_app_app {C : Type u₁} [CategoryTheory.SmallCategory C] {D : Type u₁} [CategoryTheory.SmallCategory D] (F : CategoryTheory.Functor C D) (X : C) (X : Dᵒᵖ) : ∀ (a : ((CategoryTheory.Functor.comp CategoryTheory.yoneda (CategoryTheory.lan F.op)).obj X✝).obj X), ((CategoryTheory.compYonedaIsoYonedaCompLan F).inv.app X✝).app X a = ((CategoryTheory.ColimitAdj.isExtensionAlongYoneda (CategoryTheory.Functor.comp F CategoryTheory.yoneda)).hom.app X✝).app X (CategoryTheory.Limits.colimit.desc (CategoryTheory.Lan.diagram F.op (CategoryTheory.yoneda.obj X✝) X) { pt := (CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.π (CategoryTheory.yoneda.obj X✝)).leftOp (CategoryTheory.Functor.comp F CategoryTheory.yoneda))).obj X, ι := { app := fun (i : CategoryTheory.CostructuredArrow F.op X) => CategoryTheory.CategoryStruct.comp (((CategoryTheory.Adjunction.equivHomsetRightOfNatIso (CategoryTheory.isoWhiskerRight CategoryTheory.curriedYonedaLemma' ((CategoryTheory.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type u₁)).obj F.op)).symm).symm (((CategoryTheory.ColimitAdj.yonedaAdjunction (CategoryTheory.Functor.comp F CategoryTheory.yoneda)).homEquiv (CategoryTheory.yoneda.obj X✝) (CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.π (CategoryTheory.yoneda.obj X✝)).leftOp (CategoryTheory.Functor.comp F CategoryTheory.yoneda)))) (CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.π (CategoryTheory.yoneda.obj X✝)).leftOp (CategoryTheory.Functor.comp F CategoryTheory.yoneda)))))).app i.left) ((CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.π (CategoryTheory.yoneda.obj X✝)).leftOp (CategoryTheory.Functor.comp F CategoryTheory.yoneda))).map i.hom), naturality := ⋯ } } a)

@[simp]

theorem CategoryTheory.compYonedaIsoYonedaCompLan_hom_app_app {C : Type u₁} [CategoryTheory.SmallCategory C] {D : Type u₁} [CategoryTheory.SmallCategory D] (F : CategoryTheory.Functor C D) (X : C) (X : Dᵒᵖ) : ∀ (a : ((CategoryTheory.Functor.comp F CategoryTheory.yoneda).obj X✝).obj X), ((CategoryTheory.compYonedaIsoYonedaCompLan F).hom.app X✝).app X a = (CategoryTheory.coyoneda.preimage ((CategoryTheory.Adjunction.leftAdjointsCoyonedaEquiv (CategoryTheory.Adjunction.ofNatIsoRight (CategoryTheory.Lan.adjunction (Type u₁) F.op) (CategoryTheory.isoWhiskerRight CategoryTheory.curriedYonedaLemma' ((CategoryTheory.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type u₁)).obj F.op)).symm) (CategoryTheory.ColimitAdj.yonedaAdjunction (CategoryTheory.Functor.comp F CategoryTheory.yoneda))).hom.app (Opposite.op (CategoryTheory.yoneda.obj X✝)))).unop.app X (((CategoryTheory.ColimitAdj.isExtensionAlongYoneda (CategoryTheory.Functor.comp F CategoryTheory.yoneda)).inv.app X✝).app X a)

noncomputable def CategoryTheory.compYonedaIsoYonedaCompLan {C : Type u₁} [CategoryTheory.SmallCategory C] {D : Type u₁} [CategoryTheory.SmallCategory D] (F : CategoryTheory.Functor C D) : CategoryTheory.Functor.comp F CategoryTheory.yoneda ≅ CategoryTheory.Functor.comp CategoryTheory.yoneda (CategoryTheory.lan F.op)

F ⋙ yoneda is naturally isomorphic to yoneda ⋙ Lan F.op.

Equations

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

noncomputable def CategoryTheory.extendAlongYonedaYoneda {C : Type u₁} [CategoryTheory.SmallCategory C] : CategoryTheory.ColimitAdj.extendAlongYoneda CategoryTheory.yoneda ≅ CategoryTheory.Functor.id (CategoryTheory.Functor Cᵒᵖ (Type u₁))

Since extendAlongYoneda A is adjoint to restrictedYoneda A, if we use A = yoneda then restrictedYoneda A is isomorphic to the identity, and so extendAlongYoneda A is as well.

Equations

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

def CategoryTheory.functorToRepresentables {C : Type u₁} [CategoryTheory.SmallCategory C] (P : CategoryTheory.Functor Cᵒᵖ (Type u₁)) : CategoryTheory.Functor (CategoryTheory.Functor.Elements P)ᵒᵖ (CategoryTheory.Functor Cᵒᵖ (Type u₁))

A functor to the presheaf category in which everything in the image is representable (witnessed by the fact that it factors through the yoneda embedding). coconeOfRepresentable gives a cocone for this functor which is a colimit and has point P.

Equations

• CategoryTheory.functorToRepresentables P = CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.π P).leftOp CategoryTheory.yoneda

noncomputable def CategoryTheory.coconeOfRepresentable {C : Type u₁} [CategoryTheory.SmallCategory C] (P : CategoryTheory.Functor Cᵒᵖ (Type u₁)) : CategoryTheory.Limits.Cocone (CategoryTheory.functorToRepresentables P)

This is a cocone with point P for the functor functorToRepresentables P. It is shown in colimitOfRepresentable P that this cocone is a colimit: that is, we have exhibited an arbitrary presheaf P as a colimit of representables.

The construction of [MM92], Chapter I, Section 5, Corollary 3.

Equations

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

@[simp]

theorem CategoryTheory.coconeOfRepresentable_pt {C : Type u₁} [CategoryTheory.SmallCategory C] (P : CategoryTheory.Functor Cᵒᵖ (Type u₁)) : (CategoryTheory.coconeOfRepresentable P).pt = P

theorem CategoryTheory.coconeOfRepresentable_ι_app {C : Type u₁} [CategoryTheory.SmallCategory C] (P : CategoryTheory.Functor Cᵒᵖ (Type u₁)) (j : (CategoryTheory.Functor.Elements P)ᵒᵖ) : (CategoryTheory.coconeOfRepresentable P).ι.app j = (CategoryTheory.yonedaSectionsSmall j.unop.1.unop P).inv j.unop.snd

An explicit formula for the legs of the cocone coconeOfRepresentable.

theorem CategoryTheory.coconeOfRepresentable_naturality {C : Type u₁} [CategoryTheory.SmallCategory C] {P₁ : CategoryTheory.Functor Cᵒᵖ (Type u₁)} {P₂ : CategoryTheory.Functor Cᵒᵖ (Type u₁)} (α : P₁ ⟶ P₂) (j : (CategoryTheory.Functor.Elements P₁)ᵒᵖ) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.coconeOfRepresentable P₁).ι.app j) α = (CategoryTheory.coconeOfRepresentable P₂).ι.app ((CategoryTheory.CategoryOfElements.map α).op.obj j)

The legs of the cocone coconeOfRepresentable are natural in the choice of presheaf.

noncomputable def CategoryTheory.colimitOfRepresentable {C : Type u₁} [CategoryTheory.SmallCategory C] (P : CategoryTheory.Functor Cᵒᵖ (Type u₁)) : CategoryTheory.Limits.IsColimit (CategoryTheory.coconeOfRepresentable P)

The cocone with point P given by coconeOfRepresentable is a colimit: that is, we have exhibited an arbitrary presheaf P as a colimit of representables.

The result of [MM92], Chapter I, Section 5, Corollary 3.

Equations

• CategoryTheory.colimitOfRepresentable P = let_fun this := ⋯; CategoryTheory.Limits.IsColimit.ofPointIso (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.functorToRepresentables P))

noncomputable def CategoryTheory.natIsoOfNatIsoOnRepresentables {C : Type u₁} [CategoryTheory.SmallCategory C] {ℰ : Type u₂} [CategoryTheory.Category.{u₁, u₂} ℰ] (L₁ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type u₁)) ℰ) (L₂ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type u₁)) ℰ) [CategoryTheory.Limits.PreservesColimits L₁] [CategoryTheory.Limits.PreservesColimits L₂] (h : CategoryTheory.Functor.comp CategoryTheory.yoneda L₁ ≅ CategoryTheory.Functor.comp CategoryTheory.yoneda L₂) : L₁ ≅ L₂

Given two functors L₁ and L₂ which preserve colimits, if they agree when restricted to the representable presheaves then they agree everywhere.

Equations

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

noncomputable def CategoryTheory.uniqueExtensionAlongYoneda {C : Type u₁} [CategoryTheory.SmallCategory C] {ℰ : Type u₂} [CategoryTheory.Category.{u₁, u₂} ℰ] (A : CategoryTheory.Functor C ℰ) [CategoryTheory.Limits.HasColimits ℰ] (L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type u₁)) ℰ) (hL : CategoryTheory.Functor.comp CategoryTheory.yoneda L ≅ A) [CategoryTheory.Limits.PreservesColimits L] : L ≅ CategoryTheory.ColimitAdj.extendAlongYoneda A

Show that extendAlongYoneda is the unique colimit-preserving functor which extends A to the presheaf category.

The second part of [MM92], Chapter I, Section 5, Corollary 4. See Property 3 of https://ncatlab.org/nlab/show/Yoneda+extension#properties.

Equations

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

noncomputable def CategoryTheory.isLeftAdjointOfPreservesColimitsAux {C : Type u₁} [CategoryTheory.SmallCategory C] {ℰ : Type u₂} [CategoryTheory.Category.{u₁, u₂} ℰ] [CategoryTheory.Limits.HasColimits ℰ] (L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type u₁)) ℰ) [CategoryTheory.Limits.PreservesColimits L] : CategoryTheory.IsLeftAdjoint L

If L preserves colimits and ℰ has them, then it is a left adjoint. This is a special case of isLeftAdjointOfPreservesColimits used to prove that.

Equations

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

noncomputable def CategoryTheory.isLeftAdjointOfPreservesColimits {C : Type u₁} [CategoryTheory.SmallCategory C] {ℰ : Type u₂} [CategoryTheory.Category.{u₁, u₂} ℰ] [CategoryTheory.Limits.HasColimits ℰ] (L : CategoryTheory.Functor (CategoryTheory.Functor C (Type u₁)) ℰ) [CategoryTheory.Limits.PreservesColimits L] : CategoryTheory.IsLeftAdjoint L

If L preserves colimits and ℰ has them, then it is a left adjoint. Note this is a (partial) converse to leftAdjointPreservesColimits.

Equations

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

@[simp]

theorem CategoryTheory.tautologicalCocone_pt {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)) : (CategoryTheory.tautologicalCocone P).pt = P

@[simp]

theorem CategoryTheory.tautologicalCocone_ι_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)) (X : CategoryTheory.CostructuredArrow CategoryTheory.yoneda P) : (CategoryTheory.tautologicalCocone P).ι.app X = X.hom

def CategoryTheory.tautologicalCocone {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)) : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp (CategoryTheory.CostructuredArrow.proj CategoryTheory.yoneda P) CategoryTheory.yoneda)

For a presheaf P, consider the forgetful functor from the category of representable presheaves over P to the category of presheaves. There is a tautological cocone over this functor whose leg for a natural transformation V ⟶ P with V representable is just that natural transformation.

Equations

• CategoryTheory.tautologicalCocone P = { pt := P, ι := { app := fun (X : CategoryTheory.CostructuredArrow CategoryTheory.yoneda P) => X.hom, naturality := ⋯ } }

def CategoryTheory.isColimitTautologicalCocone {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)) : CategoryTheory.Limits.IsColimit (CategoryTheory.tautologicalCocone P)

The tautological cocone with point P is a colimit cocone, exhibiting P as a colimit of representables.

Proposition 2.6.3(i) in [Kashiwara2006]

Equations

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

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

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 [Kashiwara2006]