localization_localization — Mathlib

English

If a family v: ι → A is linearly independent over R, then its image under the localization map to A_s is linearly independent over R_s.

Русский

Если семейство v: ι → A линейно независимо над R, то образ этого семейства в локализации A_s по образованию алгебраической карты A → A_s линейно независимо над R_s.

LaTeX

$$$\\operatorname{LinearIndependent}_R v \\Rightarrow \\operatorname{LinearIndependent}_{R_s}(\\alpha \\circ v),\\quad \\alpha = \\mathrm{algebraMap}_{A}^{A_s}$$$

Lean4

theorem localization_localization {ι : Type*} {v : ι → A} (hv : LinearIndependent R v) :
    LinearIndependent Rₛ (algebraMap A Aₛ ∘ v) :=
  hv.of_isLocalizedModule Rₛ S (IsScalarTower.toAlgHom R A Aₛ).toLinearMap

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