English
The action map (lsmul R B M a) as a linear map equals the scalar action a • ·.
Русский
Действие отображается как линейное отображение, совпадающее с действием скаляра a • _.
LaTeX
$$$\bigl(\mathrm{lsmul}\;R\;B\;M\;a\bigr) = (a \cdot \;\cdot )$$$
Lean4
/-- The `R`-algebra morphism `A → End (M)` corresponding to the representation of the algebra `A`
on the `B`-module `M`.
This is a stronger version of `DistribMulAction.toLinearMap`, and could also have been
called `Algebra.toModuleEnd`.
The typeclasses correspond to the situation where the types act on each other as
```
R ----→ B
| ⟍ |
| ⟍ |
↓ ↘ ↓
A ----→ M
```
where the diagram commutes, the action by `R` commutes with everything, and the action by `A` and
`B` on `M` commute.
Typically this is most useful with `B = R` as `Algebra.lsmul R R A : A →ₐ[R] Module.End R M`.
However this can be used to get the fact that left-multiplication by `A` is right `A`-linear, and
vice versa, as
```lean
example : A →ₐ[R] Module.End Aᵐᵒᵖ A := Algebra.lsmul R Aᵐᵒᵖ A
example : Aᵐᵒᵖ →ₐ[R] Module.End A A := Algebra.lsmul R A A
```
respectively; though `LinearMap.mulLeft` and `LinearMap.mulRight` can also be used here.
-/
def lsmul : A →ₐ[R] Module.End B M where
toFun := DistribMulAction.toLinearMap B M
map_one' := LinearMap.ext fun _ => one_smul A _
map_mul' a b := LinearMap.ext <| smul_assoc a b
map_zero' := LinearMap.ext fun _ => zero_smul A _
map_add' _a _b := LinearMap.ext fun _ => add_smul _ _ _
commutes' r := LinearMap.ext <| algebraMap_smul A r
