tensor — Mathlib

English

The object underlying the left-associated triple tensor of a pair X = (X1, X2) is (X1 ⊗ X2.1) ⊗ X2.2, i.e., the triple tensor yields precisely the left-associated product.

Русский

Объект, лежащий в основе лево-ассоциированного тройного тензора пары X = (X1, X2), равен (X1 ⊗ X2.1) ⊗ X2.2.

LaTeX

$$$ (leftAssocTensor C).obj X = (X.1 \\otimes X.2.1) \\otimes X.2.2. $$$

Lean4

/-- The tensor product expressed as a functor. -/
@[simps]
def tensor : C × C ⥤ C where
  obj X := X.1 ⊗ X.2
  map {X Y : C × C} (f : X ⟶ Y) := f.1 ⊗ₘ f.2

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