mathlib documentation


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 a "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.

structure category_theory.enriched_category (V : Type v) [category_theory.category V] [category_theory.monoidal_category V] (C : Type u₁) :
Type (max u₁ v w)

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!


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


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 : lax_monoidal_functor V W to each hom object.


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


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


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 coyoneda_tensor_unit, 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 coyoneda_tensor_unit, 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, coyoneda_tensor_unit is just the usual forgetful functor, however. For V = Algebra R, the usual forgetful functor is coyoneda of polynomial R, not of R. (Perhaps we should have a typeclass for this situation: concrete_monoidal?)


Typecheck an object of C as an object of forget_enrichment W C.


Typecheck an object of forget_enrichment W C as an object of C.

structure category_theory.enriched_functor (V : Type v) [category_theory.category V] [category_theory.monoidal_category V] (C : Type u₁) [category_theory.enriched_category V C] (D : Type u₂) [category_theory.enriched_category V D] :
Type (max u₁ u₂ w)

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.

Composition of enriched functors.


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.

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

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

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

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

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

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

This presheaf has components (enriched_nat_trans_yoneda 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 enriched_nat_trans F G as the special case A := 𝟙_ V with the trivial half-braiding, and when defining enriched_nat_trans_yoneda F G we use the half-braidings coming from the ambient braiding on V.)

theorem category_theory.graded_nat_trans.ext {V : Type v} {_inst_1 : category_theory.category V} {_inst_2 : category_theory.monoidal_category V} {C : Type u₁} {_inst_3 : category_theory.enriched_category V C} {D : Type u₂} {_inst_4 : category_theory.enriched_category V D} {A : V} {F G : category_theory.enriched_functor V C D} (x y : category_theory.graded_nat_trans A F G) (h : = :
x = y
@[nolint, ext]

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.


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