LinearIndependent.of_isLocalizedModule

theorem LinearIndependent.of_isLocalizedModule : ∀ {R : Type u_1} (Rₛ : Type u_2) [inst : CommSemiring R] (S : Submonoid R) [inst_1 : CommSemiring Rₛ] [inst_2 : Algebra R Rₛ] [hT : IsLocalization S Rₛ] {M : Type u_3} {M' : Type u_4} [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : AddCommMonoid M'] [inst_6 : Module R M'] [inst_7 : Module Rₛ M'] [inst_8 : IsScalarTower R Rₛ M'] (f : M →ₗ[R] M') [inst_9 : IsLocalizedModule S f] {ι : Type u_5} {v : ι → M}, LinearIndependent R v → LinearIndependent Rₛ (⇑f ∘ v)

The theorem `LinearIndependent.of_isLocalizedModule` asserts that if a family of vectors `v` is linearly independent over a commutative semiring `R`, then the image of this family under a linear map `f` is linearly independent over a localization `Rₛ` of `R`, assuming the module `M` on which the vectors act is localized with respect to a submonoid `S` of `R`. This holds under the assumptions that `Rₛ` is an algebra over `R`, that `M'` (the co-domain of `f`) is a module over both `R` and `Rₛ`, and that `Rₛ` acts on `M'` in a way that is compatible with the action of `R` (that is, there is a scalar tower).

More concisely: If a family of vectors is linearly independent over a commutative semiring, then their images under a linear map are linearly independent over the localization of the semiring, provided the module acts and is localized with respect to a submonoid, and the localization is an algebra over the semiring and acts compatibly on the co-domain of the map.