Documentation

Mathlib.CategoryTheory.Limits.Presheaf

Colimit of representables #

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

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

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

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

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

Tags #

colimit, representable, presheaf, free cocompletion

References #

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

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

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

Instances For

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

    Instances For

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

      Instances For

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

        Instances For

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

          Instances For

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

            Instances For

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

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

              Instances For

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

                Instances For

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

                  Instances For

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

                    Instances For
                      @[simp]
                      theorem CategoryTheory.ColimitAdj.extendOfCompYonedaIsoLan_inv_app_app {C : Type u₁} [CategoryTheory.SmallCategory C] {D : Type u₁} [CategoryTheory.SmallCategory D] (F : CategoryTheory.Functor C D) (X : CategoryTheory.Functor Cᵒᵖ (Type u₁)) (x : Dᵒᵖ) :
                      @[simp]
                      theorem CategoryTheory.compYonedaIsoYonedaCompLan_inv_app_app {C : Type u₁} [CategoryTheory.SmallCategory C] {D : Type u₁} [CategoryTheory.SmallCategory D] (F : CategoryTheory.Functor C D) (X : C) (X : Dᵒᵖ) :
                      ∀ (a : ((CategoryTheory.Functor.comp CategoryTheory.yoneda (CategoryTheory.lan F.op)).obj X).obj X), Dᵒᵖ.app CategoryTheory.Category.opposite (Type u₁) CategoryTheory.types ((CategoryTheory.Functor.comp CategoryTheory.yoneda (CategoryTheory.lan F.op)).obj X) ((CategoryTheory.Functor.comp F CategoryTheory.yoneda).obj X) ((CategoryTheory.compYonedaIsoYonedaCompLan F).inv.app X) X a = Dᵒᵖ.app CategoryTheory.Category.opposite (Type u₁) CategoryTheory.types (CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.π (CategoryTheory.yoneda.obj X)).leftOp (CategoryTheory.Functor.comp F CategoryTheory.yoneda))) (CategoryTheory.yoneda.obj (F.obj X)) ((CategoryTheory.ColimitAdj.isExtensionAlongYoneda (CategoryTheory.Functor.comp F CategoryTheory.yoneda)).hom.app X) X (CategoryTheory.Limits.colimit.desc (CategoryTheory.Lan.diagram F.op (CategoryTheory.yoneda.obj X) X) { pt := (CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.π (CategoryTheory.yoneda.obj X)).leftOp (CategoryTheory.Functor.comp F CategoryTheory.yoneda))).obj X, ι := CategoryTheory.NatTrans.mk fun i => CategoryTheory.CategoryStruct.comp (((CategoryTheory.Adjunction.equivHomsetRightOfNatIso (CategoryTheory.isoWhiskerRight CategoryTheory.curriedYonedaLemma' ((CategoryTheory.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type u₁)).obj F.op)).symm).symm (↑(CategoryTheory.Adjunction.homEquiv (CategoryTheory.ColimitAdj.yonedaAdjunction (CategoryTheory.Functor.comp F CategoryTheory.yoneda)) (CategoryTheory.yoneda.obj X) (CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.π (CategoryTheory.yoneda.obj X)).leftOp (CategoryTheory.Functor.comp F CategoryTheory.yoneda)))) (CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.π (CategoryTheory.yoneda.obj X)).leftOp (CategoryTheory.Functor.comp F CategoryTheory.yoneda)))))).app i.left) ((CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp (CategoryTheory.CategoryOfElements.π (CategoryTheory.yoneda.obj X)).leftOp (CategoryTheory.Functor.comp F CategoryTheory.yoneda))).map i.hom) } a)
                      @[simp]
                      theorem CategoryTheory.compYonedaIsoYonedaCompLan_hom_app_app {C : Type u₁} [CategoryTheory.SmallCategory C] {D : Type u₁} [CategoryTheory.SmallCategory D] (F : CategoryTheory.Functor C D) (X : C) (X : Dᵒᵖ) :
                      ∀ (a : ((CategoryTheory.Functor.comp F CategoryTheory.yoneda).obj X).obj X), ((CategoryTheory.compYonedaIsoYonedaCompLan F).hom.app X).app X a = (CategoryTheory.coyoneda.preimage ((CategoryTheory.Adjunction.leftAdjointsCoyonedaEquiv (CategoryTheory.Adjunction.ofNatIsoRight (CategoryTheory.Lan.adjunction (Type u₁) F.op) (CategoryTheory.isoWhiskerRight CategoryTheory.curriedYonedaLemma' ((CategoryTheory.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type u₁)).obj F.op)).symm) (CategoryTheory.ColimitAdj.yonedaAdjunction (CategoryTheory.Functor.comp F CategoryTheory.yoneda))).hom.app (Opposite.op (CategoryTheory.yoneda.obj X)))).unop.app X (((CategoryTheory.ColimitAdj.isExtensionAlongYoneda (CategoryTheory.Functor.comp F CategoryTheory.yoneda)).inv.app X).app X a)

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

                      Instances For

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

                        Instances For

                          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.

                          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 [MM92], Chapter I, Section 5, Corollary 3.

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

                              An explicit formula for the legs of the cocone coconeOfRepresentable.

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

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

                              Instances For

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

                                Instances For

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

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

                                  Instances For

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

                                    Instances For

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

                                      Instances For

                                        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.

                                        Instances For

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

                                          Instances For