English
Independence of submodules implies that any choice of nonzero representative vectors from each submodule is a linearly independent family.
Русский
Независимость подмодулей следует из того, что любой выбор ненулевых векторов из каждого подмодуля образует линейно независимую систему.
LaTeX
$$linearIndependent [NoZeroSMulDivisors R N] {p} (hp : iSupIndep p) {v} (hv : ∀ i, v i ∈ p i) (hv' : ∀ i, v i ≠ 0) : LinearIndependent R v$$
Lean4
/-- If a family of submodules is independent, then a choice of nonzero vector from each submodule
forms a linearly independent family.
See also `iSupIndep.linearIndependent'`. -/
theorem linearIndependent [NoZeroSMulDivisors R N] {ι} (p : ι → Submodule R N) (hp : iSupIndep p) {v : ι → N}
(hv : ∀ i, v i ∈ p i) (hv' : ∀ i, v i ≠ 0) : LinearIndependent R v :=
by
let _ := Classical.decEq ι
let _ := Classical.decEq R
rw [linearIndependent_iff]
intro l hl
let a := DFinsupp.mapRange.linearMap (fun i => LinearMap.toSpanSingleton R (p i) ⟨v i, hv i⟩) l.toDFinsupp
have ha : a = 0 := by
apply hp.dfinsupp_lsum_injective
rwa [← lsum_comp_mapRange_toSpanSingleton _ hv] at hl
ext i
apply smul_left_injective R (hv' i)
have : l i • v i = a i := rfl
simp only [coe_zero, Pi.zero_apply, ZeroMemClass.coe_zero, smul_eq_zero, ha] at this
simpa
