English
There exists a lift of a linearly independent family from S to M via a localized module structure when IsLocalizedModule S f holds.
Русский
Существуют подъемы линейной независимости через локализацию модуля.
LaTeX
$$IsLocalizedModule.linearIndependent_lift$$
Lean4
theorem linearIndependent_lift {ι} {v : ι → Mₛ} (hf : LinearIndependent R v) : ∃ w : ι → M, LinearIndependent R w :=
by
cases isEmpty_or_nonempty ι
· exact ⟨isEmptyElim, linearIndependent_empty_type⟩
have inj := hf.smul_left_injective (Classical.arbitrary ι)
choose sec hsec using surj S f
use fun i ↦ (sec (v i)).1
rw [linearIndependent_iff'ₛ] at hf ⊢
intro t g g' eq i hit
refine
(isRegular_of_smul_left_injective f inj (sec (v i)).2).2 <|
hf t (fun i ↦ _ * (sec (v i)).2) (fun i ↦ _ * (sec (v i)).2) ?_ i hit
simp_rw [mul_smul, ← Submonoid.smul_def, hsec, ← map_smul, ← map_sum, eq]
