English
Let b be an S-basis of M. An element m ∈ M lies in span_R(range b) if and only if all coordinates of m with respect to b lie in the image of algebraMap R S, i.e., in Set.range (algebraMap R S).
Русский
Пусть b — S-базис M. Элемент m ∈ M лежит в span_R(range b) тогда и только тогда, когда все координаты m по базе b лежат в образе алгебраического отображения algebraMap R S, т.е. в Set.range (algebraMap R S).
LaTeX
$$$m \\in \\text{span}_R(\\mathrm{range}\\, b) \\iff \\forall i,\\ m\\text{-координата}_i \\in \\mathrm{range}(\\mathrm{algebraMap}\\ R\\ S)$$$
Lean4
/-- Let `b` be an `S`-basis of `M`. Then `m : M` lies in the `R`-module spanned by `b` iff all the
coordinates of `m` on the basis `b` are in `R` (see `Basis.mem_span` for the case `R = S`). -/
theorem mem_span_iff_repr_mem (m : M) : m ∈ span R (Set.range b) ↔ ∀ i, b.repr m i ∈ Set.range (algebraMap R S) :=
by
refine ⟨fun hm i => ⟨(b.restrictScalars R).repr ⟨m, hm⟩ i, b.restrictScalars_repr_apply R ⟨m, hm⟩ i⟩, fun h => ?_⟩
rw [← b.linearCombination_repr m, Finsupp.linearCombination_apply S _]
refine sum_mem fun i _ => ?_
obtain ⟨_, h⟩ := h i
simp_rw [← h, algebraMap_smul]
exact smul_mem _ _ (subset_span (Set.mem_range_self i))
