CoherenceLemmas

📁 Source: Mathlib/CategoryTheory/Monoidal/CoherenceLemmas.lean

Statistics

Metric	Count
Definitions	0
Theorems id_tensor_rightUnitor_inv, id_tensor_rightUnitor_inv_assoc, leftUnitor_inv_tensor_id, leftUnitor_inv_tensor_id_assoc, leftUnitor_tensor_hom', leftUnitor_tensor_hom'', leftUnitor_tensor_hom''_assoc, leftUnitor_tensor_hom'_assoc, leftUnitor_tensor_inv', leftUnitor_tensor_inv'_assoc, pentagon_hom_inv, pentagon_hom_inv_assoc, pentagon_inv_hom, pentagon_inv_hom_assoc, pentagon_inv_inv_hom, pentagon_inv_inv_hom_assoc, unitors_equal, unitors_inv_equal	18
Total	18

CategoryTheory.MonoidalCategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
id_tensor_rightUnitor_inv 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorHom toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.CategoryStruct.comp CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator	—	id_tensorHom whiskerLeft_rightUnitor_inv
id_tensor_rightUnitor_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.CategoryStruct.id CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' id_tensor_rightUnitor_inv
leftUnitor_inv_tensor_id 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorHom toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.MonoidalCategoryStruct.associator	—	tensorHom_id leftUnitor_inv_whiskerRight
leftUnitor_inv_tensor_id_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.CategoryStruct.id CategoryTheory.MonoidalCategoryStruct.associator	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftUnitor_inv_tensor_id
leftUnitor_tensor_hom' 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.CategoryStruct.id	—	tensorHom_id leftUnitor_whiskerRight CategoryTheory.Iso.inv_hom_id_assoc
leftUnitor_tensor_hom'' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.CategoryStruct.id	—	tensorHom_id leftUnitor_whiskerRight
leftUnitor_tensor_hom''_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.CategoryStruct.id	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftUnitor_tensor_hom''
leftUnitor_tensor_hom'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.CategoryStruct.id	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftUnitor_tensor_hom'
leftUnitor_tensor_inv' 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.tensorObj toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator	—	tensorHom_id leftUnitor_inv_whiskerRight CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
leftUnitor_tensor_inv'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftUnitor_tensor_inv'
pentagon_hom_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj toMonoidalCategoryStruct CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.CategoryStruct.id CategoryTheory.Iso.inv	—	id_tensorHom tensorHom_id pentagon_inv_hom_hom_hom_inv
pentagon_hom_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj toMonoidalCategoryStruct CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.CategoryStruct.id CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pentagon_hom_inv
pentagon_inv_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj toMonoidalCategoryStruct CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Iso.hom CategoryTheory.CategoryStruct.id	—	tensorHom_id id_tensorHom pentagon_hom_inv_inv_inv_hom
pentagon_inv_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj toMonoidalCategoryStruct CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Iso.hom CategoryTheory.CategoryStruct.id	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pentagon_inv_hom
pentagon_inv_inv_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj toMonoidalCategoryStruct CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom	—	tensorHom_id pentagon_inv_inv_hom_hom_inv id_tensorHom
pentagon_inv_inv_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj toMonoidalCategoryStruct CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pentagon_inv_inv_hom
unitors_equal 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	Mathlib.Tactic.Monoidal.mk_eq_of_naturality Mathlib.Tactic.Monoidal.naturality_leftUnitor Mathlib.Tactic.Monoidal.naturality_rightUnitor
unitors_inv_equal 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.tensorObj toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	Mathlib.Tactic.Monoidal.mk_eq_of_naturality CategoryTheory.Iso.symm_hom Mathlib.Tactic.Monoidal.naturality_inv Mathlib.Tactic.Monoidal.naturality_leftUnitor Mathlib.Tactic.Monoidal.naturality_rightUnitor

---

← Back to Index