English
For an A-module M, End_A(ι → M) is isomorphic (as A-algebras) to the matrix algebra M_{ι×ι}(End_A M) via the natural endomorphism-to-matrix correspondence.
Русский
Для A-модуля M существует изоморфизм как A-алгебр: End_A(ι → M) ≅_A M_{ι×ι}(End_A M) по естественной correspondence между эндоморфизмами и матрицами.
LaTeX
$$$\\mathrm{End}_A(\\iota \\to M) \\cong_A \\mathrm{M}_{\\iota\\times\\iota}(\\mathrm{End}_A M)$$$
Lean4
/-- Let `M` be an `A`-module. Every `A`-linear map `Mⁿ → Mⁿ` corresponds to a `n×n`-matrix whose entries
are `R`-linear maps `M → M`. In another word, we have`End(Mⁿ) ≅ Matₙₓₙ(End(M))` defined by:
`(f : Mⁿ → Mⁿ) ↦ (x ↦ f (0, ..., x at j-th position, ..., 0) i)ᵢⱼ` and
`m : Matₙₓₙ(End(M)) ↦ (v ↦ ∑ⱼ mᵢⱼ(vⱼ))`.
See also `LinearMap.toMatrix'`
-/
@[simps!]
def endVecAlgEquivMatrixEnd : Module.End A (ι → M) ≃ₐ[R] Matrix ι ι (Module.End A M)
where
__ := endVecRingEquivMatrixEnd ι A M
commutes'
r := by
ext
simp only [endVecRingEquivMatrixEnd, RingEquiv.toEquiv_eq_coe, Module.algebraMap_end_eq_smul_id, Equiv.toFun_as_coe,
EquivLike.coe_coe, RingEquiv.coe_mk, Equiv.coe_fn_mk, LinearMap.smul_apply, id_coe, id_eq, Pi.smul_apply,
Pi.single_apply, smul_ite, smul_zero, LinearMap.coe_mk, AddHom.coe_mk, algebraMap_matrix_apply]
split_ifs <;> rfl
