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

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

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

@[simp]

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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