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 CategoryTheory.MonoidalCategory.leftUnitor_tensor_hom'' {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] (X Y : C) : CategoryStruct.comp (associator (tensorUnit C) X Y).hom (leftUnitor (tensorObj X Y)).hom = tensorHom (leftUnitor X).hom (CategoryStruct.id Y)

theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor_hom''_assoc {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] (X Y : C) {Z : C} (h : tensorObj X Y ⟶ Z) : CategoryStruct.comp (associator (tensorUnit C) X Y).hom (CategoryStruct.comp (leftUnitor (tensorObj X Y)).hom h) = CategoryStruct.comp (tensorHom (leftUnitor X).hom (CategoryStruct.id Y)) h

@[deprecated CategoryTheory.MonoidalCategory.leftUnitor_tensor_hom'' (since := "2025-06-24")]

theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor'' {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] (X Y : C) : CategoryStruct.comp (associator (tensorUnit C) X Y).hom (leftUnitor (tensorObj X Y)).hom = tensorHom (leftUnitor X).hom (CategoryStruct.id Y)

Alias of CategoryTheory.MonoidalCategory.leftUnitor_tensor_hom''.

theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor_hom' {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] (X Y : C) : (leftUnitor (tensorObj X Y)).hom = CategoryStruct.comp (associator (tensorUnit C) X Y).inv (tensorHom (leftUnitor X).hom (CategoryStruct.id Y))

theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor_hom'_assoc {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] (X Y : C) {Z : C} (h : tensorObj X Y ⟶ Z) : CategoryStruct.comp (leftUnitor (tensorObj X Y)).hom h = CategoryStruct.comp (associator (tensorUnit C) X Y).inv (CategoryStruct.comp (tensorHom (leftUnitor X).hom (CategoryStruct.id Y)) h)

@[deprecated CategoryTheory.MonoidalCategory.leftUnitor_tensor_hom' (since := "2025-06-24")]

theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor' {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] (X Y : C) : (leftUnitor (tensorObj X Y)).hom = CategoryStruct.comp (associator (tensorUnit C) X Y).inv (tensorHom (leftUnitor X).hom (CategoryStruct.id Y))

Alias of CategoryTheory.MonoidalCategory.leftUnitor_tensor_hom'.

theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor_inv' {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] (X Y : C) : (leftUnitor (tensorObj X Y)).inv = CategoryStruct.comp (tensorHom (leftUnitor X).inv (CategoryStruct.id Y)) (associator (tensorUnit C) X Y).hom

theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor_inv'_assoc {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] (X Y : C) {Z : C} (h : tensorObj (tensorUnit C) (tensorObj X Y) ⟶ Z) : CategoryStruct.comp (leftUnitor (tensorObj X Y)).inv h = CategoryStruct.comp (tensorHom (leftUnitor X).inv (CategoryStruct.id Y)) (CategoryStruct.comp (associator (tensorUnit C) X Y).hom h)

theorem CategoryTheory.MonoidalCategory.id_tensor_rightUnitor_inv {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] (X Y : C) : tensorHom (CategoryStruct.id X) (rightUnitor Y).inv = CategoryStruct.comp (rightUnitor (tensorObj X Y)).inv (associator X Y (tensorUnit C)).hom

theorem CategoryTheory.MonoidalCategory.id_tensor_rightUnitor_inv_assoc {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] (X Y : C) {Z : C} (h : tensorObj X (tensorObj Y (tensorUnit C)) ⟶ Z) : CategoryStruct.comp (tensorHom (CategoryStruct.id X) (rightUnitor Y).inv) h = CategoryStruct.comp (rightUnitor (tensorObj X Y)).inv (CategoryStruct.comp (associator X Y (tensorUnit C)).hom h)

theorem CategoryTheory.MonoidalCategory.leftUnitor_inv_tensor_id {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] (X Y : C) : tensorHom (leftUnitor X).inv (CategoryStruct.id Y) = CategoryStruct.comp (leftUnitor (tensorObj X Y)).inv (associator (tensorUnit C) X Y).inv

theorem CategoryTheory.MonoidalCategory.leftUnitor_inv_tensor_id_assoc {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] (X Y : C) {Z : C} (h : tensorObj (tensorObj (tensorUnit C) X) Y ⟶ Z) : CategoryStruct.comp (tensorHom (leftUnitor X).inv (CategoryStruct.id Y)) h = CategoryStruct.comp (leftUnitor (tensorObj X Y)).inv (CategoryStruct.comp (associator (tensorUnit C) X Y).inv h)

theorem CategoryTheory.MonoidalCategory.pentagon_inv_inv_hom {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] (W X Y Z : C) : CategoryStruct.comp (associator W (tensorObj X Y) Z).inv (CategoryStruct.comp (tensorHom (associator W X Y).inv (CategoryStruct.id Z)) (associator (tensorObj W X) Y Z).hom) = CategoryStruct.comp (tensorHom (CategoryStruct.id W) (associator X Y Z).hom) (associator W X (tensorObj Y Z)).inv

theorem CategoryTheory.MonoidalCategory.pentagon_inv_inv_hom_assoc {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] (W X Y Z : C) {Z✝ : C} (h : tensorObj (tensorObj W X) (tensorObj Y Z) ⟶ Z✝) : CategoryStruct.comp (associator W (tensorObj X Y) Z).inv (CategoryStruct.comp (tensorHom (associator W X Y).inv (CategoryStruct.id Z)) (CategoryStruct.comp (associator (tensorObj W X) Y Z).hom h)) = CategoryStruct.comp (tensorHom (CategoryStruct.id W) (associator X Y Z).hom) (CategoryStruct.comp (associator W X (tensorObj Y Z)).inv h)

theorem CategoryTheory.MonoidalCategory.unitors_equal {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] : (leftUnitor (tensorUnit C)).hom = (rightUnitor (tensorUnit C)).hom

theorem CategoryTheory.MonoidalCategory.unitors_inv_equal {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] : (leftUnitor (tensorUnit C)).inv = (rightUnitor (tensorUnit C)).inv

theorem CategoryTheory.MonoidalCategory.pentagon_hom_inv {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] {W X Y Z : C} : CategoryStruct.comp (associator W X (tensorObj Y Z)).hom (tensorHom (CategoryStruct.id W) (associator X Y Z).inv) = CategoryStruct.comp (associator (tensorObj W X) Y Z).inv (CategoryStruct.comp (tensorHom (associator W X Y).hom (CategoryStruct.id Z)) (associator W (tensorObj X Y) Z).hom)

theorem CategoryTheory.MonoidalCategory.pentagon_hom_inv_assoc {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] {W X Y Z Z✝ : C} (h : tensorObj W (tensorObj (tensorObj X Y) Z) ⟶ Z✝) : CategoryStruct.comp (associator W X (tensorObj Y Z)).hom (CategoryStruct.comp (tensorHom (CategoryStruct.id W) (associator X Y Z).inv) h) = CategoryStruct.comp (associator (tensorObj W X) Y Z).inv (CategoryStruct.comp (tensorHom (associator W X Y).hom (CategoryStruct.id Z)) (CategoryStruct.comp (associator W (tensorObj X Y) Z).hom h))

theorem CategoryTheory.MonoidalCategory.pentagon_inv_hom {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] (W X Y Z : C) : CategoryStruct.comp (associator (tensorObj W X) Y Z).inv (tensorHom (associator W X Y).hom (CategoryStruct.id Z)) = CategoryStruct.comp (associator W X (tensorObj Y Z)).hom (CategoryStruct.comp (tensorHom (CategoryStruct.id W) (associator X Y Z).inv) (associator W (tensorObj X Y) Z).inv)

theorem CategoryTheory.MonoidalCategory.pentagon_inv_hom_assoc {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] (W X Y Z : C) {Z✝ : C} (h : tensorObj (tensorObj W (tensorObj X Y)) Z ⟶ Z✝) : CategoryStruct.comp (associator (tensorObj W X) Y Z).inv (CategoryStruct.comp (tensorHom (associator W X Y).hom (CategoryStruct.id Z)) h) = CategoryStruct.comp (associator W X (tensorObj Y Z)).hom (CategoryStruct.comp (tensorHom (CategoryStruct.id W) (associator X Y Z).inv) (CategoryStruct.comp (associator W (tensorObj X Y) Z).inv h))