tensorTensorTensorComm — Mathlib

English

There is a compatibility between two-layer tensor products when exchanging middle components, yielding a new associativity-like symmetry.

Русский

Существует совместимость между двумя слоями тензорных произведений при перестановке серединных компонентов, образующая симметрию, близкую к ассоциативности.

LaTeX

$$tensorTensorTensorComm R R' S T A B C D = ...$$

Lean4

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

This is the algebra version of `TensorProduct.AlgebraTensorModule.tensorTensorTensorComm`. -/
def tensorTensorTensorComm : A ⊗[R'] B ⊗[S] (C ⊗[R] D) ≃ₐ[T] A ⊗[S] C ⊗[R'] (B ⊗[R] D) :=
  AlgEquiv.ofLinearEquiv (TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R' S T A B C D) rfl
    (LinearMap.map_mul_iff _ |>.mpr <| by ext; simp)

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