tensor_left_iff — Mathlib

English

The left-associated triple tensor product is naturally isomorphic to the right-associated one, via the associator; this is realized by a natural isomorphism between the left-associated and right-associated triple tensor functors.

Русский

Левоассоциированное тройное тензорирование естественным образом изоморфно правому, посредством ассоциатора; существует естественным образом изоморфность между левосторонним и правосторонним тройным тензором.

LaTeX

$$$ \\text{leftAssocTensor} \\cong \\text{rightAssocTensor} \\quad \\text{via} \\quad \\text{associator}.$$

Lean4

theorem tensor_left_iff {X Y : C} (f g : X ⟶ Y) : 𝟙 (𝟙_ C) ⊗ₘ f = 𝟙 (𝟙_ C) ⊗ₘ g ↔ f = g := by simp

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