mathlib documentation

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

@[class]
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!

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.

Equations
@[nolint]

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.

Equations
Instances for category_theory.transport_enrichment

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

Equations

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

Equations
@[nolint]

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

Equations
Instances for category_theory.forget_enrichment

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

Equations

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

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

Instances for category_theory.enriched_functor
@[simp]
theorem category_theory.enriched_functor.map_comp {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] (self : category_theory.enriched_functor V C D) (X Y Z : C) :
category_theory.e_comp V X Y Z self.map X Z = (self.map X Y self.map Y Z) category_theory.e_comp V (self.obj X) (self.obj Y) (self.obj Z)
@[simp]
theorem category_theory.enriched_functor.map_comp_assoc {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] (self : category_theory.enriched_functor V C D) (X Y Z : C) {X' : V} (f' : category_theory.enriched_category.hom (self.obj X) (self.obj Z) X') :
category_theory.e_comp V X Y Z self.map X Z f' = (self.map X Y self.map Y Z) category_theory.e_comp V (self.obj X) (self.obj Y) (self.obj Z) f'

Composition of enriched functors.

Equations

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 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 : category_theory.center V} {F G : category_theory.enriched_functor V C D} (x y : category_theory.graded_nat_trans A F G) (h : x.app = y.app) :
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.

Instances for category_theory.graded_nat_trans
  • category_theory.graded_nat_trans.has_sizeof_inst

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

Equations
@[simp]

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

Equations