mathlib documentation

category_theory.monoidal.unitors

The two morphisms Ξ»_ (πŸ™_ C) and ρ_ (πŸ™_ C) from πŸ™_ C βŠ— πŸ™_ C to πŸ™_ C are equal.

This is suprisingly difficult to prove directly from the usual axioms for a monoidal category!

This proof follows the diagram given at https://people.math.osu.edu/penneys.2/QS2019/VicaryHandout.pdf

It should be a consequence of the coherence theorem for monoidal categories (although quite possibly it is a necessary building block of any proof).

source
theorem category_theory.monoidal_category.unitors_equal.cells_1_2 {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] :
(ρ_ (πŸ™_ C)).hom = (Ξ»_ (πŸ™_ C βŠ— πŸ™_ C)).inv ≫ (πŸ™ (πŸ™_ C) βŠ— (ρ_ (πŸ™_ C)).hom) ≫ (Ξ»_ (πŸ™_ C)).hom

source
theorem category_theory.monoidal_category.unitors_equal.cells_4 {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] :
(Ξ»_ (πŸ™_ C βŠ— πŸ™_ C)).inv ≫ (πŸ™ (πŸ™_ C) βŠ— (Ξ»_ (πŸ™_ C)).hom) = (Ξ»_ (πŸ™_ C)).hom ≫ (Ξ»_ (πŸ™_ C)).inv

source
theorem category_theory.monoidal_category.unitors_equal.cells_4' {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] :
(Ξ»_ (πŸ™_ C βŠ— πŸ™_ C)).inv = (Ξ»_ (πŸ™_ C)).hom ≫ (Ξ»_ (πŸ™_ C)).inv ≫ (πŸ™ (πŸ™_ C) βŠ— (Ξ»_ (πŸ™_ C)).inv)

source
theorem category_theory.monoidal_category.unitors_equal.cells_3_4 {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] :
(Ξ»_ (πŸ™_ C βŠ— πŸ™_ C)).inv = (πŸ™ (πŸ™_ C) βŠ— (Ξ»_ (πŸ™_ C)).inv)

source
theorem category_theory.monoidal_category.unitors_equal.cells_1_4 {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] :
(ρ_ (πŸ™_ C)).hom = (πŸ™ (πŸ™_ C) βŠ— (Ξ»_ (πŸ™_ C)).inv) ≫ (πŸ™ (πŸ™_ C) βŠ— (ρ_ (πŸ™_ C)).hom) ≫ (Ξ»_ (πŸ™_ C)).hom

source
theorem category_theory.monoidal_category.unitors_equal.cells_6 {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] :
((ρ_ (πŸ™_ C)).inv βŠ— πŸ™ (πŸ™_ C)) ≫ (ρ_ (πŸ™_ C βŠ— πŸ™_ C)).hom = (ρ_ (πŸ™_ C)).hom ≫ (ρ_ (πŸ™_ C)).inv

source
theorem category_theory.monoidal_category.unitors_equal.cells_6' {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] :
(ρ_ (πŸ™_ C)).inv βŠ— πŸ™ (πŸ™_ C) = (ρ_ (πŸ™_ C)).hom ≫ (ρ_ (πŸ™_ C)).inv ≫ (ρ_ (πŸ™_ C βŠ— πŸ™_ C)).inv

source
theorem category_theory.monoidal_category.unitors_equal.cells_5_6 {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] :
(ρ_ (πŸ™_ C)).inv βŠ— πŸ™ (πŸ™_ C) = (ρ_ (πŸ™_ C βŠ— πŸ™_ C)).inv

source
theorem category_theory.monoidal_category.unitors_equal.cells_7 {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] :
πŸ™ (πŸ™_ C) βŠ— (Ξ»_ (πŸ™_ C)).inv = ((ρ_ (πŸ™_ C)).inv βŠ— πŸ™ (πŸ™_ C)) ≫ (Ξ±_ (πŸ™_ C) (πŸ™_ C) (πŸ™_ C)).hom

source
theorem category_theory.monoidal_category.unitors_equal.cells_1_7 {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] :
(ρ_ (πŸ™_ C)).hom = (ρ_ (πŸ™_ C βŠ— πŸ™_ C)).inv ≫ (Ξ±_ (πŸ™_ C) (πŸ™_ C) (πŸ™_ C)).hom ≫ (πŸ™ (πŸ™_ C) βŠ— (ρ_ (πŸ™_ C)).hom) ≫ (Ξ»_ (πŸ™_ C)).hom

source
theorem category_theory.monoidal_category.unitors_equal.cells_8 {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] :
(Ξ±_ (πŸ™_ C) (πŸ™_ C) (πŸ™_ C)).hom = (ρ_ (πŸ™_ C βŠ— πŸ™_ C βŠ— πŸ™_ C)).inv ≫ ((Ξ±_ (πŸ™_ C) (πŸ™_ C) (πŸ™_ C)).hom βŠ— πŸ™ (πŸ™_ C)) ≫ (ρ_ (πŸ™_ C βŠ— (πŸ™_ C βŠ— πŸ™_ C))).hom

source
theorem category_theory.monoidal_category.unitors_equal.cells_14 {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] :
(ρ_ (πŸ™_ C βŠ— πŸ™_ C)).inv ≫ (ρ_ (πŸ™_ C βŠ— πŸ™_ C βŠ— πŸ™_ C)).inv = (ρ_ (πŸ™_ C βŠ— πŸ™_ C)).inv ≫ ((ρ_ (πŸ™_ C βŠ— πŸ™_ C)).inv βŠ— πŸ™ (πŸ™_ C))

source
theorem category_theory.monoidal_category.unitors_equal.cells_9 {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] :
(Ξ±_ (πŸ™_ C) (πŸ™_ C) (πŸ™_ C)).hom βŠ— πŸ™ (πŸ™_ C) = (Ξ±_ (πŸ™_ C βŠ— πŸ™_ C) (πŸ™_ C) (πŸ™_ C)).hom ≫ (Ξ±_ (πŸ™_ C) (πŸ™_ C) (πŸ™_ C βŠ— πŸ™_ C)).hom ≫ (πŸ™ (πŸ™_ C) βŠ— (Ξ±_ (πŸ™_ C) (πŸ™_ C) (πŸ™_ C)).inv) ≫ (Ξ±_ (πŸ™_ C) (πŸ™_ C βŠ— πŸ™_ C) (πŸ™_ C)).inv

source
theorem category_theory.monoidal_category.unitors_equal.cells_10_13 {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] :
((ρ_ (πŸ™_ C βŠ— πŸ™_ C)).inv βŠ— πŸ™ (πŸ™_ C)) ≫ (Ξ±_ (πŸ™_ C βŠ— πŸ™_ C) (πŸ™_ C) (πŸ™_ C)).hom ≫ (Ξ±_ (πŸ™_ C) (πŸ™_ C) (πŸ™_ C βŠ— πŸ™_ C)).hom ≫ (πŸ™ (πŸ™_ C) βŠ— (Ξ±_ (πŸ™_ C) (πŸ™_ C) (πŸ™_ C)).inv) ≫ (Ξ±_ (πŸ™_ C) (πŸ™_ C βŠ— πŸ™_ C) (πŸ™_ C)).inv = (πŸ™ (πŸ™_ C) βŠ— (ρ_ (πŸ™_ C)).inv βŠ— πŸ™ (πŸ™_ C))

source
theorem category_theory.monoidal_category.unitors_equal.cells_9_13 {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] :
((ρ_ (πŸ™_ C βŠ— πŸ™_ C)).inv βŠ— πŸ™ (πŸ™_ C)) ≫ ((Ξ±_ (πŸ™_ C) (πŸ™_ C) (πŸ™_ C)).hom βŠ— πŸ™ (πŸ™_ C)) = (πŸ™ (πŸ™_ C) βŠ— (ρ_ (πŸ™_ C)).inv βŠ— πŸ™ (πŸ™_ C))

source
theorem category_theory.monoidal_category.unitors_equal.cells_15 {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] :
(ρ_ (πŸ™_ C βŠ— πŸ™_ C)).inv ≫ (πŸ™ (πŸ™_ C) βŠ— (ρ_ (πŸ™_ C)).inv βŠ— πŸ™ (πŸ™_ C)) ≫ (ρ_ (πŸ™_ C βŠ— (πŸ™_ C βŠ— πŸ™_ C))).hom ≫ (πŸ™ (πŸ™_ C) βŠ— (ρ_ (πŸ™_ C)).hom) = πŸ™ (πŸ™_ C βŠ— πŸ™_ C)

source
theorem category_theory.monoidal_category.unitors_equal {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] :
(Ξ»_ (πŸ™_ C)).hom = (ρ_ (πŸ™_ C)).hom