leftComm — Mathlib

English

There is an isomorphism exchanging the leftmost factor with the middle two in a triple tensor product: A ⊗ (B ⊗ C) ≅ B ⊗ (A ⊗ C).

Русский

Существует изоморфизм, переставляющий первый и второй факторы в тройном тензорном произведении: A ⊗ (B ⊗ C) ≅ B ⊗ (A ⊗ C).

LaTeX

$$A ⊗_R (B ⊗_R C) ≅_R B ⊗_R (A ⊗_R C)$$

Lean4

/-- Tensor product of algebras analogue of `mul_left_comm`.

This is the algebra version of `TensorProduct.leftComm`. -/
def leftComm : A ⊗[R] (B ⊗[R] C) ≃ₐ[R] B ⊗[R] (A ⊗[R] C) :=
  (Algebra.TensorProduct.assoc R R A B C).symm.trans <|
    (congr (Algebra.TensorProduct.comm R A B) .refl).trans <| TensorProduct.assoc R R B A C

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