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') :

(α_ (𝟙_ C) X Y).hom ≫ (λ_ (X ⊗ Y)).hom ≫ f' = ((λ_ X).hom ⊗ 𝟙 Y) ≫ f'

theorem category_theory.monoidal_category.left_unitor_tensor' {C : Type u_1} [category_theory.category C] [category_theory.monoidal_category C] (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} [category_theory.category C] [category_theory.monoidal_category C] (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} [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.left_unitor_tensor_inv {C : Type u_1} [category_theory.category C] [category_theory.monoidal_category C] (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} [category_theory.category C] [category_theory.monoidal_category C] (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} [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.left_unitor_inv_tensor_id {C : Type u_1} [category_theory.category C] [category_theory.monoidal_category C] (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} [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.triangle_assoc_comp_right_inv_assoc {C : Type u_1} [category_theory.category C] [category_theory.monoidal_category C] (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} [category_theory.category C] [category_theory.monoidal_category C] (X Y : C) :

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

theorem category_theory.monoidal_category.unitors_equal {C : Type u_1} [category_theory.category C] [category_theory.monoidal_category C] :

(λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom

theorem category_theory.monoidal_category.unitors_inv_equal {C : Type u_1} [category_theory.category C] [category_theory.monoidal_category C] :

(λ_ (𝟙_ C)).inv = (ρ_ (𝟙_ C)).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'