monoidalCategory

Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

URI: https://scilib.ai/kg/mathlib#ModuleCat.monoidalCategory

Lean4

instance monoidalCategory : MonoidalCategory (ModuleCat.{u} R) :=
  MonoidalCategory.ofTensorHom (id_tensorHom_id := fun M N ↦ id_tensorHom_id M N) (tensorHom_comp_tensorHom :=
    fun f g h ↦ MonoidalCategory.tensorHom_comp_tensorHom f g h) (associator_naturality := fun f g h ↦
    MonoidalCategory.associator_naturality f g h) (leftUnitor_naturality := fun f ↦
    MonoidalCategory.leftUnitor_naturality f) (rightUnitor_naturality := fun f ↦ rightUnitor_naturality f) (pentagon :=
    fun M N K L ↦ pentagon M N K L) (triangle := fun M N ↦ triangle M N)

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru