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

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

    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.

      Instances For

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

        Instances For

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

          Instances For

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

            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?)

              Instances For

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

                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.)

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

                  Instances For
                    @[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 = CategoryTheory.EnrichedFunctor.map (Type v) CategoryTheory.types CategoryTheory.typesMonoidal C 𝒞 D 𝒟 F X Y 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.EnrichedFunctor.obj (CategoryTheory.enrichedFunctorTypeEquivFunctor.symm F) X = F.obj X
                    @[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 = CategoryTheory.EnrichedFunctor.obj F 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.EnrichedFunctor.map (Type v) CategoryTheory.types CategoryTheory.typesMonoidal C 𝒞 D 𝒟 (CategoryTheory.enrichedFunctorTypeEquivFunctor.symm F) X Y f = F.map f

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

                    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!

                      Instances For