of_isLocalizedModule_of_isRegular

English

If f is a localized map from M to Mₛ and S is a submonoid making localization possible, then any linear independence in M transfers to a linear independence in Mₛ after applying f to a basis.

Русский

Линейная независимость передаётся через локализацию на отображение f и базис модуля Mₛ.

LaTeX

$$LinearIndependent R v → LinearIndependent Rₛ (Function.comp (LinearMap.instFunLike.coe f) v)$$

Lean4

theorem of_isLocalizedModule_of_isRegular {ι : Type*} {v : ι → M} (hv : LinearIndependent R v)
    (h : ∀ s : S, IsRegular (s : R)) : LinearIndependent R (f ∘ v) :=
  hv.map_injOn _ <| by
    rw [← Finsupp.range_linearCombination]
    rintro _ ⟨_, r, rfl⟩ _ ⟨_, r', rfl⟩ eq
    congr; ext i
    have ⟨s, eq⟩ := IsLocalizedModule.exists_of_eq (S := S) eq
    simp_rw [Submonoid.smul_def, ← map_smul] at eq
    exact (h s).1 (DFunLike.congr_fun (hv eq) i)

Похожие утверждения