Documentation

Mathlib.CategoryTheory.Comma.Presheaf.Basic

Computation of Over A for a presheaf A #

Let A : Cᵒᵖ ⥤ Type v be a presheaf. In this file, we construct an equivalence e : Over A ≌ (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v and show that there is a quasi-commutative diagram

CostructuredArrow yoneda A      ⥤      Over A

                             ⇘           ⥥

                               PSh(CostructuredArrow yoneda A)

where the top arrow is the forgetful functor forgetting the yoneda-costructure, the right arrow is the aforementioned equivalence and the diagonal arrow is the Yoneda embedding.

In the notation of Kashiwara-Schapira, the type of the equivalence is written C^ₐ ≌ Cₐ^, where ·ₐ is CostructuredArrow (with the functor S being either the identity or the Yoneda embedding) and ^ is taking presheaves. The equivalence is a key ingredient in various results in Kashiwara-Schapira.

The proof is somewhat long and technical, in part due to the construction inherently involving a sigma type which comes with the usual DTT issues. However, a user of this result should not need to interact with the actual construction, the mere existence of the equivalence and the commutative triangle should generally be sufficient.

Main results #

Implementation details #

The proof needs to introduce "correction terms" in various places in order to overcome DTT issues, and these need to be canceled against each other when appropriate. It is important to deal with these in a structured manner, otherwise you get large goals containing many correction terms which are very tedious to manipulate. We avoid this blowup by carefully controlling which definitions (d)simp is allowed to unfold and stating many lemmas explicitly before they are required. This leads to manageable goals containing only a small number of correction terms. Generally, we use the form F.map (eqToHom _) for these correction terms and try to push them as far outside as possible.

Future work #

References #

Tags #

presheaf, over category, coyoneda

Construction of the forward functor Over A ⥤ (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v #

structure CategoryTheory.OverPresheafAux.MakesOverArrow {C : Type u} [CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F A) {X : C} (s : CategoryTheory.yoneda.obj X A) (u : F.obj (Opposite.op X)) :

Via the Yoneda lemma, u : F.obj (op X) defines a natural transformation yoneda.obj X ⟶ F and via the element η.app (op X) u also a morphism yoneda.obj X ⟶ A. This structure witnesses the fact that these morphisms from a commutative triangle with η : F ⟶ A, i.e., that yoneda.obj X ⟶ F lifts to a morphism in Over A.

  • app : η.app (Opposite.op X) u = CategoryTheory.yonedaEquiv s
Instances For
    theorem CategoryTheory.OverPresheafAux.MakesOverArrow.app {C : Type u} [CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F A} {X : C} {s : CategoryTheory.yoneda.obj X A} {u : F.obj (Opposite.op X)} (self : CategoryTheory.OverPresheafAux.MakesOverArrow η s u) :
    η.app (Opposite.op X) u = CategoryTheory.yonedaEquiv s
    theorem CategoryTheory.OverPresheafAux.MakesOverArrow.map₁ {C : Type u} [CategoryTheory.Category.{v, u} C] {A F G : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F A} {μ : G A} {ε : F G} (hε : CategoryTheory.CategoryStruct.comp ε μ = η) {X : C} {s : CategoryTheory.yoneda.obj X A} {u : F.obj (Opposite.op X)} (h : CategoryTheory.OverPresheafAux.MakesOverArrow η s u) :

    "Functoriality" of MakesOverArrow η s in η.

    theorem CategoryTheory.OverPresheafAux.MakesOverArrow.map₂ {C : Type u} [CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F A} {X Y : C} (f : X Y) {s : CategoryTheory.yoneda.obj X A} {t : CategoryTheory.yoneda.obj Y A} (hst : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) t = s) {u : F.obj (Opposite.op Y)} (h : CategoryTheory.OverPresheafAux.MakesOverArrow η t u) :

    "Functoriality of MakesOverArrow η s in s.

    theorem CategoryTheory.OverPresheafAux.MakesOverArrow.of_arrow {C : Type u} [CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F A} {X : C} {s : CategoryTheory.yoneda.obj X A} {f : CategoryTheory.yoneda.obj X F} (hf : CategoryTheory.CategoryStruct.comp f η = s) :
    CategoryTheory.OverPresheafAux.MakesOverArrow η s (CategoryTheory.yonedaEquiv f)
    theorem CategoryTheory.OverPresheafAux.MakesOverArrow.of_yoneda_arrow {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C} {η : CategoryTheory.yoneda.obj Y A} {X : C} {s : CategoryTheory.yoneda.obj X A} {f : X Y} (hf : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) η = s) :
    def CategoryTheory.OverPresheafAux.OverArrows {C : Type u} [CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F A) {X : C} (s : CategoryTheory.yoneda.obj X A) :

    This is equivalent to the type Over.mk s ⟶ Over.mk η, but that lives in the wrong universe. However, if F = yoneda.obj Y for some Y, then (using that the Yoneda embedding is fully faithful) we get a good statement, see OverArrow.costructuredArrowIso.

    Equations
    Instances For

      Since OverArrows η s can be thought of to contain certain morphisms yoneda.obj X ⟶ F, the Yoneda lemma yields elements F.obj (op X).

      Equations
      • CategoryTheory.OverPresheafAux.OverArrows.val = Subtype.val
      Instances For
        theorem CategoryTheory.OverPresheafAux.OverArrows.ext {C : Type u} [CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F A} {X : C} {s : CategoryTheory.yoneda.obj X A} {u v : CategoryTheory.OverPresheafAux.OverArrows η s} :
        u.val = v.valu = v
        theorem CategoryTheory.OverPresheafAux.OverArrows.app_val {C : Type u} [CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F A} {X : C} {s : CategoryTheory.yoneda.obj X A} (p : CategoryTheory.OverPresheafAux.OverArrows η s) :
        η.app (Opposite.op X) p.val = CategoryTheory.yonedaEquiv s

        The defining property of OverArrows.val.

        @[simp]
        theorem CategoryTheory.OverPresheafAux.OverArrows.map_val {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C} {η : CategoryTheory.yoneda.obj Y A} {X : C} {s : CategoryTheory.yoneda.obj X A} (p : CategoryTheory.OverPresheafAux.OverArrows η s) :
        CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map p.val) η = s

        In the special case F = yoneda.obj Y, the element p.val for p : OverArrows η s is itself a morphism X ⟶ Y.

        Functoriality of OverArrows η s in η.

        Equations
        Instances For
          @[simp]
          theorem CategoryTheory.OverPresheafAux.OverArrows.map₁_val {C : Type u} [CategoryTheory.Category.{v, u} C] {A F G : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F A} {μ : G A} {X : C} (s : CategoryTheory.yoneda.obj X A) (u : CategoryTheory.OverPresheafAux.OverArrows η s) (ε : F G) (hε : CategoryTheory.CategoryStruct.comp ε μ = η) :
          (u.map₁ ε ).val = ε.app (Opposite.op X) u.val
          def CategoryTheory.OverPresheafAux.OverArrows.map₂ {C : Type u} [CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F A} {X Y : C} {s : CategoryTheory.yoneda.obj X A} {t : CategoryTheory.yoneda.obj Y A} (u : CategoryTheory.OverPresheafAux.OverArrows η t) (f : X Y) (hst : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) t = s) :

          Functoriality of OverArrows η s in s.

          Equations
          • u.map₂ f hst = F.map f.op u.val,
          Instances For
            @[simp]
            theorem CategoryTheory.OverPresheafAux.OverArrows.map₂_val {C : Type u} [CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F A} {X Y : C} (f : X Y) {s : CategoryTheory.yoneda.obj X A} {t : CategoryTheory.yoneda.obj Y A} (hst : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) t = s) (u : CategoryTheory.OverPresheafAux.OverArrows η t) :
            (u.map₂ f hst).val = F.map f.op u.val
            @[simp]
            theorem CategoryTheory.OverPresheafAux.OverArrows.map₁_map₂ {C : Type u} [CategoryTheory.Category.{v, u} C] {A F G : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F A} {μ : G A} (ε : F G) (hε : CategoryTheory.CategoryStruct.comp ε μ = η) {X Y : C} {s : CategoryTheory.yoneda.obj X A} {t : CategoryTheory.yoneda.obj Y A} (f : X Y) (hf : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) t = s) (u : CategoryTheory.OverPresheafAux.OverArrows η t) :
            (u.map₁ ε ).map₂ f hf = (u.map₂ f hf).map₁ ε
            def CategoryTheory.OverPresheafAux.OverArrows.yonedaArrow {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C} {η : CategoryTheory.yoneda.obj Y A} {X : C} {s : CategoryTheory.yoneda.obj X A} (f : X Y) (hf : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) η = s) :

            Construct an element of OverArrows η s with F = yoneda.obj Y from a suitable morphism f : X ⟶ Y.

            Equations
            Instances For
              @[simp]
              theorem CategoryTheory.OverPresheafAux.OverArrows.yonedaArrow_val {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C} {η : CategoryTheory.yoneda.obj Y A} {X : C} {s : CategoryTheory.yoneda.obj X A} {f : X Y} (hf : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) η = s) :

              If η is also yoneda-costructured, then OverArrows η s is just morphisms of costructured arrows.

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

                This is basically just yoneda.obj η : (Over A)ᵒᵖ ⥤ Type (max u v) restricted along the forgetful functor CostructuredArrow yoneda A ⥤ Over A, but done in a way that we land in a smaller universe.

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

                  Functoriality of restrictedYonedaObj η in η.

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

                    This is basically just yoneda : Over A ⥤ (Over A)ᵒᵖ ⥤ Type (max u v) restricted in the second argument along the forgetful functor CostructuredArrow yoneda A ⥤ Over A, but done in a way that we land in a smaller universe.

                    This is one direction of the equivalence we're constructing.

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

                      Further restricting the functor restrictedYoneda : Over A ⥤ (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v along the forgetful functor in the first argument recovers the Yoneda embedding CostructuredArrow yoneda A ⥤ (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v. This basically follows from the fact that the Yoneda embedding on C is fully faithful.

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

                        Construction of the backward functor ((CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v) ⥤ Over A #

                        This lemma will be key to establishing good simp normal forms.

                        To give an object of Over A, we will in particular need a presheaf Cᵒᵖ ⥤ Type v. This is the definition of that presheaf on objects.

                        We would prefer to think of this sigma type to be indexed by natural transformations yoneda.obj X ⟶ A instead of A.obj (op X). These are equivalent by the Yoneda lemma, but we cannot use the former because that type lives in the wrong universe. Hence, we will provide a lot of API that will enable us to pretend that we are really indexing over yoneda.obj X ⟶ A.

                        Equations
                        Instances For

                          Given a costructured arrow s : yoneda.obj X ⟶ A and an element x : F.obj s, construct an element of YonedaCollection F X.

                          Equations
                          Instances For

                            Access the first component of an element of YonedaCollection F X.

                            Equations
                            • p.fst = CategoryTheory.yonedaEquiv.symm p.fst
                            Instances For

                              This is a definition because it will be helpful to be able to control precisely when this definition is unfolded.

                              Equations
                              • p.yonedaEquivFst = CategoryTheory.yonedaEquiv p.fst
                              Instances For

                                Functoriality of YonedaCollection F X in X.

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

                                  Given F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v, this is the presheaf that is given by YonedaCollection F X on objects.

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

                                    This is the functor F ↦ X ↦ YonedaCollection F X.

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

                                      The Yoneda lemma yields a natural transformation yonedaCollectionPresheaf A F ⟶ A.

                                      Equations
                                      Instances For

                                        This is the reverse direction of the equivalence we're constructing.

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

                                          Construction of the unit #

                                          Intermediate stage of assembling the unit.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            @[simp]
                                            theorem CategoryTheory.OverPresheafAux.unitAuxAux_inv_app_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F A) (X : Cᵒᵖ) (a✝ : F.obj X) :
                                            ((CategoryTheory.OverPresheafAux.unitAuxAux η).inv.app X a✝).fst = η.app X a✝

                                            Construction of the counit #

                                            Intermediate stage of assembling the counit.

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

                                              Intermediate stage of assembling the counit.

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

                                                If A : Cᵒᵖ ⥤ Type v is a presheaf, then we have an equivalence between presheaves lying over A and the category of presheaves on CostructuredArrow yoneda A. There is a quasicommutative triangle involving this equivalence, see CostructuredArrow.toOverCompOverEquivPresheafCostructuredArrow.

                                                This is Lemma 1.4.12 in [KS06].

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

                                                  If A : Cᵒᵖ ⥤ Type v is a presheaf, then the Yoneda embedding for CostructuredArrow yoneda A factors through Over A via a forgetful functor and an equivalence.

                                                  This is Lemma 1.4.12 in [KS06].

                                                  Equations
                                                  Instances For
                                                    def CategoryTheory.CostructuredArrow.toOverCompYoneda {C : Type u} [CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v)) (T : CategoryTheory.Over A) :
                                                    (CategoryTheory.CostructuredArrow.toOver CategoryTheory.yoneda A).op.comp (CategoryTheory.yoneda.obj T) CategoryTheory.yoneda.op.comp (CategoryTheory.yoneda.obj ((CategoryTheory.overEquivPresheafCostructuredArrow A).functor.obj T))

                                                    This isomorphism says that hom-sets in the category Over A for a presheaf A where the domain is of the form (CostructuredArrow.toOver yoneda A).obj X can instead be interpreted as hom-sets in the category (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v where the domain is of the form yoneda.obj X after adjusting the codomain accordingly. This is desirable because in the latter case the Yoneda lemma can be applied.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      def CategoryTheory.CostructuredArrow.toOverCompCoyoneda {C : Type u} [CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v)) :
                                                      (CategoryTheory.CostructuredArrow.toOver CategoryTheory.yoneda A).op.comp CategoryTheory.coyoneda CategoryTheory.yoneda.op.comp (CategoryTheory.coyoneda.comp ((CategoryTheory.whiskeringLeft (CategoryTheory.Over A) (CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) (Type (max u v))).obj (CategoryTheory.overEquivPresheafCostructuredArrow A).functor))

                                                      This isomorphism says that hom-sets in the category Over A for a presheaf A where the domain is of the form (CostructuredArrow.toOver yoneda A).obj X can instead be interpreted as hom-sets in the category (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v where the domain is of the form yoneda.obj X after adjusting the codomain accordingly. This is desirable because in the latter case the Yoneda lemma can be applied.

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