English
The image of finsuppTotal is exactly I · span R(Set.range v).
Русский
Образ отображения finsuppTotal равен I · span R(Set.range v).
LaTeX
$$$\\operatorname{range}(\\mathrm{finsuppTotal}_{\\iota,M,I,v}) = I \\cdot \\operatorname{span}(\\operatorname{Set.range} v)$$$
Lean4
theorem range_finsuppTotal : LinearMap.range (finsuppTotal ι M I v) = I • Submodule.span R (Set.range v) :=
by
ext
rw [Submodule.mem_ideal_smul_span_iff_exists_sum]
refine ⟨fun ⟨f, h⟩ => ⟨Finsupp.mapRange.linearMap I.subtype f, fun i => (f i).2, h⟩, ?_⟩
rintro ⟨a, ha, rfl⟩
classical
refine
⟨a.mapRange (fun r => if h : r ∈ I then ⟨r, h⟩ else 0) (by simp only [Submodule.zero_mem, ↓reduceDIte]; rfl), ?_⟩
rw [finsuppTotal_apply, Finsupp.sum_mapRange_index]
· apply Finsupp.sum_congr
intro i _
rw [dif_pos (ha i)]
· exact fun _ => zero_smul _ _
