curriedTensorPre — Mathlib

English

Tensoring a commutative monoid object with the tensor unit on the left preserves commutativity.

Русский

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

LaTeX

$$$\text{IsCommMonObj}(M \otimes \mathbb{1}_C)$$$

Lean4

/-- The bifunctor `F - ⊗ F -`. -/
abbrev curriedTensorPre (F : C ⥤ D) : C ⥤ C ⥤ D :=
  (whiskeringLeft₂ _).obj F |>.obj F |>.obj (curriedTensor D)

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