leftAssocTensor_map — Mathlib

English

The left-associated triple tensor map is f.1 ⊗ f.2.1 ⊗ f.2.2 for a morphism f, i.e., the natural action on components.

Русский

Картирование лево-ассоциированного тройного тензора действует на компоненты так: f.1 ⊗ f.2.1 ⊗ f.2.2.

LaTeX

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

Lean4

@[simp]
theorem leftAssocTensor_map {X Y} (f : X ⟶ Y) : (leftAssocTensor C).map f = (f.1 ⊗ₘ f.2.1) ⊗ₘ f.2.2 :=
  rfl

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