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