mathlib3 documentation

category_theory.monoidal.coherence_lemmas

Lemmas which are consequences of monoidal coherence #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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') :
(λ_ (X Y)).hom f' = (α_ (𝟙_ C) X Y).inv ((λ_ X).hom 𝟙 Y) 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
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'