mathlib documentation

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} [category_theory.category C] [category_theory.monoidal_category C] (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_assoc {C : Type u_1} [category_theory.category C] [category_theory.monoidal_category C] (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} [category_theory.category C] [category_theory.monoidal_category C] (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.id_tensor_right_unitor_inv_assoc {C : Type u_1} [category_theory.category C] [category_theory.monoidal_category C] (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} [category_theory.category C] [category_theory.monoidal_category C] (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.pentagon_inv_inv_hom_assoc {C : Type u_1} [category_theory.category C] [category_theory.monoidal_category C] (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} [category_theory.category C] [category_theory.monoidal_category C] (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.pentagon_hom_inv_assoc {C : Type u_1} [category_theory.category C] [category_theory.monoidal_category C] {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} [category_theory.category C] [category_theory.monoidal_category C] {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} [category_theory.category C] [category_theory.monoidal_category C] (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} [category_theory.category C] [category_theory.monoidal_category C] (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'