span_eq_top_localization_localization

English

If the R-span of a set v generates the whole space (span_R v = ⊤), then the R_s-span of its image under the algebra map to A_s also generates the whole A_s (span_Rs (algebraMap A A_s '' v) = ⊤).

Русский

Если множество v порождает все пространство над R (span_R v = ⊤), то образ его под алгебраическим отображением в A_s порождает всё пространство над R_s (span_Rs (алгебраMap A A_s '' v) = ⊤).

LaTeX

$$$\\operatorname{span}_R v = \\top \\Rightarrow \\operatorname{span}_{R_s}(\\operatorname{algebraMap}_{A}^{A_s}'' v) = \\top$$$

Lean4

theorem span_eq_top_localization_localization {v : Set A} (hv : span R v = ⊤) : span Rₛ (algebraMap A Aₛ '' v) = ⊤ :=
  span_eq_top_of_isLocalizedModule Rₛ S (IsScalarTower.toAlgHom R A Aₛ).toLinearMap hv

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