Documentation

Mathlib.CategoryTheory.Monoidal.CoherenceLemmas

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.

source
theorem CategoryTheory.MonoidalCategory.leftUnitor_tensor'' {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] (X Y : C) :
CategoryStruct.comp (associator (šŸ™_ C) X Y).hom (leftUnitor (tensorObj X Y)).hom = tensorHom (leftUnitor X).hom (CategoryStruct.id Y)
source
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) :
CategoryStruct.comp (associator (šŸ™_ C) X Y).hom (CategoryStruct.comp (leftUnitor (tensorObj X Y)).hom h) = CategoryStruct.comp (tensorHom (leftUnitor X).hom (CategoryStruct.id Y)) h
source
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 (šŸ™_ C) X Y).inv (tensorHom (leftUnitor X).hom (CategoryStruct.id Y))
source
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) :
CategoryStruct.comp (leftUnitor (tensorObj X Y)).hom h = CategoryStruct.comp (associator (šŸ™_ C) X Y).inv (CategoryStruct.comp (tensorHom (leftUnitor X).hom (CategoryStruct.id Y)) h)
source
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 (šŸ™_ C) X Y).hom
source
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) :
CategoryStruct.comp (leftUnitor (tensorObj X Y)).inv h = CategoryStruct.comp (tensorHom (leftUnitor X).inv (CategoryStruct.id Y)) (CategoryStruct.comp (associator (šŸ™_ C) X Y).hom h)
source
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 (šŸ™_ C)).hom
source
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) :
CategoryStruct.comp (tensorHom (CategoryStruct.id X) (rightUnitor Y).inv) h = CategoryStruct.comp (rightUnitor (tensorObj X Y)).inv (CategoryStruct.comp (associator X Y (šŸ™_ C)).hom h)
source
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 (šŸ™_ C) X Y).inv
source
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) :
CategoryStruct.comp (tensorHom (leftUnitor X).inv (CategoryStruct.id Y)) h = CategoryStruct.comp (leftUnitor (tensorObj X Y)).inv (CategoryStruct.comp (associator (šŸ™_ C) X Y).inv h)
source
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
source
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)
source
theorem CategoryTheory.MonoidalCategory.unitors_equal {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] :
(leftUnitor (šŸ™_ C)).hom = (rightUnitor (šŸ™_ C)).hom
source
theorem CategoryTheory.MonoidalCategory.unitors_inv_equal {C : Type u_1} [Category.{u_2, u_1} C] [MonoidalCategory C] :
(leftUnitor (šŸ™_ C)).inv = (rightUnitor (šŸ™_ C)).inv
source
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)
source
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))
source
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)
source
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))