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

theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor_inv' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X 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 (𝟙_ C) X Y).hom

theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor_inv'_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X Y : C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj (𝟙_ C) (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 (𝟙_ C) X Y).hom h)

theorem CategoryTheory.MonoidalCategory.id_tensor_rightUnitor_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X 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 (𝟙_ C)).hom

theorem CategoryTheory.MonoidalCategory.id_tensor_rightUnitor_inv_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X Y : C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorObj Y (𝟙_ C)) ⟶ 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 (𝟙_ C)).hom h)

theorem CategoryTheory.MonoidalCategory.leftUnitor_inv_tensor_id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X 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 (𝟙_ C) X Y).inv

theorem CategoryTheory.MonoidalCategory.leftUnitor_inv_tensor_id_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (X Y : C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj (𝟙_ C) 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 (𝟙_ C) X Y).inv h)

theorem CategoryTheory.MonoidalCategory.pentagon_inv_inv_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (W X Y 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

theorem CategoryTheory.MonoidalCategory.pentagon_inv_inv_hom_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (W X Y 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.unitors_equal {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] : (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).hom = (CategoryTheory.MonoidalCategory.rightUnitor (𝟙_ 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 (𝟙_ C)).inv = (CategoryTheory.MonoidalCategory.rightUnitor (𝟙_ C)).inv

theorem CategoryTheory.MonoidalCategory.pentagon_hom_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {W X Y 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_hom_inv_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] {W X Y Z 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_inv_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (W X Y 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)

theorem CategoryTheory.MonoidalCategory.pentagon_inv_hom_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.MonoidalCategory C] (W X Y 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))