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

@[simp]

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

@[simp]

theorem CategoryTheory.Presheaf.restrictedYoneda_map_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [CategoryTheory.Category.{v₁, 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.Presheaf.restrictedYoneda A).map f).app X_1 a = CategoryTheory.CategoryStruct.comp a f

@[simp]

theorem CategoryTheory.Presheaf.restrictedYoneda_obj_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [CategoryTheory.Category.{v₁, 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.Presheaf.restrictedYoneda A).obj X).map f a = CategoryTheory.CategoryStruct.comp (A.map f.unop) a

def CategoryTheory.Presheaf.restrictedYoneda {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [CategoryTheory.Category.{v₁, u₂} ℰ] (A : CategoryTheory.Functor C ℰ) : CategoryTheory.Functor ℰ (CategoryTheory.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 v₁)).obj A.op)

def CategoryTheory.Presheaf.restrictedYonedaHomEquiv' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [CategoryTheory.Category.{v₁, u₂} ℰ] (A : CategoryTheory.Functor C ℰ) (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)) (E : ℰ) : ((CategoryTheory.CostructuredArrow.proj CategoryTheory.yoneda P).comp A ⟶ (CategoryTheory.Functor.const (CategoryTheory.CostructuredArrow CategoryTheory.yoneda P)).obj E) ≃ (P ⟶ (CategoryTheory.Presheaf.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₁} [CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [CategoryTheory.Category.{v₁, u₂} ℰ] {A : CategoryTheory.Functor C ℰ} [CategoryTheory.yoneda.HasPointwiseLeftKanExtension A] (L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) ℰ) (α : A ⟶ CategoryTheory.yoneda.comp L) [L.IsLeftKanExtension α] (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)) (E : ℰ) : (L.obj P ⟶ E) ≃ (P ⟶ (CategoryTheory.Presheaf.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₁} [CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [CategoryTheory.Category.{v₁, u₂} ℰ] {A : CategoryTheory.Functor C ℰ} [CategoryTheory.yoneda.HasPointwiseLeftKanExtension A] (L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) ℰ) (α : A ⟶ CategoryTheory.yoneda.comp L) [L.IsLeftKanExtension α] : L ⊣ CategoryTheory.Presheaf.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.

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

Any left Kan extension along the Yoneda embedding preserves colimits.

Equations

• CategoryTheory.Presheaf.preservesColimitsOfSizeOfIsLeftKanExtension L α = (CategoryTheory.Presheaf.yonedaAdjunction L α).leftAdjointPreservesColimits

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

noncomputable instance CategoryTheory.Presheaf.preservesColimitsOfSizeLeftKanExtension {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [CategoryTheory.Category.{v₁, u₂} ℰ] (A : CategoryTheory.Functor C ℰ) [CategoryTheory.yoneda.HasPointwiseLeftKanExtension A] : CategoryTheory.Limits.PreservesColimitsOfSize.{v₃, u₃, max v₁ u₁, v₁, max (v₁ + 1) u₁, u₂} (CategoryTheory.yoneda.leftKanExtension 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.

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

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.Presheaf.isExtensionAlongYoneda {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [CategoryTheory.Category.{v₁, u₂} ℰ] (A : CategoryTheory.Functor C ℰ) [CategoryTheory.yoneda.HasPointwiseLeftKanExtension A] : CategoryTheory.yoneda.comp (CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)) : CategoryTheory.Functor P.Elementsᵒᵖ (CategoryTheory.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

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.Presheaf.coconeOfRepresentable {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)) : CategoryTheory.Limits.Cocone (CategoryTheory.Presheaf.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 := ⋯ } }

theorem CategoryTheory.Presheaf.coconeOfRepresentable_naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P₁ : CategoryTheory.Functor Cᵒᵖ (Type v₁)} {P₂ : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (α : P₁ ⟶ P₂) (j : P₁.Elementsᵒᵖ) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Presheaf.coconeOfRepresentable P₁).ι.app j) α = (CategoryTheory.Presheaf.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.Presheaf.colimitOfRepresentable {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)) : CategoryTheory.Limits.IsColimit (CategoryTheory.Presheaf.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₁} [CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [CategoryTheory.Category.{v₁, u₂} ℰ] {A : CategoryTheory.Functor C ℰ} [CategoryTheory.yoneda.HasPointwiseLeftKanExtension A] (L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) ℰ) (α : A ⟶ CategoryTheory.yoneda.comp L) [L.IsLeftKanExtension α] : CategoryTheory.IsIso α

Equations

• ⋯ = ⋯

theorem CategoryTheory.Presheaf.isLeftKanExtension_along_yoneda_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [CategoryTheory.Category.{v₁, u₂} ℰ] {A : CategoryTheory.Functor C ℰ} [CategoryTheory.yoneda.HasPointwiseLeftKanExtension A] (L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) ℰ) (α : A ⟶ CategoryTheory.yoneda.comp L) : L.IsLeftKanExtension α ↔ CategoryTheory.IsIso α ∧ Nonempty (CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [CategoryTheory.Category.{v₁, u₂} ℰ] {A : CategoryTheory.Functor C ℰ} [CategoryTheory.yoneda.HasPointwiseLeftKanExtension A] (L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) ℰ) (e : A ≅ CategoryTheory.yoneda.comp L) [CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [CategoryTheory.Category.{v₁, u₂} ℰ] {A : CategoryTheory.Functor C ℰ} [CategoryTheory.yoneda.HasPointwiseLeftKanExtension A] (L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) ℰ) (e : A ≅ CategoryTheory.yoneda.comp L) [CategoryTheory.Limits.PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L] : L ≅ CategoryTheory.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

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

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

Equations

• ⋯ = ⋯

theorem CategoryTheory.Presheaf.isLeftAdjoint_of_preservesColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [CategoryTheory.Category.{v₁, u₂} ℰ] (L : CategoryTheory.Functor (CategoryTheory.Functor C (Type v₁)) ℰ) [CategoryTheory.Limits.PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L] [CategoryTheory.yoneda.HasPointwiseLeftKanExtension (CategoryTheory.yoneda.comp ((CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (F : CategoryTheory.Functor C D) (X : C) (Y : F.op.LeftExtension (CategoryTheory.yoneda.obj X)) : Unique (CategoryTheory.Functor.LeftExtension.mk (CategoryTheory.yoneda.obj (F.obj X)) (CategoryTheory.yonedaMap F X) ⟶ Y)

Equations

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

instance CategoryTheory.Presheaf.instIsLeftKanExtensionOppositeObjFunctorTypeYonedaYonedaMap {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : (CategoryTheory.yoneda.obj (F.obj X)).IsLeftKanExtension (CategoryTheory.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.

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (F : CategoryTheory.Functor C D) [∀ (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)), F.op.HasLeftKanExtension P] : F.comp CategoryTheory.yoneda ≅ CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (F : CategoryTheory.Functor C D) [∀ (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)), F.op.HasLeftKanExtension P] (X : C) : ((CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan F).inv.app X).app (Opposite.op (F.obj X)) ((F.op.lanUnit.app (CategoryTheory.yoneda.obj X)).app (Opposite.op X) (CategoryTheory.CategoryStruct.id X)) = CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.op (F.obj X)))

def CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.coconeApp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) (CategoryTheory.Functor Dᵒᵖ (Type v₁))} (φ : F.comp CategoryTheory.yoneda ⟶ CategoryTheory.yoneda.comp G) {P : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (x : P.Elements) : CategoryTheory.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_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) (CategoryTheory.Functor Dᵒᵖ (Type v₁))} (φ : F.comp CategoryTheory.yoneda ⟶ CategoryTheory.yoneda.comp G) {P : CategoryTheory.Functor Cᵒᵖ (Type v₁)} {x : P.Elements} {y : P.Elements} (f : x ⟶ y) {Z : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (h : F.op.comp (G.obj P) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map (↑f).unop) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.coconeApp φ x) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.coconeApp φ y) h

@[simp]

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

noncomputable def CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.presheafHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) (CategoryTheory.Functor Dᵒᵖ (Type v₁))} (φ : F.comp CategoryTheory.yoneda ⟶ CategoryTheory.yoneda.comp G) (P : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) (CategoryTheory.Functor Dᵒᵖ (Type v₁))} (φ : F.comp CategoryTheory.yoneda ⟶ CategoryTheory.yoneda.comp G) (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)) {X : C} (f : CategoryTheory.yoneda.obj X ⟶ P) : CategoryTheory.yonedaEquiv (CategoryTheory.CategoryStruct.comp f (CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.presheafHom φ P)) = (G.map f).app (Opposite.op (F.obj X)) ((φ.app X).app (Opposite.op (F.obj X)) (CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.op (F.obj X)))))

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

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.natTrans {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} [∀ (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)), F.op.HasLeftKanExtension P] {G : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) (CategoryTheory.Functor Dᵒᵖ (Type v₁))} (φ : F.comp CategoryTheory.yoneda ⟶ CategoryTheory.yoneda.comp G) : 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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} [∀ (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)), F.op.HasLeftKanExtension P] {G : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type v₁)) (CategoryTheory.Functor Dᵒᵖ (Type v₁))} (φ : F.comp CategoryTheory.yoneda ⟶ CategoryTheory.yoneda.comp G) (X : C) : (CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.natTrans φ).app (CategoryTheory.yoneda.obj X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan F).inv.app X) (φ.app X)

noncomputable def CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan.extensionHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} [∀ (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)), F.op.HasLeftKanExtension P] (Φ : CategoryTheory.yoneda.LeftExtension (F.comp CategoryTheory.yoneda)) : CategoryTheory.Functor.LeftExtension.mk F.op.lan (CategoryTheory.Presheaf.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] {F : CategoryTheory.Functor C D} [∀ (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)), F.op.HasLeftKanExtension P] {Φ : CategoryTheory.yoneda.LeftExtension (F.comp CategoryTheory.yoneda)} (f : CategoryTheory.Functor.LeftExtension.mk F.op.lan (CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan F).hom ⟶ Φ) (g : CategoryTheory.Functor.LeftExtension.mk F.op.lan (CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan F).hom ⟶ Φ) : f = g

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

Equations

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

instance CategoryTheory.Presheaf.instIsLeftKanExtensionFunctorOppositeTypeLanOpHomCompYonedaIsoYonedaCompLan {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (F : CategoryTheory.Functor C D) [∀ (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)), F.op.HasLeftKanExtension P] : F.op.lan.IsLeftKanExtension (CategoryTheory.Presheaf.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₁.

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

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

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

def CategoryTheory.Presheaf.isColimitTautologicalCocone {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)) : CategoryTheory.Limits.IsColimit (CategoryTheory.Presheaf.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₁} [CategoryTheory.Category.{v₁, u₁} C] {I : Type v₁} [CategoryTheory.SmallCategory I] (F : CategoryTheory.Functor I C) {c : CategoryTheory.Limits.Cocone (F.comp CategoryTheory.yoneda)} (hc : CategoryTheory.Limits.IsColimit c) : (c.toCostructuredArrow.comp (CategoryTheory.CostructuredArrow.pre F CategoryTheory.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]