associator

Mathlib.CategoryTheory.Localization.Monoidal

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

Lean4

/-- The associator in the localized monoidal category `LocalizedMonoidal L W ε`. -/
noncomputable def associator :
    bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε) ≅
      bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε) :=
  Localization.associator L' L' L' L' L' L' W W W W W (curriedAssociatorNatIso C) (tensorBifunctor L W ε)
    (tensorBifunctor L W ε) (tensorBifunctor L W ε) (tensorBifunctor L W ε)

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

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

Разделы

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

Аффилиация

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