English
For a ∈ A and M ∈ Matrix n n R, the action of toFunBilinear is a · M mapped by the algebra map.
Русский
Для a ∈ A и M ∈ Matrix(n,n,R) действие toFunBilinear задаётся как a · map(algebraMap_R^A)(M).
LaTeX
$$$ toFunBilinear(n,R,A)(a,M) = a \cdot M.map(\mathrm{algebraMap}_{R}^{A}) $$$
Lean4
/-- The function `(A ⊗[R] Matrix n n R) →ₐ[R] Matrix n n A`, as an algebra homomorphism.
-/
def toFunAlgHom : A ⊗[R] Matrix n n R →ₐ[R] Matrix n n A :=
algHomOfLinearMapTensorProduct (toFunLinear n R A)
(by
intros
simp_rw [toFunLinear, lift.tmul, toFunBilinear_apply, Matrix.map_mul]
ext
dsimp
simp_rw [Matrix.mul_apply, Matrix.smul_apply, Matrix.map_apply, smul_eq_mul, Finset.mul_sum, _root_.mul_assoc,
Algebra.left_comm])
(by
simp_rw [toFunLinear, lift.tmul, toFunBilinear_apply, Matrix.map_one (algebraMap R A) (map_zero _) (map_one _),
one_smul])
