curriedTensorInsertFunctor₁

Mathlib.CategoryTheory.Monoidal.Multifunctor

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MonoidalCategory.curriedTensorInsertFunctor₁

← MathLib Explorer

English

The tensor of two commutative monoid objects inherits commutativity.

Русский

Тензор двух коммутативных моноидальных объектов наследует коммутативность.

LaTeX

$$$\text{IsCommMonObj}(M \otimes N)$$$

Lean4

/-- The bifunctor `(F -) ⊗ -`. -/
abbrev curriedTensorInsertFunctor₁ (F : C ⥤ D) : C ⥤ D ⥤ D :=
  (((whiskeringLeft₂ _).obj F).obj (𝟭 D)).obj (curriedTensor D)

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

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

Разделы

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

Аффилиация

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