Colimit of representables

All the definitions in this file are deprecated. The results from this file are now in the folder Mathlib/CategoryTheory/Functor/KanExtension/. In particular, the fact that any presheaf of types is a colimit of representable presheaves is now proven in the fil Mathlib/CategoryTheory/Functor/KanExtension/DenseAtYoneda.lean.

In this file, We show that every presheaf of types on a category C (with Category.{v₁} C) is a colimit of representables. This result is also known as the density theorem, the co-Yoneda lemma and the Ninja Yoneda lemma. Three formulations are given:

• colimitOfRepresentable uses the category of elements of a functor to types;
• isColimitTautologicalCocone uses the category of costructured arrows for yoneda : C ⥤ Cᵒᵖ ⥤ Type v₁;
• isColimitTautologicalCocone' uses the category of costructured arrows for uliftYoneda : C ⥤ Cᵒᵖ ⥤ Type max w v₁, when the presheaf has values in Type max w v₁;

In this file, we also study the left Kan extensions of functors A : C ⥤ ℰ along the Yoneda embedding uliftYoneda : C ⥤ Cᵒᵖ ⥤ Type max w v₁ v₂ (when Category.{v₂} ℰ and w is an auxiliary universe). In particular, the definition uliftYonedaAdjunction shows that such a pointwise left Kan extension (which exists when ℰ has colimits) is a left adjoint to the functor restrictedULiftYoneda : ℰ ⥤ Cᵒᵖ ⥤ Type max w v₁ v₂.

In the lemma isLeftKanExtension_along_uliftYoneda_iff, we show that if L : (Cᵒᵖ ⥤ Type max w v₁ v₂) ⥤ ℰ and α : A ⟶ uliftYoneda ⋙ 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. uniqueExtensionAlongULiftYoneda shows uliftYoneda.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 compULiftYonedaIsoULiftYonedaCompLan : F ⋙ uliftYoneda ≅ uliftYoneda ⋙ F.op.lan, and show that it makes F.op.lan a left Kan extension of F ⋙ uliftYoneda.

Tags

colimit, representable, presheaf, free cocompletion

References

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

@[deprecated "use `restrictedShrinkYonedaHomEquivAux` instead." (since := "2026-08-17")]

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

Auxiliary definition for restrictedULiftYonedaHomEquiv.

Equations

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

@[deprecated "Use `restrictedShrinkYonedaHomEquiv_symm_naturality_right` instead." (since := "2026-08-17")]

theorem CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv'_symm_naturality_right {C : Type u₁} [Category.{v₁, u₁} C] {ℰ : Type u₂} [Category.{v₂, u₂} ℰ] (A : Functor C ℰ) (P : Functor Cᵒᵖ (Type (max w v₁ v₂))) {E E' : ℰ} (g : E ⟶ E') (f : P ⟶ (restrictedULiftYoneda A).obj E) : (restrictedULiftYonedaHomEquiv' A P E').symm (CategoryStruct.comp f ((restrictedULiftYoneda A).map g)) = CategoryStruct.comp ((restrictedULiftYonedaHomEquiv' A P E).symm f) ((Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).map g)

theorem CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv'_symm_naturality_right_assoc {C : Type u₁} [Category.{v₁, u₁} C] {ℰ : Type u₂} [Category.{v₂, u₂} ℰ] (A : Functor C ℰ) (P : Functor Cᵒᵖ (Type (max w v₁ v₂))) {E E' : ℰ} (g : E ⟶ E') (f : P ⟶ (restrictedULiftYoneda A).obj E) {Z : Functor (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P) ℰ} (h : (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E' ⟶ Z) : CategoryStruct.comp ((restrictedULiftYonedaHomEquiv' A P E').symm (CategoryStruct.comp f ((restrictedULiftYoneda A).map g))) h = CategoryStruct.comp ((restrictedULiftYonedaHomEquiv' A P E).symm f) (CategoryStruct.comp ((Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).map g) h)

@[deprecated "Use `restrictedShrinkYonedaHomEquiv_symm_naturality_left`" (since := "2026-08-17")]

theorem CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv'_symm_app_naturality_left {C : Type u₁} [Category.{v₁, u₁} C] {ℰ : Type u₂} [Category.{v₂, u₂} ℰ] (A : Functor C ℰ) {P Q : Functor Cᵒᵖ (Type (max w v₁ v₂))} (f : P ⟶ Q) (E : ℰ) (g : Q ⟶ (restrictedULiftYoneda A).obj E) (p : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P) : ((restrictedULiftYonedaHomEquiv' A P E).symm (CategoryStruct.comp f g)).app p = ((restrictedULiftYonedaHomEquiv' A Q E).symm g).app ((CostructuredArrow.map f).obj p)

theorem CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv'_symm_app_naturality_left_assoc {C : Type u₁} [Category.{v₁, u₁} C] {ℰ : Type u₂} [Category.{v₂, u₂} ℰ] (A : Functor C ℰ) {P Q : Functor Cᵒᵖ (Type (max w v₁ v₂))} (f : P ⟶ Q) (E : ℰ) (g : Q ⟶ (restrictedULiftYoneda A).obj E) (p : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P) {Z : ℰ} (h : ((Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E).obj p ⟶ Z) : CategoryStruct.comp (((restrictedULiftYonedaHomEquiv' A P E).symm (CategoryStruct.comp f g)).app p) h = CategoryStruct.comp (((restrictedULiftYonedaHomEquiv' A Q E).symm g).app ((CostructuredArrow.map f).obj p)) h

@[deprecated "Use `restrictedULiftYonedaAdjunction`" (since := "2026-08-27")]

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

Auxiliary definition for uliftYonedaAdjunction.

Equations

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

@[deprecated CategoryTheory.Presheaf.restrictedULiftYonedaAdjunction (since := "2026-08-17")]

noncomputable def CategoryTheory.Presheaf.uliftYonedaAdjunction {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor (Functor Cᵒᵖ (Type (max w v₁ v₂))) D} {A : Functor C D} [uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A] (α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁}.comp L) [L.IsLeftKanExtension α] : L ⊣ restrictedULiftYoneda A

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

Equations

• @CategoryTheory.Presheaf.uliftYonedaAdjunction = @CategoryTheory.Presheaf.restrictedULiftYonedaAdjunction

@[deprecated CategoryTheory.Presheaf.restrictedULiftYonedaAdjunction_unit_app_app (since := "2026-08-17")]

theorem CategoryTheory.Presheaf.uliftYonedaAdjunction_unit_app_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor (Functor Cᵒᵖ (Type (max w v₁ v₂))) D} {A : Functor C D} [uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A] (α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁}.comp L) [L.IsLeftKanExtension α] (P : Functor Cᵒᵖ (Type (max w v₁ v₂))) {X : Cᵒᵖ} (x : P.obj X) : (ConcreteCategory.hom (((restrictedULiftYonedaAdjunction α).unit.app P).app X)) x = { down := CategoryStruct.comp (α.app (Opposite.unop X)) (L.map (uliftYonedaEquiv.symm x)) }

Alias of CategoryTheory.Presheaf.restrictedULiftYonedaAdjunction_unit_app_app.

@[deprecated CategoryTheory.Presheaf.restrictedULiftYonedaAdjunction_homEquiv_app (since := "2026-08-17")]

theorem CategoryTheory.Presheaf.uliftYonedaAdjunction_homEquiv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor (Functor Cᵒᵖ (Type (max w v₁ v₂))) D} {A : Functor C D} [uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A] (α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁}.comp L) [L.IsLeftKanExtension α] {P : Functor Cᵒᵖ (Type (max w v₁ v₂))} {Y : D} (f : L.obj P ⟶ Y) {Z : Cᵒᵖ} (z : P.obj Z) : (ConcreteCategory.hom ((((restrictedULiftYonedaAdjunction α).homEquiv P Y) f).app Z)) z = { down := CategoryStruct.comp (α.app (Opposite.unop Z)) (CategoryStruct.comp (L.map (uliftYonedaEquiv.symm z)) f) }

Alias of CategoryTheory.Presheaf.restrictedULiftYonedaAdjunction_homEquiv_app.

@[deprecated "No replacement" (since := "2026-08-17")]

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

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

Equations

• CategoryTheory.Presheaf.isExtensionAlongULiftYoneda A = (CategoryTheory.asIso (CategoryTheory.uliftYoneda.{max ?u.3 ?u.5, ?u.4, ?u.2}.leftKanExtensionUnit A)).symm

@[deprecated "See `denseAtUliftYoneda`" (since := "2026-08-17")]

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

Given P : Cᵒᵖ ⥤ Type max w v₁, this is the functor from the opposite category of the category of elements of X which sends an element in P.obj (op X) to the presheaf represented by X. The definition coconeOfRepresentable gives a cocone for this functor which is a colimit and has point P.

Equations

• CategoryTheory.Presheaf.functorToRepresentables P = (CategoryTheory.Functor.Elements.π P).leftOp.comp CategoryTheory.uliftYoneda.{?u.3, ?u.2, ?u.1}

@[simp]

theorem CategoryTheory.Presheaf.functorToRepresentables_map {C : Type u₁} [Category.{v₁, u₁} C] (P : Functor Cᵒᵖ (Type (max w v₁))) {X✝ Y✝ : P.Elementsᵒᵖ} (f : X✝ ⟶ Y✝) : (functorToRepresentables P).map f = uliftYoneda.{w, v₁, u₁}.map f.unop.hom.unop

@[simp]

theorem CategoryTheory.Presheaf.functorToRepresentables_obj {C : Type u₁} [Category.{v₁, u₁} C] (P : Functor Cᵒᵖ (Type (max w v₁))) (X : P.Elementsᵒᵖ) : (functorToRepresentables P).obj X = uliftYoneda.{w, v₁, u₁}.obj (Opposite.unop (Opposite.unop X).obj)

@[deprecated "See `denseAtUliftYoneda`" (since := "2026-08-17")]

def CategoryTheory.Presheaf.coconeOfRepresentable {C : Type u₁} [Category.{v₁, u₁} C] (P : Functor Cᵒᵖ (Type (max w 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.uliftYonedaEquiv.symm (Opposite.unop x).val, naturality := ⋯ } }

@[simp]

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

@[simp]

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

@[deprecated "No replacement" (since := "2026-08-17")]

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

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

@[deprecated CategoryTheory.denseAtUliftYoneda (since := "2026-08-17")]

def CategoryTheory.Presheaf.colimitOfRepresentable {C : Type u₁} [Category.{v₁, u₁} C] (P : Functor Cᵒᵖ (Type (max w 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.

@[deprecated CategoryTheory.Presheaf.isLeftKanExtension_along_uliftYoneda_of_preservesColimits (since := "2026-08-18")]

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

Alias of CategoryTheory.Presheaf.isLeftKanExtension_along_uliftYoneda_of_preservesColimits.

@[deprecated "No replacement" (since := "2026-08-17")]

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

Show that uliftYoneda.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.

@[deprecated "No replacement." (since := "2026-08-23")]

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

Auxiliary definition for presheafHom.

Equations

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

@[simp, deprecated "No replacement." (since := "2026-08-23")]

theorem CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.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 (max w v₁ v₂))) (Functor Dᵒᵖ (Type (max w v₁ v₂)))} (φ : F.comp uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁}.comp G) {P : Functor Cᵒᵖ (Type (max w v₁ v₂))} {x y : P.Elements} (f : x ⟶ y) : CategoryStruct.comp (uliftYoneda.{max v₂ w, v₁, u₁}.map f.hom.unop) (coconeApp φ x) = coconeApp φ y

@[simp]

theorem CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.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 (max w v₁ v₂))) (Functor Dᵒᵖ (Type (max w v₁ v₂)))} (φ : F.comp uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁}.comp G) {P : Functor Cᵒᵖ (Type (max w v₁ v₂))} {x y : P.Elements} (f : x ⟶ y) {Z : Functor Cᵒᵖ (Type (max (max v₂ w) v₁))} (h : F.op.comp (G.obj P) ⟶ Z) : CategoryStruct.comp (uliftYoneda.{max v₂ w, v₁, u₁}.map f.hom.unop) (CategoryStruct.comp (coconeApp φ x) h) = CategoryStruct.comp (coconeApp φ y) h

@[deprecated "No replacement" (since := "2026-09-20")]

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

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

Equations

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

@[deprecated "No replacement" (since := "2026-09-20")]

theorem CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.uliftYonedaEquiv_ι_presheafHom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor (Functor Cᵒᵖ (Type (max w v₁ v₂))) (Functor Dᵒᵖ (Type (max w v₁ v₂)))} (φ : F.comp uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁}.comp G) (P : Functor Cᵒᵖ (Type (max w v₁ v₂))) {X : C} (f : uliftYoneda.{max w v₂, v₁, u₁}.obj X ⟶ P) : uliftYonedaEquiv (CategoryStruct.comp f (presheafHom φ P)) = (ConcreteCategory.hom ((G.map f).app (Opposite.op (F.obj X)))) ((ConcreteCategory.hom ((φ.app X).app (Opposite.op (F.obj X)))) { down := CategoryStruct.id (Opposite.unop (Opposite.op (F.obj X))) })

@[deprecated "No replacement" (since := "2026-09-20")]

theorem CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.uliftYonedaEquiv_presheafHom_uliftYoneda_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor (Functor Cᵒᵖ (Type (max w v₁ v₂))) (Functor Dᵒᵖ (Type (max w v₁ v₂)))} (φ : F.comp uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁}.comp G) (X : C) : uliftYonedaEquiv (presheafHom φ (uliftYoneda.{max w v₂, v₁, u₁}.obj X)) = (ConcreteCategory.hom ((φ.app X).app (F.op.obj (Opposite.op X)))) { down := CategoryStruct.id (Opposite.unop (F.op.obj (Opposite.op X))) }

@[deprecated "No replacement" (since := "2026-09-20")]

theorem CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.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 (max w v₁ v₂))) (Functor Dᵒᵖ (Type (max w v₁ v₂)))} (φ : F.comp uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁}.comp G) {P Q : Functor Cᵒᵖ (Type (max w v₁ v₂))} (f : P ⟶ Q) : CategoryStruct.comp (presheafHom φ P) (F.op.whiskerLeft (G.map f)) = CategoryStruct.comp f (presheafHom φ Q)

theorem CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.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 (max w v₁ v₂))) (Functor Dᵒᵖ (Type (max w v₁ v₂)))} (φ : F.comp uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁}.comp G) {P Q : Functor Cᵒᵖ (Type (max w v₁ v₂))} (f : P ⟶ Q) {Z : Functor Cᵒᵖ (Type (max w v₁ v₂))} (h : F.op.comp (G.obj Q) ⟶ Z) : CategoryStruct.comp (presheafHom φ P) (CategoryStruct.comp (F.op.whiskerLeft (G.map f)) h) = CategoryStruct.comp f (CategoryStruct.comp (presheafHom φ Q) h)

@[deprecated "No replacement" (since := "2026-08-23")]

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

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

Equations

• CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.natTrans φ = F.op.lan.descOfIsLeftKanExtension (CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan F).hom G φ

@[deprecated "No replacemenet" (since := "2026-08-23")]

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

@[deprecated "No replacement" (since := "2026-08-23")]

noncomputable def CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.presheafHom' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor (Functor Cᵒᵖ (Type (max w v₁ v₂))) (Functor Dᵒᵖ (Type (max w v₁ v₂)))} (φ : F.comp uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁}.comp G) [∀ (P : Functor Cᵒᵖ (Type (max w v₁ v₂))), F.op.HasLeftKanExtension P] (P : Functor Cᵒᵖ (Type (max w v₁ v₂))) : P ⟶ F.op.comp (G.obj P)

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

Equations

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

@[deprecated "No replacement" (since := "2026-08-23")]

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

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

Equations

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

@[deprecated "No replacement" (since := "2026-08-23")]

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

theorem CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.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 (max w v₁ v₂))), F.op.HasLeftKanExtension P] {Φ : uliftYoneda.{max w v₂, v₁, u₁}.LeftExtension (F.comp uliftYoneda.{max w v₁, v₂, u₂})} {f g : Functor.LeftExtension.mk F.op.lan (compULiftYonedaIsoULiftYonedaCompLan F).hom ⟶ Φ} : f = g ↔ True

@[deprecated "See `denseAtUliftYoneda`" (since := "2026-09-20")]

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

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. (In this version, we allow the presheaf P to have values in a larger universe.)

Equations

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

@[simp]

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

@[simp]

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

@[deprecated "denseAtUliftYoneda" (since := "2026-09-20")]

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

The tautological cocone with point P is a colimit cocone, exhibiting P as a colimit of representables. (In this version, we allow the presheaf P to have values in a larger universe.)

Proposition 2.6.3(i) in [KS06]

Equations

• CategoryTheory.Presheaf.isColimitTautologicalCocone' P = CategoryTheory.denseAtUliftYoneda P

@[deprecated "See `denseAtYoneda`" (since := "2026-09-20")]

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

@[deprecated "See `denseAtYoneda`" (since := "2026-09-20")]

noncomputable 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

• CategoryTheory.Presheaf.isColimitTautologicalCocone P = CategoryTheory.denseAtYoneda P

@[deprecated "Use shrinkCoyonedaCocone" (since := "2026-09-20")]

noncomputable def CategoryTheory.Functor.Elements.coconeπOpCompShrinkYonedaObj {C : Type u₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] (F : Functor C (Type w)) (X : C) : Limits.Cocone ((π F).op.comp (shrinkYoneda.{w, v₁, u₁}.obj X))

If F : C ⥤ Type w and C is locally w-small, then for any X : C, this is the colimit cocone which identifies F.obj X to the colimit of (CategoryOfElements.π F).op ⋙ shrinkYoneda.obj X.

Equations

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

@[simp]

theorem CategoryTheory.Functor.Elements.coconeπOpCompShrinkYonedaObj_ι_app {C : Type u₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] (F : Functor C (Type w)) (X : C) (u : F.Elementsᵒᵖ) : (coconeπOpCompShrinkYonedaObj F X).ι.app u = TypeCat.ofHom fun (t : ((π F).op.comp (shrinkYoneda.{w, v₁, u₁}.obj X)).obj u) => (ConcreteCategory.hom (F.map (shrinkYonedaObjObjEquiv t))) (Opposite.unop u).val

@[simp]

theorem CategoryTheory.Functor.Elements.coconeπOpCompShrinkYonedaObj_pt {C : Type u₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] (F : Functor C (Type w)) (X : C) : (coconeπOpCompShrinkYonedaObj F X).pt = F.obj X

@[deprecated CategoryTheory.Functor.Elements.isColimitShrinkCoyonedaCoconeObj (since := "2026-09-20")]

noncomputable def CategoryTheory.Functor.Elements.isColimitCoconeπOpCompShrinkYonedaObj {C : Type u₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] (F : Functor C (Type w)) (X : C) : Limits.IsColimit (coconeπOpCompShrinkYonedaObj F X)

If F : C ⥤ Type w and C is locally w-small, then for any X : C, F.obj X identifies to the colimit of (CategoryOfElements.π F).op ⋙ shrinkYoneda.obj X.

Equations

• CategoryTheory.Functor.Elements.isColimitCoconeπOpCompShrinkYonedaObj F X = CategoryTheory.Functor.Elements.isColimitShrinkCoyonedaCoconeObj F X

@[simp, deprecated CategoryTheory.Functor.Elements.shrinkYoneda_map_app_shrinkCoyonedaCocone_ι_app_app (since := "2026-09-20")]

theorem CategoryTheory.Functor.Elements.shrinkYoneda_map_app_coconeπOpCompShrinkYonedaObj_ι_app {C : Type u₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] (F : Functor C (Type w)) {X₁ X₂ : C} (f : X₁ ⟶ X₂) (u : F.Elements) : CategoryStruct.comp ((shrinkYoneda.{w, v₁, u₁}.map f).app (Opposite.op u.obj)) (TypeCat.ofHom fun (t : (shrinkYoneda.{w, v₁, u₁}.obj X₂).obj (Opposite.op u.obj)) => (ConcreteCategory.hom (F.map (shrinkYonedaObjObjEquiv t))) u.val) = CategoryStruct.comp (TypeCat.ofHom fun (t : (shrinkYoneda.{w, v₁, u₁}.obj X₁).obj (Opposite.op u.obj)) => (ConcreteCategory.hom (F.map (shrinkYonedaObjObjEquiv t))) u.val) (F.map f)

@[simp]

theorem CategoryTheory.Functor.Elements.shrinkYoneda_map_app_coconeπOpCompShrinkYonedaObj_ι_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] [LocallySmall.{w, v₁, u₁} C] (F : Functor C (Type w)) {X₁ X₂ : C} (f : X₁ ⟶ X₂) (u : F.Elements) {Z : Type w} (h : F.obj X₂ ⟶ Z) : CategoryStruct.comp ((shrinkYoneda.{w, v₁, u₁}.map f).app (Opposite.op u.obj)) (CategoryStruct.comp (TypeCat.ofHom fun (t : (shrinkYoneda.{w, v₁, u₁}.obj X₂).obj (Opposite.op u.obj)) => (ConcreteCategory.hom (F.map (shrinkYonedaObjObjEquiv t))) u.val) h) = CategoryStruct.comp (TypeCat.ofHom fun (t : (shrinkYoneda.{w, v₁, u₁}.obj X₁).obj (Opposite.op u.obj)) => (ConcreteCategory.hom (F.map (shrinkYonedaObjObjEquiv t))) u.val) (CategoryStruct.comp (F.map f) h)

@[deprecated CategoryTheory.Functor.Elements.shrinkCoyonedaCocone (since := "2026-09-20")]

noncomputable def CategoryTheory.Functor.Elements.coconeπOpCompShrinkYonedaFlip {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})

If C is a locally w-small category, this is a (colimit) cocone expressing F : C ⥤ Type w as a colimit of corepresentable functors.

Equations

• @CategoryTheory.Functor.Elements.coconeπOpCompShrinkYonedaFlip = @CategoryTheory.Functor.Elements.shrinkCoyonedaCocone

@[deprecated CategoryTheory.Functor.Elements.isColimitShrinkCoyonedaCocone (since := "2026-09-20")]

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

If F : C ⥤ Type w and C is locally w-small, then F identifies to the colimit of (CategoryOfElements.π F).op ⋙ shrinkYoneda.{w}.flip.

Equations

• @CategoryTheory.Functor.Elements.isColimitCoconeπOpCompShrinkYonedaFlip = @CategoryTheory.Functor.Elements.isColimitShrinkCoyonedaCocone

@[deprecated CategoryTheory.Functor.Elements.isInitialShrinkCoyonedaObj (since := "2026-09-20")]

noncomputable def CategoryTheory.Functor.Elements.isInitialElementsMkShrinkYonedaObjObjEquivId {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (A : Cᵒᵖ) : Limits.IsInitial (initialShrinkCoyonedaObj A)

Alias of CategoryTheory.Functor.Elements.isInitialShrinkCoyonedaObj.

Equations

• @CategoryTheory.Functor.Elements.isInitialElementsMkShrinkYonedaObjObjEquivId = @CategoryTheory.Functor.Elements.isInitialShrinkCoyonedaObj