English
For matrices, the left-right multiplication map has an explicit inverse given by a sum over standard basis elements; this inverse undoes the left-right multiplication map.
Русский
Для матриц существует явный обратный отображение для mulLeftRight, записанный как сумма по базису, который обращает процесс умножения слева и справа.
LaTeX
$$$ (\text{mulLeftRightMatrix_inv } R n) \circ (\text{mulLeftRight } R (\text{Matrix } n\, n\, R)) = \mathrm{id}$$$
Lean4
/-- The canonical map from `A ⊗[R] Aᵐᵒᵖ` to `Module.End R A` where
`a ⊗ b` maps to `f : x ↦ a * x * b`. -/
def mulLeftRight : (A ⊗[R] Aᵐᵒᵖ) →ₐ[R] Module.End R A :=
letI : Module (A ⊗[R] Aᵐᵒᵖ) A := TensorProduct.Algebra.module
letI : IsScalarTower R (A ⊗[R] Aᵐᵒᵖ) A :=
{
smul_assoc := fun r ab a ↦
by
change TensorProduct.Algebra.moduleAux _ _ = _ • TensorProduct.Algebra.moduleAux _ _
simp }
Algebra.lsmul R (A := A ⊗[R] Aᵐᵒᵖ) R A
