Documentation

Mathlib.CategoryTheory.Enriched.Basic

Enriched categories #

We set up the basic theory of V-enriched categories, for V an arbitrary monoidal category.

We do not assume here that V is a concrete category, so there does not need to be an "honest" underlying category!

Use X ⟶[V] Y to obtain the V object of morphisms from X to Y.

This file contains the definitions of V-enriched categories and V-functors.

We don't yet define the V-object of natural transformations between a pair of V-functors (this requires limits in V), but we do provide a presheaf isomorphic to the Yoneda embedding of this object.

We verify that when V = Type v, all these notion reduce to the usual ones.

A V-category is a category enriched in a monoidal category V.

Note that we do not assume that V is a concrete category, so there may not be an "honest" underlying category at all!

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

      The 𝟙_ V-shaped generalized element giving the identity in a V-enriched category.

      Equations
      Instances For

        A type synonym for C, which should come equipped with a V-enriched category structure. In a moment we will equip this with the W-enriched category structure obtained by applying the functor F : LaxMonoidalFunctor V W to each hom object.

        Equations
        Instances For

          Construct an honest category from a Type v-enriched category.

          Equations
          Instances For

            Construct a Type v-enriched category from an honest category.

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

              We verify that an enriched category in Type u is just the same thing as an honest category.

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

                A type synonym for C, which should come equipped with a V-enriched category structure. In a moment we will equip this with the (honest) category structure so that X ⟶ Y is (𝟙_ W) ⟶ (X ⟶[W] Y).

                We obtain this category by transporting the enrichment in V along the lax monoidal functor coyonedaTensorUnit, then using the equivalence of Type-enriched categories with honest categories.

                This is sometimes called the "underlying" category of an enriched category, although some care is needed as the functor coyonedaTensorUnit, which always exists, does not necessarily coincide with "the forgetful functor" from V to Type, if such exists. When V is any of Type, Top, AddCommGroup, or Module R, coyonedaTensorUnit is just the usual forgetful functor, however. For V = Algebra R, the usual forgetful functor is coyoneda of R[X], not of R. (Perhaps we should have a typeclass for this situation: ConcreteMonoidal?)

                Equations
                Instances For

                  A V-functor F between V-enriched categories has a V-morphism from X ⟶[V] Y to F.obj X ⟶[V] F.obj Y, satisfying the usual axioms.

                  Instances For

                    The identity enriched functor.

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

                      Composition of enriched functors.

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

                        An enriched functor induces an honest functor of the underlying categories, by mapping the (𝟙_ W)-shaped morphisms.

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

                          We now turn to natural transformations between V-functors.

                          The mostly commonly encountered definition of an enriched natural transformation is a collection of morphisms

                          (𝟙_ W) ⟶ (F.obj X ⟶[V] G.obj X)
                          

                          satisfying an appropriate analogue of the naturality square. (c.f. https://ncatlab.org/nlab/show/enriched+natural+transformation)

                          This is the same thing as a natural transformation F.forget ⟶ G.forget.

                          We formalize this as EnrichedNatTrans F G, which is a Type.

                          However, there's also something much nicer: with appropriate additional hypotheses, there is a V-object EnrichedNatTransObj F G which contains more information, and from which one can recover EnrichedNatTrans F G ≃ (𝟙_ V) ⟶ EnrichedNatTransObj F G.

                          Using these as the hom-objects, we can build a V-enriched category with objects the V-functors.

                          For EnrichedNatTransObj to exist, it suffices to have V braided and complete.

                          Before assuming V is complete, we assume it is braided and define a presheaf enrichedNatTransYoneda F G which is isomorphic to the Yoneda embedding of EnrichedNatTransObj F G whether or not that object actually exists.

                          This presheaf has components (enrichedNatTransYoneda F G).obj A what we call the A-graded enriched natural transformations, which are collections of morphisms

                          A ⟶ (F.obj X ⟶[V] G.obj X)
                          

                          satisfying a similar analogue of the naturality square, this time incorporating a half-braiding on A.

                          (We actually define EnrichedNatTrans F G as the special case A := 𝟙_ V with the trivial half-braiding, and when defining enrichedNatTransYoneda F G we use the half-braidings coming from the ambient braiding on V.)

                          The type of A-graded natural transformations between V-functors F and G. This is the type of morphisms in V from A to the V-object of natural transformations.

                          Instances For

                            A presheaf isomorphic to the Yoneda embedding of the V-object of natural transformations from F to G.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              @[simp]
                              theorem CategoryTheory.enrichedFunctorTypeEquivFunctor_apply_obj {C : Type u₁} [𝒞 : CategoryTheory.EnrichedCategory (Type v) C] {D : Type u₂} [𝒟 : CategoryTheory.EnrichedCategory (Type v) D] (F : CategoryTheory.EnrichedFunctor (Type v) C D) (X : C) :
                              (CategoryTheory.enrichedFunctorTypeEquivFunctor F).obj X = F.obj X
                              @[simp]
                              theorem CategoryTheory.enrichedFunctorTypeEquivFunctor_symm_apply_map {C : Type u₁} [𝒞 : CategoryTheory.EnrichedCategory (Type v) C] {D : Type u₂} [𝒟 : CategoryTheory.EnrichedCategory (Type v) D] (F : CategoryTheory.Functor C D) (X : C) (Y : C) (f : CategoryTheory.EnrichedCategory.Hom X Y) :
                              (CategoryTheory.enrichedFunctorTypeEquivFunctor.symm F).map X Y f = F.map f
                              @[simp]
                              theorem CategoryTheory.enrichedFunctorTypeEquivFunctor_symm_apply_obj {C : Type u₁} [𝒞 : CategoryTheory.EnrichedCategory (Type v) C] {D : Type u₂} [𝒟 : CategoryTheory.EnrichedCategory (Type v) D] (F : CategoryTheory.Functor C D) (X : C) :
                              (CategoryTheory.enrichedFunctorTypeEquivFunctor.symm F).obj X = F.obj X
                              @[simp]
                              theorem CategoryTheory.enrichedFunctorTypeEquivFunctor_apply_map {C : Type u₁} [𝒞 : CategoryTheory.EnrichedCategory (Type v) C] {D : Type u₂} [𝒟 : CategoryTheory.EnrichedCategory (Type v) D] (F : CategoryTheory.EnrichedFunctor (Type v) C D) :
                              ∀ {X Y : C} (f : X Y), (CategoryTheory.enrichedFunctorTypeEquivFunctor F).map f = F.map X Y f

                              We verify that an enriched functor between Type v enriched categories is just the same thing as an honest functor.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                def CategoryTheory.enrichedNatTransYonedaTypeIsoYonedaNatTrans {C : Type v} [CategoryTheory.EnrichedCategory (Type v) C] {D : Type v} [CategoryTheory.EnrichedCategory (Type v) D] (F : CategoryTheory.EnrichedFunctor (Type v) C D) (G : CategoryTheory.EnrichedFunctor (Type v) C D) :
                                CategoryTheory.enrichedNatTransYoneda F G CategoryTheory.yoneda.obj (CategoryTheory.enrichedFunctorTypeEquivFunctor F CategoryTheory.enrichedFunctorTypeEquivFunctor G)

                                We verify that the presheaf representing natural transformations between Type v-enriched functors is actually represented by the usual type of natural transformations!

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