English
Let p_i be submodules of N indexed by ι and let v_i ∈ p_i for all i. Then the linear map obtained by summing the inclusions (p_i) into N after embedding v_i via the span-singleton construction is equal to the linear combination map that sends the family (v_i) to the finite sum ∑ i v_i. In other words, combining lsum with mapRange toSpanSingleton recovers the same map as Finsupp.linearCombination.
Русский
Набор подмодулей p_i ⊂ N (индексирован по ι) образует векторный набор {v_i} с v_i ∈ p_i. Тогда линейное отображение, получаемое суммированием вложений p_i в N после вложения v_i через отображение доSpanSingleton, совпадает с отображением линейной комбинации, отправляющим семейство v_i в ∑ i v_i. Иными словами, сочетание lsum с mapRange доSpanSingleton восстанавливает ту же линейную комбинацию, что и Finsupp.linearCombination.
LaTeX
$$$\left( \mathrm{lsum} \,\mathbb{N} \ f\_i\,(p_i).subtype \right) \circ \left( \left( \mathrm{mapRange}.\text{linearMap} \; f \right) \circ (\mathrm{finsuppLequivDFinsupp} \; R).toLinearMap \right) = \mathrm{Finsupp.linearCombination} R v$$$
Lean4
/-- Combining `DFinsupp.lsum` with `LinearMap.toSpanSingleton` is the same as
`Finsupp.linearCombination` -/
theorem lsum_comp_mapRange_toSpanSingleton [∀ m : R, Decidable (m ≠ 0)] (p : ι → Submodule R N) {v : ι → N}
(hv : ∀ i : ι, v i ∈ p i) :
(lsum ℕ fun i => (p i).subtype : _ →ₗ[R] _).comp
((mapRange.linearMap fun i => LinearMap.toSpanSingleton R (↥(p i)) ⟨v i, hv i⟩ : _ →ₗ[R] _).comp
(finsuppLequivDFinsupp R : (ι →₀ R) ≃ₗ[R] _).toLinearMap) =
Finsupp.linearCombination R v :=
by
ext
simp
