linearCombinationEquiv — Mathlib

English

There is a canonical linear equivalence between the space of finitely supported functions on the index set and the span of the given independent family.

Русский

Существует каноническое линейное эквивалентство между пространством функционалов с конечной поддержкой и гладким охватом заданной линейно независимой семейства.

LaTeX

$$$\\text{linearCombinationEquiv} : (\\iota \\to_R \\text{M})^0 \\simeq_R \\operatorname{span}_R(\\operatorname{range} v)$$$

Lean4

/-- Canonical isomorphism between linear combinations and the span of linearly independent vectors.
-/
@[simps (rhsMd := default) apply_coe symm_apply]
def linearCombinationEquiv (hv : LinearIndependent R v) : (ι →₀ R) ≃ₗ[R] span R (range v) :=
  by
  refine
    LinearEquiv.ofBijective (LinearMap.codRestrict (span R (range v)) (Finsupp.linearCombination R v) ?_)
      ⟨hv.codRestrict _, ?_⟩
  · simp_rw [← Finsupp.range_linearCombination]; exact fun c ↦ ⟨c, rfl⟩
  rw [← LinearMap.range_eq_top, LinearMap.range_eq_map, LinearMap.map_codRestrict, ← LinearMap.range_le_iff_comap,
    range_subtype, Submodule.map_top, Finsupp.range_linearCombination]

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