Documentation

Mathlib.CategoryTheory.Limits.Presheaf

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:

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 #

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
Instances For
    @[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✝ Y✝ : Cᵒᵖ} (f : X✝ Y✝) (a✝ : (CategoryTheory.yoneda.obj X).obj (A.op.obj 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 : Cᵒᵖ) (a✝ : (CategoryTheory.yoneda.obj X✝).obj (A.op.obj X)) :

    Auxiliary definition for restrictedYonedaHomEquiv.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      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 : ) :

      Auxiliary definition for yonedaAdjunction.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        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 α] :

        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.
        Instances For

          Any left Kan extension along the Yoneda embedding preserves colimits.

          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 α] :

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

          Equations
          • =
          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
          Instances For
            @[reducible]

            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
            Instances For

              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
              Instances For

                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.
                Instances For
                  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 α] :
                  Equations
                  • =
                  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
                  Instances For

                    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.

                    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.
                    Instances For
                      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.
                      Instances For
                        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.
                        Instances For
                          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) :
                          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))))
                          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} {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₁)), 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.
                          Instances For
                            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)) :

                            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
                            Instances For
                              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 g : CategoryTheory.Functor.LeftExtension.mk F.op.lan (CategoryTheory.Presheaf.compYonedaIsoYonedaCompLan F).hom Φ) :
                              f = g

                              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
                              • =

                              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
                              Instances For

                                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.
                                Instances For
                                  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]