equivFun — Mathlib

English

For a finite index set ι, there is a canonical linear equivalence between M and ι → R, given by the basis equivFun.

Русский

Для конечного множества индексов ι существует каноническое линейное эквивалентное отображение между M и ι → R, заданное через эквивияцию базиса.

LaTeX

$$$M \simeq_R ι \to R$ via $b.equivFun$$$

Lean4

/-- A module over `R` with a finite basis is linearly equivalent to functions from its basis to `R`.
-/
def equivFun [Finite ι] (b : Basis ι R M) : M ≃ₗ[R] ι → R :=
  LinearEquiv.trans b.repr
    ({ Finsupp.equivFunOnFinite with
        toFun := (↑)
        map_add' := Finsupp.coe_add
        map_smul' := Finsupp.coe_smul } :
      (ι →₀ R) ≃ₗ[R] ι → R)

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