English
Let {v_i} be a family in M and suppose the iSupIndep condition holds for the submodules R · v_i, and each v_i has trivial torsion (torsionOf(R,M,v_i) = ⊥). Then the family v_i is linearly independent over R.
Русский
Пусть {v_i} — семейство в M; если выполняются условия iSupIndep для подмодулов R · v_i и для каждого i тorsionOf(R,M,v_i) = ⊥, то семейство v_i линейно независимо над R.
LaTeX
$$$\big( iSupIndep\, (i \mapsto R \cdot v_i) \big) \to \big( \forall i, \operatorname{torsionOf}(R,M,v_i) = \bot \big) \to \text{LinearIndependent}_R(v)$$$
Lean4
/-- See also `iSupIndep.linearIndependent` which provides the same conclusion
but requires the stronger hypothesis `NoZeroSMulDivisors R M`. -/
theorem linearIndependent' {ι R M : Type*} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M]
(hv : iSupIndep fun i => R ∙ v i) (h_ne_zero : ∀ i, Ideal.torsionOf R M (v i) = ⊥) : LinearIndependent R v :=
by
refine linearIndependent_iff_eq_zero_of_smul_mem_span.mpr fun i r hi => ?_
replace hv := iSupIndep_def.mp hv i
simp only [iSup_subtype', ← Submodule.span_range_eq_iSup (ι := Subtype _), disjoint_iff] at hv
have : r • v i ∈ (⊥ : Submodule R M) := by
rw [← hv, Submodule.mem_inf]
refine ⟨Submodule.mem_span_singleton.mpr ⟨r, rfl⟩, ?_⟩
convert hi
ext
simp
rw [← Submodule.mem_bot R, ← h_ne_zero i]
simpa using this
