mathlib documentation

category_theory.monoidal.category

Monoidal categories

A monoidal category is a category equipped with a tensor product, unitors, and an associator. In the definition, we provide the tensor product as a pair of functions

The tensor product can be expressed as a functor via tensor : C × C ⥤ C. The unitors and associator are gathered together as natural isomorphisms in left_unitor_nat_iso, right_unitor_nat_iso and associator_nat_iso.

Some consequences of the definition are proved in other files, e.g. (λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom in category_theory.monoidal.unitors_equal.

Implementation

Dealing with unitors and associators is painful, and at this stage we do not have a useful implementation of coherence for monoidal categories.

In an effort to lessen the pain, we put some effort into choosing the right simp lemmas. Generally, the rule is that the component index of a natural transformation "weighs more" in considering the complexity of an expression than does a structural isomorphism (associator, etc).

As an example when we prove Proposition 2.2.4 of http://www-math.mit.edu/~etingof/egnobookfinal.pdf we state it as a @[simp] lemma as

(λ_ (X  Y)).hom = (α_ (𝟙_ C) X Y).inv  (λ_ X).hom  (𝟙 Y)

This is far from completely effective, but seems to prove a useful principle.

References

@[class]
structure category_theory.monoidal_category (C : Type u) [𝒞 : category_theory.category C] :
Type (max u v)

In a monoidal category, we can take the tensor product of objects, X ⊗ Y and of morphisms f ⊗ g. Tensor product does not need to be strictly associative on objects, but there is a specified associator, α_ X Y Z : (X ⊗ Y) ⊗ Z ≅ X ⊗ (Y ⊗ Z). There is a tensor unit 𝟙_ C, with specified left and right unitor isomorphisms λ_ X : 𝟙_ C ⊗ X ≅ X and ρ_ X : X ⊗ 𝟙_ C ≅ X. These associators and unitors satisfy the pentagon and triangle equations.

See https://stacks.math.columbia.edu/tag/0FFK.

Instances
@[simp]
theorem category_theory.tensor_iso_hom {C : Type u} {X Y X' Y' : C} [category_theory.category C] [category_theory.monoidal_category C] (f : X Y) (g : X' Y') :
(f g).hom = (f.hom g.hom)

@[simp]
theorem category_theory.tensor_iso_inv {C : Type u} {X Y X' Y' : C} [category_theory.category C] [category_theory.monoidal_category C] (f : X Y) (g : X' Y') :
(f g).inv = (f.inv g.inv)

def category_theory.tensor_iso {C : Type u} {X Y X' Y' : C} [category_theory.category C] [category_theory.monoidal_category C] :
(X Y)(X' Y')(X X' Y Y')

The tensor product of two isomorphisms is an isomorphism.

Equations
@[simp]
theorem category_theory.monoidal_category.comp_tensor_id {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {W X Y Z : C} (f : W X) (g : X Y) :
f g 𝟙 Z = (f 𝟙 Z) (g 𝟙 Z)

@[simp]
theorem category_theory.monoidal_category.id_tensor_comp {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {W X Y Z : C} (f : W X) (g : X Y) :
𝟙 Z f g = (𝟙 Z f) (𝟙 Z g)

@[simp]
theorem category_theory.monoidal_category.id_tensor_comp_tensor_id {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {W X Y Z : C} (f : W X) (g : Y Z) :
(𝟙 Y f) (g 𝟙 X) = (g f)

@[simp]
theorem category_theory.monoidal_category.id_tensor_comp_tensor_id_assoc {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {W X Y Z : C} (f : W X) (g : Y Z) {X' : C} (f' : Z X X') :
(𝟙 Y f) (g 𝟙 X) f' = (g f) f'

@[simp]
theorem category_theory.monoidal_category.tensor_id_comp_id_tensor {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {W X Y Z : C} (f : W X) (g : Y Z) :
(g 𝟙 W) (𝟙 Z f) = (g f)

@[simp]
theorem category_theory.monoidal_category.tensor_id_comp_id_tensor_assoc {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {W X Y Z : C} (f : W X) (g : Y Z) {X' : C} (f' : Z X X') :
(g 𝟙 W) (𝟙 Z f) f' = (g f) f'

theorem category_theory.monoidal_category.associator_inv_naturality {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {X Y Z X' Y' Z' : C} (f : X X') (g : Y Y') (h : Z Z') :
(f (g h)) (α_ X' Y' Z').inv = (α_ X Y Z).inv (f g h)

theorem category_theory.monoidal_category.pentagon_inv {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (W X Y Z : C) :
(𝟙 W (α_ X Y Z).inv) (α_ W (X Y) Z).inv ((α_ W X Y).inv 𝟙 Z) = (α_ W X (Y Z)).inv (α_ (W X) Y Z).inv

The tensor product expressed as a functor.

Equations

The left-associated triple tensor product as a functor.

Equations

The right-associated triple tensor product as a functor.

Equations

The functor λ X, 𝟙_ C ⊗ X.

Equations

The functor λ X, X ⊗ 𝟙_ C.

Equations

Tensoring on the left with a fixed object, as a functor.

Equations

Tensoring on the right with a fixed object, as a functor.

Equations

Tensoring on the right, as a functor from C into endofunctors of C.

We later show this is a monoidal functor.

Equations