monoidalCategoryStruct

Mathlib.CategoryTheory.Localization.Monoidal

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Localization.Monoidal.monoidalCategoryStruct

Lean4

noncomputable instance monoidalCategoryStruct : MonoidalCategoryStruct (LocalizedMonoidal L W ε)
    where
  tensorObj X Y := ((tensorBifunctor L W ε).obj X).obj Y
  whiskerLeft X _ _ g := ((tensorBifunctor L W ε).obj X).map g
  whiskerRight f Y := ((tensorBifunctor L W ε).map f).app Y
  tensorUnit := unit
  associator X Y Z := (((associator L W ε).app X).app Y).app Z
  leftUnitor Y := (leftUnitor L W ε).app Y
  rightUnitor X := (rightUnitor L W ε).app X

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

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

Разделы

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

Аффилиация

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