mathlib3 documentation


Enriched categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.


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 of this typeclass
Instances of other typeclasses for category_theory.enriched_category
  • category_theory.enriched_category.has_sizeof_inst

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.

Instances for category_theory.transport_enrichment

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 R[X], not of R. (Perhaps we should have a typeclass for this situation: concrete_monoidal?)

Instances for category_theory.forget_enrichment

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.


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 category_theory.enriched_functor

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

@[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.

Instances for category_theory.graded_nat_trans
  • category_theory.graded_nat_trans.has_sizeof_inst

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