English
If each f i is a linearly independent family, then the family of finsupp singles with i-indexed components, namely ix ↦ single ix.1 (f ix.1 ix.2), is linearly independent.
Русский
Если для каждого i множество векторов f_i линейно независимо, то семейство элементов вида single i (f_i) в Finsupp-области линейно независимо.
LaTeX
$$$\\text{LinearIndependent } R\\;\\bigl(\\lambda x. \\mathrm{single}_{x.1}(f_{x.1}(x.2))\\bigr)$$$
Lean4
theorem linearIndependent_single (hf : ∀ i, LinearIndependent R (f i)) :
LinearIndependent R fun ix : Σ i, φ i ↦ single ix.1 (f ix.1 ix.2) := by
classical
have :
linearCombination R (fun ix : Σ i, φ i ↦ single ix.1 (f ix.1 ix.2)) =
DFinsupp.mapRange.linearMap (fun i ↦ linearCombination R (f i)) ∘ₗ (sigmaFinsuppLequivDFinsupp R).toLinearMap :=
by ext; simp
rw [LinearIndependent, this]
exact ((DFinsupp.mapRange_injective _ fun _ ↦ map_zero _).mpr hf).comp (Equiv.injective _)
