Colimit of representables

This file constructs an adjunction Presheaf.yonedaAdjunction between (Cᵒᵖ ⥤ Type u) and ℰ given a functor A : C ⥤ ℰ, where the right adjoint restrictedYoneda sends (E : ℰ) to c ↦ (A.obj c ⟶ E), and the left adjoint (Cᵒᵖ ⥤ Type v₁) ⥤ ℰ is a pointwise left Kan extension of A along the Yoneda embedding, which exists provided ℰ has colimits)

We also 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. Two formulations are given:

• colimitOfRepresentable uses the category of elements of a functor to types;
• isColimitTautologicalCocone uses the category of costructured arrows.

In the lemma isLeftKanExtension_along_yoneda_iff, we show that if L : (Cᵒᵖ ⥤ Type v₁) ⥤ ℰ) and α : A ⟶ yoneda ⋙ L, then α makes L the left Kan extension of L along yoneda if and only if α is an isomorphism (i.e. L extends A) and L preserves colimits. uniqueExtensionAlongYoneda shows yoneda.leftKanExtension A is unique amongst functors preserving colimits with this property, establishing the presheaf category as the free cocompletion of a category.

Given a functor F : C ⥤ D, we also show construct an isomorphism compYonedaIsoYonedaCompLan : F ⋙ yoneda ≅ yoneda ⋙ F.op.lan, and show that it makes F.op.lan a left Kan extension of F ⋙ yoneda.

Tags

colimit, representable, presheaf, free cocompletion

References

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

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

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 [MLM92], Chapter I, Section 5, Theorem 2.

Equations

• CategoryTheory.Presheaf.restrictedYoneda A = CategoryTheory.yoneda.comp ((CategoryTheory.whiskeringLeft Cᵒᵖ ℰᵒᵖ (Type ?u.36)).obj A.op)

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Presheaf.restrictedYonedaHomEquiv' {C : Type u₁} [Category.{v₁, u₁} C] {ℰ : Type u₂} [Category.{v₁, u₂} ℰ] (A : Functor C ℰ) (P : Functor Cᵒᵖ (Type v₁)) (E : ℰ) : ((CostructuredArrow.proj yoneda P).comp A ⟶ (Functor.const (CostructuredArrow yoneda P)).obj E) ≃ (P ⟶ (restrictedYoneda A).obj E)

Auxiliary definition for restrictedYonedaHomEquiv.

Equations

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

noncomputable def CategoryTheory.Presheaf.restrictedYonedaHomEquiv {C : Type u₁} [Category.{v₁, u₁} C] {ℰ : Type u₂} [Category.{v₁, u₂} ℰ] {A : Functor C ℰ} [yoneda.HasPointwiseLeftKanExtension A] (L : Functor (Functor Cᵒᵖ (Type v₁)) ℰ) (α : A ⟶ yoneda.comp L) [L.IsLeftKanExtension α] (P : Functor Cᵒᵖ (Type v₁)) (E : ℰ) : (L.obj P ⟶ E) ≃ (P ⟶ (restrictedYoneda A).obj E)

Auxiliary definition for yonedaAdjunction.

Equations

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

noncomputable def CategoryTheory.Presheaf.yonedaAdjunction {C : Type u₁} [Category.{v₁, u₁} C] {ℰ : Type u₂} [Category.{v₁, u₂} ℰ] {A : Functor C ℰ} [yoneda.HasPointwiseLeftKanExtension A] (L : Functor (Functor Cᵒᵖ (Type v₁)) ℰ) (α : A ⟶ yoneda.comp L) [L.IsLeftKanExtension α] : L ⊣ restrictedYoneda A

If L : (Cᵒᵖ ⥤ Type v₁) ⥤ ℰ is a pointwise left Kan extension of a functor A : C ⥤ ℰ along the Yoneda embedding, then L is a left adjoint of restrictedYoneda A : ℰ ⥤ Cᵒᵖ ⥤ Type v₁

Equations

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

theorem CategoryTheory.Presheaf.preservesColimitsOfSize_of_isLeftKanExtension {C : Type u₁} [Category.{v₁, u₁} C] {ℰ : Type u₂} [Category.{v₁, u₂} ℰ] {A : Functor C ℰ} [yoneda.HasPointwiseLeftKanExtension A] (L : Functor (Functor Cᵒᵖ (Type v₁)) ℰ) (α : A ⟶ yoneda.comp L) [L.IsLeftKanExtension α] : Limits.PreservesColimitsOfSize.{v₃, u₃, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L

Any left Kan extension along the Yoneda embedding preserves colimits.

theorem CategoryTheory.Presheaf.isIso_of_isLeftKanExtension {C : Type u₁} [Category.{v₁, u₁} C] {ℰ : Type u₂} [Category.{v₁, u₂} ℰ] {A : Functor C ℰ} [yoneda.HasPointwiseLeftKanExtension A] (L : Functor (Functor Cᵒᵖ (Type v₁)) ℰ) (α : A ⟶ yoneda.comp L) [L.IsLeftKanExtension α] : IsIso α

instance CategoryTheory.Presheaf.preservesColimitsOfSize_leftKanExtension {C : Type u₁} [Category.{v₁, u₁} C] {ℰ : Type u₂} [Category.{v₁, u₂} ℰ] (A : Functor C ℰ) [yoneda.HasPointwiseLeftKanExtension A] : Limits.PreservesColimitsOfSize.{v₃, u₃, max v₁ u₁, v₁, max (v₁ + 1) u₁, u₂} (yoneda.leftKanExtension A)

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

instance CategoryTheory.Presheaf.instIsIsoFunctorLeftKanExtensionUnitOppositeTypeYoneda {C : Type u₁} [Category.{v₁, u₁} C] {ℰ : Type u₂} [Category.{v₁, u₂} ℰ] (A : Functor C ℰ) [yoneda.HasPointwiseLeftKanExtension A] : IsIso (yoneda.leftKanExtensionUnit A)

noncomputable def CategoryTheory.Presheaf.isExtensionAlongYoneda {C : Type u₁} [Category.{v₁, u₁} C] {ℰ : Type u₂} [Category.{v₁, u₂} ℰ] (A : Functor C ℰ) [yoneda.HasPointwiseLeftKanExtension A] : yoneda.comp (yoneda.leftKanExtension A) ≅ A

A pointwise left Kan extension along the Yoneda embedding is an extension.

Equations

• CategoryTheory.Presheaf.isExtensionAlongYoneda A = (CategoryTheory.asIso (CategoryTheory.yoneda.leftKanExtensionUnit A)).symm

@[reducible]

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

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.Presheaf.functorToRepresentables P = (CategoryTheory.CategoryOfElements.π P).leftOp.comp CategoryTheory.yoneda

noncomputable def CategoryTheory.Presheaf.coconeOfRepresentable {C : Type u₁} [Category.{v₁, u₁} C] (P : Functor Cᵒᵖ (Type v₁)) : Limits.Cocone (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 [MLM92], Chapter I, Section 5, Corollary 3.

Equations

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

@[simp]

theorem CategoryTheory.Presheaf.coconeOfRepresentable_ι_app {C : Type u₁} [Category.{v₁, u₁} C] (P : Functor Cᵒᵖ (Type v₁)) (x : P.Elementsᵒᵖ) : (coconeOfRepresentable P).ι.app x = yonedaEquiv.symm (Opposite.unop x).snd

@[simp]

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

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

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

noncomputable def CategoryTheory.Presheaf.colimitOfRepresentable {C : Type u₁} [Category.{v₁, u₁} C] (P : Functor Cᵒᵖ (Type v₁)) : Limits.IsColimit (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 [MLM92], Chapter I, Section 5, Corollary 3.

Equations

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

instance CategoryTheory.Presheaf.instIsIsoFunctorOfIsLeftKanExtensionOppositeType {C : Type u₁} [Category.{v₁, u₁} C] {ℰ : Type u₂} [Category.{v₁, u₂} ℰ] {A : Functor C ℰ} [yoneda.HasPointwiseLeftKanExtension A] (L : Functor (Functor Cᵒᵖ (Type v₁)) ℰ) (α : A ⟶ yoneda.comp L) [L.IsLeftKanExtension α] : IsIso α

theorem CategoryTheory.Presheaf.isLeftKanExtension_along_yoneda_iff {C : Type u₁} [Category.{v₁, u₁} C] {ℰ : Type u₂} [Category.{v₁, u₂} ℰ] {A : Functor C ℰ} [yoneda.HasPointwiseLeftKanExtension A] (L : Functor (Functor Cᵒᵖ (Type v₁)) ℰ) (α : A ⟶ yoneda.comp L) : L.IsLeftKanExtension α ↔ IsIso α ∧ Limits.PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L

theorem CategoryTheory.Presheaf.isLeftKanExtension_of_preservesColimits {C : Type u₁} [Category.{v₁, u₁} C] {ℰ : Type u₂} [Category.{v₁, u₂} ℰ] {A : Functor C ℰ} [yoneda.HasPointwiseLeftKanExtension A] (L : Functor (Functor Cᵒᵖ (Type v₁)) ℰ) (e : A ≅ yoneda.comp L) [Limits.PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L] : L.IsLeftKanExtension e.hom

noncomputable def CategoryTheory.Presheaf.uniqueExtensionAlongYoneda {C : Type u₁} [Category.{v₁, u₁} C] {ℰ : Type u₂} [Category.{v₁, u₂} ℰ] {A : Functor C ℰ} [yoneda.HasPointwiseLeftKanExtension A] (L : Functor (Functor Cᵒᵖ (Type v₁)) ℰ) (e : A ≅ yoneda.comp L) [Limits.PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L] : L ≅ yoneda.leftKanExtension A

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

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

Equations

• CategoryTheory.Presheaf.uniqueExtensionAlongYoneda L e = L.leftKanExtensionUnique e.hom (CategoryTheory.yoneda.leftKanExtension A) (CategoryTheory.yoneda.leftKanExtensionUnit A)

instance CategoryTheory.Presheaf.instIsLeftKanExtensionFunctorOppositeTypeIdCompYonedaOfPreservesColimitsOfSizeOfHasPointwiseLeftKanExtension {C : Type u₁} [Category.{v₁, u₁} C] {ℰ : Type u₂} [Category.{v₁, u₂} ℰ] (L : Functor (Functor Cᵒᵖ (Type v₁)) ℰ) [Limits.PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L] [yoneda.HasPointwiseLeftKanExtension (yoneda.comp L)] : L.IsLeftKanExtension (CategoryStruct.id (yoneda.comp L))

theorem CategoryTheory.Presheaf.isLeftAdjoint_of_preservesColimits {C : Type u₁} [Category.{v₁, u₁} C] {ℰ : Type u₂} [Category.{v₁, u₂} ℰ] (L : Functor (Functor C (Type v₁)) ℰ) [Limits.PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L] [yoneda.HasPointwiseLeftKanExtension (yoneda.comp ((opOpEquivalence C).congrLeft.functor.comp L))] : L.IsLeftAdjoint

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

instance CategoryTheory.Presheaf.instUniqueHomLeftExtensionOppositeOpObjFunctorTypeYonedaMkYonedaMap {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₁, u₂} D] (F : Functor C D) (X : C) (Y : F.op.LeftExtension (yoneda.obj X)) : Unique (Functor.LeftExtension.mk (yoneda.obj (F.obj X)) (yonedaMap F X) ⟶ Y)

Equations

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

instance CategoryTheory.Presheaf.instIsLeftKanExtensionOppositeObjFunctorTypeYonedaYonedaMap {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₁, u₂} D] (F : Functor C D) (X : C) : (yoneda.obj (F.obj X)).IsLeftKanExtension (yonedaMap F X)

Given F : C ⥤ D and X : C, yoneda.obj (F.obj X) : Dᵒᵖ ⥤ Type _ is the left Kan extension of yoneda.obj X : Cᵒᵖ ⥤ Type _ along F.op.

noncomputable def CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₁, u₂} D] (F : Functor C D) [∀ (P : Functor Cᵒᵖ (Type v₁)), F.op.HasLeftKanExtension P] : F.comp yoneda ≅ yoneda.comp F.op.lan

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

Equations

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

@[simp]

theorem CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan_inv_app_app_apply_eq_id {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₁, u₂} D] (F : Functor C D) [∀ (P : Functor Cᵒᵖ (Type v₁)), F.op.HasLeftKanExtension P] (X : C) : ((compYonedaIsoYonedaCompLan F).inv.app X).app (Opposite.op (F.obj X)) ((F.op.lanUnit.app (yoneda.obj X)).app (Opposite.op X) (CategoryStruct.id X)) = CategoryStruct.id (Opposite.unop (Opposite.op (F.obj X)))

def CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.coconeApp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor (Functor Cᵒᵖ (Type v₁)) (Functor Dᵒᵖ (Type v₁))} (φ : F.comp yoneda ⟶ yoneda.comp G) {P : Functor Cᵒᵖ (Type v₁)} (x : P.Elements) : yoneda.obj (Opposite.unop x.fst) ⟶ F.op.comp (G.obj P)

Auxiliary definition for presheafHom.

Equations

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

@[simp]

theorem CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.coconeApp_naturality {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor (Functor Cᵒᵖ (Type v₁)) (Functor Dᵒᵖ (Type v₁))} (φ : F.comp yoneda ⟶ yoneda.comp G) {P : Functor Cᵒᵖ (Type v₁)} {x y : P.Elements} (f : x ⟶ y) : CategoryStruct.comp (yoneda.map (↑f).unop) (coconeApp φ x) = coconeApp φ y

@[simp]

theorem CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.coconeApp_naturality_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor (Functor Cᵒᵖ (Type v₁)) (Functor Dᵒᵖ (Type v₁))} (φ : F.comp yoneda ⟶ yoneda.comp G) {P : Functor Cᵒᵖ (Type v₁)} {x y : P.Elements} (f : x ⟶ y) {Z : Functor Cᵒᵖ (Type v₁)} (h : F.op.comp (G.obj P) ⟶ Z) : CategoryStruct.comp (yoneda.map (↑f).unop) (CategoryStruct.comp (coconeApp φ x) h) = CategoryStruct.comp (coconeApp φ y) h

noncomputable def CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.presheafHom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor (Functor Cᵒᵖ (Type v₁)) (Functor Dᵒᵖ (Type v₁))} (φ : F.comp yoneda ⟶ yoneda.comp G) (P : Functor Cᵒᵖ (Type v₁)) : P ⟶ F.op.comp (G.obj P)

Given functors F : C ⥤ D and G : (Cᵒᵖ ⥤ Type v₁) ⥤ (Dᵒᵖ ⥤ Type v₁), and a natural transformation φ : F ⋙ yoneda ⟶ yoneda ⋙ G, this is the (natural) morphism P ⟶ F.op ⋙ G.obj P for all P : Cᵒᵖ ⥤ Type v₁ that is determined by φ.

Equations

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

theorem CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.yonedaEquiv_ι_presheafHom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor (Functor Cᵒᵖ (Type v₁)) (Functor Dᵒᵖ (Type v₁))} (φ : F.comp yoneda ⟶ yoneda.comp G) (P : Functor Cᵒᵖ (Type v₁)) {X : C} (f : yoneda.obj X ⟶ P) : yonedaEquiv (CategoryStruct.comp f (presheafHom φ P)) = (G.map f).app (Opposite.op (F.obj X)) ((φ.app X).app (Opposite.op (F.obj X)) (CategoryStruct.id (Opposite.unop (Opposite.op (F.obj X)))))

theorem CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.yonedaEquiv_presheafHom_yoneda_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor (Functor Cᵒᵖ (Type v₁)) (Functor Dᵒᵖ (Type v₁))} (φ : F.comp yoneda ⟶ yoneda.comp G) (X : C) : yonedaEquiv (presheafHom φ (yoneda.obj X)) = (φ.app X).app (F.op.obj (Opposite.op X)) (CategoryStruct.id (Opposite.unop (F.op.obj (Opposite.op X))))

@[simp]

theorem CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.presheafHom_naturality {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor (Functor Cᵒᵖ (Type v₁)) (Functor Dᵒᵖ (Type v₁))} (φ : F.comp yoneda ⟶ yoneda.comp G) {P Q : Functor Cᵒᵖ (Type v₁)} (f : P ⟶ Q) : CategoryStruct.comp (presheafHom φ P) (whiskerLeft F.op (G.map f)) = CategoryStruct.comp f (presheafHom φ Q)

@[simp]

theorem CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.presheafHom_naturality_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor (Functor Cᵒᵖ (Type v₁)) (Functor Dᵒᵖ (Type v₁))} (φ : F.comp yoneda ⟶ yoneda.comp G) {P Q : Functor Cᵒᵖ (Type v₁)} (f : P ⟶ Q) {Z : Functor Cᵒᵖ (Type v₁)} (h : F.op.comp (G.obj Q) ⟶ Z) : CategoryStruct.comp (presheafHom φ P) (CategoryStruct.comp (whiskerLeft F.op (G.map f)) h) = CategoryStruct.comp f (CategoryStruct.comp (presheafHom φ Q) h)

noncomputable def CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.natTrans {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor (Functor Cᵒᵖ (Type v₁)) (Functor Dᵒᵖ (Type v₁))} (φ : F.comp yoneda ⟶ yoneda.comp G) [∀ (P : Functor Cᵒᵖ (Type v₁)), F.op.HasLeftKanExtension P] : F.op.lan ⟶ G

Given functors F : C ⥤ D and G : (Cᵒᵖ ⥤ Type v₁) ⥤ (Dᵒᵖ ⥤ Type v₁), and a natural transformation φ : F ⋙ yoneda ⟶ yoneda ⋙ G, this is the canonical natural transformation F.op.lan ⟶ G, which is part of the that F.op.lan : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁ is the left Kan extension of F ⋙ yoneda : C ⥤ Dᵒᵖ ⥤ Type v₁ along yoneda : C ⥤ Cᵒᵖ ⥤ Type v₁.

Equations

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

theorem CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.natTrans_app_yoneda_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₁, u₂} D] {F : Functor C D} {G : Functor (Functor Cᵒᵖ (Type v₁)) (Functor Dᵒᵖ (Type v₁))} (φ : F.comp yoneda ⟶ yoneda.comp G) [∀ (P : Functor Cᵒᵖ (Type v₁)), F.op.HasLeftKanExtension P] (X : C) : (natTrans φ).app (yoneda.obj X) = CategoryStruct.comp ((compYonedaIsoYonedaCompLan F).inv.app X) (φ.app X)

noncomputable def CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.extensionHom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₁, u₂} D] {F : Functor C D} [∀ (P : Functor Cᵒᵖ (Type v₁)), F.op.HasLeftKanExtension P] (Φ : yoneda.LeftExtension (F.comp yoneda)) : Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom ⟶ Φ

Given a functor F : C ⥤ D, this definition is part of the verification that Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom is universal, i.e. that F.op.lan : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁ is the left Kan extension of F ⋙ yoneda : C ⥤ Dᵒᵖ ⥤ Type v₁ along yoneda : C ⥤ Cᵒᵖ ⥤ Type v₁.

Equations

• CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.extensionHom Φ = CategoryTheory.StructuredArrow.homMk (CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.natTrans Φ.hom) ⋯

theorem CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.hom_ext {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₁, u₂} D] {F : Functor C D} [∀ (P : Functor Cᵒᵖ (Type v₁)), F.op.HasLeftKanExtension P] {Φ : yoneda.LeftExtension (F.comp yoneda)} (f g : Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom ⟶ Φ) : f = g

theorem CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.hom_ext_iff {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₁, u₂} D] {F : Functor C D} [∀ (P : Functor Cᵒᵖ (Type v₁)), F.op.HasLeftKanExtension P] {Φ : yoneda.LeftExtension (F.comp yoneda)} {f g : Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom ⟶ Φ} : f = g ↔ True

noncomputable instance CategoryTheory.Presheaf.instUniqueHomLeftExtensionFunctorOppositeTypeYonedaCompMkLanOpHomCompYonedaIsoYonedaCompLan {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₁, u₂} D] (F : Functor C D) [∀ (P : Functor Cᵒᵖ (Type v₁)), F.op.HasLeftKanExtension P] (Φ : StructuredArrow (F.comp yoneda) ((whiskeringLeft C (Functor Cᵒᵖ (Type v₁)) (Functor Dᵒᵖ (Type v₁))).obj yoneda)) : Unique (Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom ⟶ Φ)

Equations

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

instance CategoryTheory.Presheaf.instIsLeftKanExtensionFunctorOppositeTypeLanOpHomCompYonedaIsoYonedaCompLan {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₁, u₂} D] (F : Functor C D) [∀ (P : Functor Cᵒᵖ (Type v₁)), F.op.HasLeftKanExtension P] : F.op.lan.IsLeftKanExtension (compYonedaIsoYonedaCompLan F).hom

Given a functor F : C ⥤ D, F.op.lan : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁ is the left Kan extension of F ⋙ yoneda : C ⥤ Dᵒᵖ ⥤ Type v₁ along yoneda : C ⥤ Cᵒᵖ ⥤ Type v₁.

def CategoryTheory.Presheaf.tautologicalCocone {C : Type u₁} [Category.{v₁, u₁} C] (P : Functor Cᵒᵖ (Type v₁)) : Limits.Cocone ((CostructuredArrow.proj yoneda P).comp 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.Presheaf.tautologicalCocone P = { pt := P, ι := { app := fun (X : CategoryTheory.CostructuredArrow CategoryTheory.yoneda P) => X.hom, naturality := ⋯ } }

@[simp]

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

@[simp]

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

def CategoryTheory.Presheaf.isColimitTautologicalCocone {C : Type u₁} [Category.{v₁, u₁} C] (P : Functor Cᵒᵖ (Type v₁)) : Limits.IsColimit (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 [KS06]

Equations

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

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]