mathlib documentation

category_theory.​monoidal.​category

category_theory.​monoidal.​category

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

Instances
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]

@[simp]

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 as fixed object, as a functor.

Equations

Tensoring on the right with as 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