instMonoidalCategoryStruct

Mathlib.Algebra.Category.CoalgCat.Monoidal

URI: https://scilib.ai/kg/mathlib#CoalgCat.instMonoidalCategoryStruct

Lean4

@[simps]
noncomputable instance instMonoidalCategoryStruct : MonoidalCategoryStruct.{u} (CoalgCat R)
    where
  tensorObj X Y := of R (X ⊗[R] Y)
  whiskerLeft X _ _ f := ofHom (f.1.lTensor X)
  whiskerRight f X := ofHom (f.1.rTensor X)
  tensorHom f g := ofHom (Coalgebra.TensorProduct.map f.1 g.1)
  tensorUnit := CoalgCat.of R R
  associator X Y Z := (Coalgebra.TensorProduct.assoc R R X Y Z).toCoalgIso
  leftUnitor X := (Coalgebra.TensorProduct.lid R X).toCoalgIso
  rightUnitor X := (Coalgebra.TensorProduct.rid R R X).toCoalgIso

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

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

Разделы

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

Аффилиация

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