# mathlibdocumentation

category_theory.monoidal.coherence_lemmas

# Lemmas which are consequences of monoidal coherence #

These lemmas are all proved by coherence.

## Future work #

Investigate whether these lemmas are really needed, or if they can be replaced by use of the coherence tactic.

theorem category_theory.monoidal_category.left_unitor_tensor'_assoc {C : Type u_1} (X Y : C) {X' : C} (f' : X Y X') :
(α_ (𝟙_ C) X Y).hom (λ_ (X Y)).hom f' = ((λ_ X).hom 𝟙 Y) f'
theorem category_theory.monoidal_category.left_unitor_tensor' {C : Type u_1} (X Y : C) :
(α_ (𝟙_ C) X Y).hom (λ_ (X Y)).hom = (λ_ X).hom 𝟙 Y
@[simp]
theorem category_theory.monoidal_category.left_unitor_tensor {C : Type u_1} (X Y : C) :
(λ_ (X Y)).hom = (α_ (𝟙_ C) X Y).inv ((λ_ X).hom 𝟙 Y)
theorem category_theory.monoidal_category.left_unitor_tensor_assoc {C : Type u_1} (X Y : C) {X' : C} (f' : X Y X') :
(λ_ (X Y)).hom f' = (α_ (𝟙_ C) X Y).inv ((λ_ X).hom 𝟙 Y) f'
theorem category_theory.monoidal_category.left_unitor_tensor_inv_assoc {C : Type u_1} (X Y : C) {X' : C} (f' : 𝟙_ C X Y X') :
(λ_ (X Y)).inv f' = ((λ_ X).inv 𝟙 Y) (α_ (𝟙_ C) X Y).hom f'
theorem category_theory.monoidal_category.left_unitor_tensor_inv {C : Type u_1} (X Y : C) :
(λ_ (X Y)).inv = ((λ_ X).inv 𝟙 Y) (α_ (𝟙_ C) X Y).hom
theorem category_theory.monoidal_category.id_tensor_right_unitor_inv {C : Type u_1} (X Y : C) :
𝟙 X (ρ_ Y).inv = (ρ_ (X Y)).inv (α_ X Y (𝟙_ C)).hom
theorem category_theory.monoidal_category.id_tensor_right_unitor_inv_assoc {C : Type u_1} (X Y : C) {X' : C} (f' : X Y 𝟙_ C X') :
(𝟙 X (ρ_ Y).inv) f' = (ρ_ (X Y)).inv (α_ X Y (𝟙_ C)).hom f'
theorem category_theory.monoidal_category.left_unitor_inv_tensor_id_assoc {C : Type u_1} (X Y : C) {X' : C} (f' : (𝟙_ C X) Y X') :
((λ_ X).inv 𝟙 Y) f' = (λ_ (X Y)).inv (α_ (𝟙_ C) X Y).inv f'
theorem category_theory.monoidal_category.left_unitor_inv_tensor_id {C : Type u_1} (X Y : C) :
(λ_ X).inv 𝟙 Y = (λ_ (X Y)).inv (α_ (𝟙_ C) X Y).inv
theorem category_theory.monoidal_category.pentagon_inv_inv_hom_assoc {C : Type u_1} (W X Y Z : C) {X' : C} (f' : (W X) Y Z X') :
(α_ W (X Y) Z).inv ((α_ W X Y).inv 𝟙 Z) (α_ (W X) Y Z).hom f' = (𝟙 W (α_ X Y Z).hom) (α_ W X (Y Z)).inv f'
theorem category_theory.monoidal_category.pentagon_inv_inv_hom {C : Type u_1} (W X Y Z : C) :
(α_ W (X Y) Z).inv ((α_ W X Y).inv 𝟙 Z) (α_ (W X) Y Z).hom = (𝟙 W (α_ X Y Z).hom) (α_ W X (Y Z)).inv
@[simp]
theorem category_theory.monoidal_category.triangle_assoc_comp_right_inv_assoc {C : Type u_1} (X Y : C) {X' : C} (f' : X 𝟙_ C Y X') :
((ρ_ X).inv 𝟙 Y) (α_ X (𝟙_ C) Y).hom f' = (𝟙 X (λ_ Y).inv) f'
@[simp]
theorem category_theory.monoidal_category.triangle_assoc_comp_right_inv {C : Type u_1} (X Y : C) :
((ρ_ X).inv 𝟙 Y) (α_ X (𝟙_ C) Y).hom = 𝟙 X (λ_ Y).inv
theorem category_theory.monoidal_category.pentagon_hom_inv_assoc {C : Type u_1} {W X Y Z X' : C} (f' : W (X Y) Z X') :
(α_ W X (Y Z)).hom (𝟙 W (α_ X Y Z).inv) f' = (α_ (W X) Y Z).inv ((α_ W X Y).hom 𝟙 Z) (α_ W (X Y) Z).hom f'
theorem category_theory.monoidal_category.pentagon_hom_inv {C : Type u_1} {W X Y Z : C} :
(α_ W X (Y Z)).hom (𝟙 W (α_ X Y Z).inv) = (α_ (W X) Y Z).inv ((α_ W X Y).hom 𝟙 Z) (α_ W (X Y) Z).hom
theorem category_theory.monoidal_category.pentagon_inv_hom {C : Type u_1} (W X Y Z : C) :
(α_ (W X) Y Z).inv ((α_ W X Y).hom 𝟙 Z) = (α_ W X (Y Z)).hom (𝟙 W (α_ X Y Z).inv) (α_ W (X Y) Z).inv
theorem category_theory.monoidal_category.pentagon_inv_hom_assoc {C : Type u_1} (W X Y Z : C) {X' : C} (f' : (W X Y) Z X') :
(α_ (W X) Y Z).inv ((α_ W X Y).hom 𝟙 Z) f' = (α_ W X (Y Z)).hom (𝟙 W (α_ X Y Z).inv) (α_ W (X Y) Z).inv f'