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}
[Category.{u_2, u_1} C]
[MonoidalCategory C]
(X Y : C)
{Z : C}
(h : tensorObj X Y ā¶ Z)
:
theorem
CategoryTheory.MonoidalCategory.leftUnitor_tensor'_assoc
{C : Type u_1}
[Category.{u_2, u_1} C]
[MonoidalCategory C]
(X Y : C)
{Z : C}
(h : tensorObj X Y ā¶ Z)
:
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 (š_ C) (tensorObj X Y) ā¶ Z)
:
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 (š_ C)) ā¶ Z)
:
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 (š_ C) X) Y ā¶ Z)
:
theorem
CategoryTheory.MonoidalCategory.pentagon_inv_inv_hom
{C : Type u_1}
[Category.{u_2, u_1} C]
[MonoidalCategory C]
(W X Y Z : C)
:
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.pentagon_hom_inv
{C : Type u_1}
[Category.{u_2, u_1} C]
[MonoidalCategory C]
{W X Y Z : C}
:
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)
:
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))