endVecRingEquivMatrixEnd — Mathlib

English

There is a canonical isomorphism between the A-endomorphisms of the free A-module ι → M and the matrices ι × ι with entries in End_A(M).

Русский

Существует каноническое изоморирование между End_A(ι → M) и матрицами размером ι × ι с элементами в End_A(M).

LaTeX

$$$\\operatorname{End}_A(\\iota \\to M) \\cong M_{\\iota \\times \\iota}(\\operatorname{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 `A`-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'`
-/
@[simp]
def endVecRingEquivMatrixEnd : Module.End A (ι → M) ≃+* Matrix ι ι (Module.End A M)
    where
  toFun f i
    j :=
    { toFun := fun x ↦ f (Pi.single j x) i
      map_add' := fun x y ↦ by simp [Pi.single_add]
      map_smul' := fun x y ↦ by simp [Pi.single_smul] }
  invFun
    m :=
    { toFun := fun x i ↦ ∑ j, m i j (x j)
      map_add' := by intros; ext; simp [Finset.sum_add_distrib]
      map_smul' := by intros; ext; simp [Finset.smul_sum] }
  left_inv
    f := by
    ext i x j
    simp only [LinearMap.coe_mk, AddHom.coe_mk, coe_comp, coe_single, Function.comp_apply]
    rw [← Fintype.sum_apply, ← map_sum]
    exact congr_arg₂ _ (by aesop) rfl
  right_inv m := by ext; simp [Pi.single_apply, apply_ite]
  map_mul' f
    g := by
    ext
    simp only [Module.End.mul_apply, LinearMap.coe_mk, AddHom.coe_mk, Matrix.mul_apply, coeFn_sum, Finset.sum_apply]
    rw [← Fintype.sum_apply, ← map_sum]
    exact congr_arg₂ _ (by aesop) rfl
  map_add' f g := by ext; simp

Похожие утверждения