leftAssocTensor — Mathlib

English

The map on morphisms induced by left-associated triple tensor is given by f ↦ f.1 ⊗ f.2.1 ⊗ f.2.2.

Русский

Отображение на морфизмах, индуцированное левосторонне-ассоциированным тройным тензором, задаётся как f ↦ f.1 ⊗ f.2.1 ⊗ f.2.2.

LaTeX

$$$ (leftAssocTensor C).map f = (f.1 \\otimes f.2.1) \\otimes f.2.2. $$$

Lean4

/-- The left-associated triple tensor product as a functor. -/
def leftAssocTensor : C × C × C ⥤ C where
  obj X := (X.1 ⊗ X.2.1) ⊗ X.2.2
  map {X Y : C × C × C} (f : X ⟶ Y) := (f.1 ⊗ₘ f.2.1) ⊗ₘ f.2.2

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