tensorTensorTensorComm — Mathlib

English

The heterobasic rightComm equals the standard rightComm.

Русский

Гетеробазовый rightComm совпадает с обычным rightComm.

LaTeX

$$$\mathrm{rightComm}_{R S B M P Q} = \mathrm{TensorProduct.rightComm}_{R M P Q}$$$

Lean4

/-- Heterobasic version of `tensorTensorTensorComm`.

Suppose we have towers of algebras `R → S → B` and `R → A → B`, and
a `B`-module `M`, `S`-module `N`, `A`-module `P`, `R`-module `Q`, then
```
(M ⊗ˢ N)      ⎛ M ⎞ ⊗ˢ ⎛ N ⎞
 ⊗ᴬ       ≅ᴮ  ⎜ ⊗ᴬ⎟    ⎜ ⊗ᴿ⎟
(P ⊗ᴿ Q)      ⎝ P ⎠    ⎝ Q ⎠
```
-/
def tensorTensorTensorComm : (M ⊗[S] N) ⊗[A] (P ⊗[R] Q) ≃ₗ[B] (M ⊗[A] P) ⊗[S] (N ⊗[R] Q) :=
  (assoc R A B (M ⊗[S] N) P Q).symm ≪≫ₗ congr (rightComm A S B M N P) (.refl R Q) ≪≫ₗ assoc R _ _ (M ⊗[A] P) N Q

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