English
If v is a linearly independent family in M over R and we localize, then its image under localization is linearly independent over Rₛ. In particular, a basis lifts through localization to a localized basis.
Русский
Если набор векторных баз в Module M над R линейно независим, то его локализованный образ линейно независим над Rₛ; база локализуется.
LaTeX
$$LinearIndependent R v → LinearIndependent Rₛ (f ∘ v)$$
Lean4
theorem of_isLocalizedModule {ι : Type*} {v : ι → M} (hv : LinearIndependent R v) : LinearIndependent Rₛ (f ∘ v) :=
by
rw [linearIndependent_iff'ₛ] at hv ⊢
intro t g₁ g₂ eq i hi
choose! a fg hfg using IsLocalization.exist_integer_multiples S (t.disjSum t) (Sum.elim g₁ g₂)
simp_rw [Sum.forall, Finset.inl_mem_disjSum, Sum.elim_inl, Finset.inr_mem_disjSum, Sum.elim_inr,
Subtype.forall'] at hfg
apply_fun ((a : R) • ·) at eq
simp_rw [← t.sum_coe_sort, Finset.smul_sum, ← smul_assoc, ← hfg, algebraMap_smul, Function.comp_def, ← map_smul, ←
map_sum, t.sum_coe_sort (f := fun x ↦ fg (Sum.inl x) • v x),
t.sum_coe_sort (f := fun x ↦ fg (Sum.inr x) • v x)] at eq
have ⟨s, eq⟩ := IsLocalizedModule.exists_of_eq (S := S) eq
simp_rw [Finset.smul_sum, Submonoid.smul_def, smul_smul] at eq
have := congr(algebraMap R Rₛ $(hv t _ _ eq i hi))
simpa only [map_mul, (IsLocalization.map_units Rₛ s).mul_right_inj, hfg.1 ⟨i, hi⟩, hfg.2 ⟨i, hi⟩, Algebra.smul_def,
(IsLocalization.map_units Rₛ a).mul_right_inj] using this
