English
On simple tensors, rightComm acts by swapping the outer factors: rightComm (m ⊗ (p ⊗ q)) = (m ⊗ q) ⊗ p.
Русский
На простых тензорах правый коммутатор меняет местами внешние факторы: rightComm(m ⊗ (p ⊗ q)) = (m ⊗ q) ⊗ p.
LaTeX
$$$\text{rightComm}_{R S B M P Q}( (m\otimes p)\otimes q ) = (m\otimes q)\otimes p$$$
Lean4
/-- A tensor product analogue of `mul_right_comm`.
Suppose we have a diagram of algebras `R → B ← S`,
and a `B`-module `M`, `S`-module `P`, `R`-module `Q`, then
```
(M ⊗ˢ P) ⎛ M ⎞ ⊗ˢ P
⊗ᴿ ≅ᴮ ⎜ ⊗ᴿ⎟
Q ⎝ Q ⎠
```
-/
def rightComm : (M ⊗[S] P) ⊗[R] Q ≃ₗ[B] (M ⊗[R] Q) ⊗[S] P :=
LinearEquiv.ofLinear
(lift
(lift (LinearMap.lflip.toLinearMap ∘ₗ (AlgebraTensorModule.mk _ _ _ _).compr₂ (AlgebraTensorModule.mk _ _ _ _))))
(lift
(lift (LinearMap.lflip.toLinearMap ∘ₗ (AlgebraTensorModule.mk _ _ _ _).compr₂ (AlgebraTensorModule.mk _ _ _ _))))
(by ext; simp) (by ext; simp)
