# mathlibdocumentation

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) (C : Type u₁) :
Type (max u₁ v w)
• hom : C → C → V
• id : Π (X : C),
• comp : Π (X Y Z : C),
• id_comp : (∀ (X Y : C), . "obviously"
• comp_id : (∀ (X Y : C), . "obviously"
• assoc : (∀ (W X Y Z : C), . "obviously"

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
def category_theory.e_id (V : Type v) {C : Type u₁} (X : C) :

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

Equations
def category_theory.e_comp (V : Type v) {C : Type u₁} (X Y Z : C) :

The composition V-morphism for a V-enriched category.

Equations
@[simp]
theorem category_theory.e_id_comp (V : Type v) {C : Type u₁} (X Y : C) :
Y =
@[simp]
theorem category_theory.e_id_comp_assoc (V : Type v) {C : Type u₁} (X Y : C) {X' : V} (f' : X') :
Y f' = f'
@[simp]
theorem category_theory.e_comp_id (V : Type v) {C : Type u₁} (X Y : C) :
Y =
@[simp]
theorem category_theory.e_comp_id_assoc (V : Type v) {C : Type u₁} (X Y : C) {X' : V} (f' : X') :
Y f' = f'
@[simp]
theorem category_theory.e_assoc_assoc (V : Type v) {C : Type u₁} (W X Y Z : C) {X' : V} (f' : X') :
X Y Z f' = Z) Z f'
@[simp]
theorem category_theory.e_assoc (V : Type v) {C : Type u₁} (W X Y Z : C) :
X Y Z = Z) Z
@[nolint]
def category_theory.transport_enrichment {V : Type v} {W : Type v} (C : Type u₁) :
Type u₁

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
@[protected, instance]
def category_theory.transport_enrichment.enriched_category {V : Type v} {C : Type u₁} {W : Type v}  :
Equations
def category_theory.category_of_enriched_category_Type (C : Type u₁) [𝒞 : C] :

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

Equations

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

Equations

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

Equations
@[nolint]
def category_theory.forget_enrichment (W : Type (v+1)) (C : Type u₁)  :
Type u₁

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
def category_theory.forget_enrichment.of {C : Type u₁} (W : Type (v+1)) (X : C) :

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

Equations
def category_theory.forget_enrichment.to {C : Type u₁} (W : Type (v+1))  :
C

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

Equations
@[simp]
theorem category_theory.forget_enrichment.to_of {C : Type u₁} (W : Type (v+1)) (X : C) :
@[simp]
theorem category_theory.forget_enrichment.of_to {C : Type u₁} (W : Type (v+1))  :
@[protected, instance]
def category_theory.category_forget_enrichment {C : Type u₁} (W : Type (v+1))  :
Equations
def category_theory.forget_enrichment.hom_of {C : Type u₁} (W : Type (v+1)) {X Y : C} (f : 𝟙_ W ) :

Typecheck a (𝟙_ W)-shaped W-morphism as a morphism in forget_enrichment W C.

Equations
def category_theory.forget_enrichment.hom_to {C : Type u₁} (W : Type (v+1)) {X Y : C} (f : X Y) :

Typecheck a morphism in forget_enrichment W C as a (𝟙_ W)-shaped W-morphism.

Equations
@[simp]
theorem category_theory.forget_enrichment.hom_to_hom_of {C : Type u₁} (W : Type (v+1)) {X Y : C} (f : 𝟙_ W ) :
@[simp]
theorem category_theory.forget_enrichment.hom_of_hom_to {C : Type u₁} (W : Type (v+1)) {X Y : C} (f : X Y) :
@[simp]
theorem category_theory.forget_enrichment_id {C : Type u₁} (W : Type (v+1))  :

The identity in the "underlying" category of an enriched category.

@[simp]
theorem category_theory.forget_enrichment_id' {C : Type u₁} (W : Type (v+1)) (X : C) :
@[simp]
theorem category_theory.forget_enrichment_comp {C : Type u₁} (W : Type (v+1)) {X Y Z : C} (f : X Y) (g : Y Z) :

Composition in the "underlying" category of an enriched category.

structure category_theory.enriched_functor (V : Type v) (C : Type u₁) (D : Type u₂)  :
Type (max u₁ u₂ w)
• obj : C → D
• map : Π (X Y : C), (self.obj Y)
• map_id' : (∀ (X : C), self.map X X = (self.obj X)) . "obviously"
• map_comp' : (∀ (X Y Z : C), Z self.map X Z = (self.map X Y self.map Y Z) (self.obj X) (self.obj Y) (self.obj Z)) . "obviously"

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_id {V : Type v} {C : Type u₁} {D : Type u₂} (self : D) (X : C) :
self.map X X = (self.obj X)
@[simp]
theorem category_theory.enriched_functor.map_comp {V : Type v} {C : Type u₁} {D : Type u₂} (self : D) (X Y Z : C) :
Z self.map X Z = (self.map X Y self.map Y Z) (self.obj X) (self.obj Y) (self.obj Z)
@[simp]
theorem category_theory.enriched_functor.map_id_assoc {V : Type v} {C : Type u₁} {D : Type u₂} (self : D) (X : C) {X' : V} (f' : (self.obj X) X') :
self.map X X f' = (self.obj X) f'
@[simp]
theorem category_theory.enriched_functor.map_comp_assoc {V : Type v} {C : Type u₁} {D : Type u₂} (self : D) (X Y Z : C) {X' : V} (f' : (self.obj Z) X') :
Z self.map X Z f' = (self.map X Y self.map Y Z) (self.obj X) (self.obj Y) (self.obj Z) f'
@[simp]
theorem category_theory.enriched_functor.id_obj (V : Type v) (C : Type u₁) (X : C) :
= X
def category_theory.enriched_functor.id (V : Type v) (C : Type u₁)  :

The identity enriched functor.

Equations
@[simp]
theorem category_theory.enriched_functor.id_map (V : Type v) (C : Type u₁) (X Y : C) :
@[protected, instance]
def category_theory.enriched_functor.inhabited (V : Type v) {C : Type u₁}  :
Equations
def category_theory.enriched_functor.comp (V : Type v) {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : D) (G : E) :

Composition of enriched functors.

Equations
@[simp]
theorem category_theory.enriched_functor.comp_obj (V : Type v) {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : D) (G : E) (X : C) :
X = G.obj (F.obj X)
@[simp]
theorem category_theory.enriched_functor.comp_map (V : Type v) {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : D) (G : E) (X Y : C) :
X Y = F.map X Y G.map (F.obj X) (F.obj Y)
def category_theory.enriched_functor.forget {W : Type (v+1)} {C : Type u₁} {D : Type u₂} (F : D) :

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

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_iff {V : Type v} {_inst_1 : category_theory.category V} {_inst_2 : category_theory.monoidal_category V} {C : Type u₁} {_inst_3 : C} {D : Type u₂} {_inst_4 : D} {A : category_theory.center V} {F G : D} (x y : G) :
x = y x.app = y.app
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 : C} {D : Type u₂} {_inst_4 : D} {A : category_theory.center V} {F G : D} (x y : G) (h : x.app = y.app) :
x = y
@[nolint, ext]
structure category_theory.graded_nat_trans {V : Type v} {C : Type u₁} {D : Type u₂} (A : category_theory.center V) (F G : D) :
Type (max u₁ w)

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
@[simp]
theorem category_theory.enriched_nat_trans_yoneda_map_app {V : Type v} {C : Type u₁} {D : Type u₂} (F G : D) (A A' : Vᵒᵖ) (f : A A') (X : C) :
σ).app X = f.unop σ.app X
@[simp]
theorem category_theory.enriched_nat_trans_yoneda_obj {V : Type v} {C : Type u₁} {D : Type u₂} (F G : D) (A : Vᵒᵖ) :
noncomputable def category_theory.enriched_nat_trans_yoneda {V : Type v} {C : Type u₁} {D : Type u₂} (F G : D) :
Vᵒᵖ Type (max u₁ w)

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

Equations
@[simp]
theorem category_theory.enriched_functor_Type_equiv_functor_apply_map {C : Type u₁} [𝒞 : C] {D : Type u₂} [𝒟 : D] (F : category_theory.enriched_functor (Type v) C D) (X Y : C) (f : X Y) :
= F.map X Y f
@[simp]
theorem category_theory.enriched_functor_Type_equiv_functor_apply_obj {C : Type u₁} [𝒞 : C] {D : Type u₂} [𝒟 : D] (F : category_theory.enriched_functor (Type v) C D) (X : C) :
@[simp]
theorem category_theory.enriched_functor_Type_equiv_functor_symm_apply_obj {C : Type u₁} [𝒞 : C] {D : Type u₂} [𝒟 : D] (F : C D) (X : C) :
def category_theory.enriched_functor_Type_equiv_functor {C : Type u₁} [𝒞 : C] {D : Type u₂} [𝒟 : D] :

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

Equations
@[simp]
theorem category_theory.enriched_functor_Type_equiv_functor_symm_apply_map {C : Type u₁} [𝒞 : C] {D : Type u₂} [𝒟 : D] (F : C D) (X Y : C)  :
= F.map f
noncomputable def category_theory.enriched_nat_trans_yoneda_Type_iso_yoneda_nat_trans {C : Type v} [ C] {D : Type v} [ D] (F G : category_theory.enriched_functor (Type v) C D) :

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

Equations