localizationLocalization_span — Mathlib

English

Let b be a basis of A over R. Then the span of the localized basis images equals the range of IsScalarTower.toAlgHom R A A_s.

Русский

Пусть b — база A над R. Тогда линейная оболочка образов локализованной базы равна образованию IsScalarTower.toAlgHom R A A_s.

LaTeX

$$$\\operatorname{span}_R\\big( \\operatorname{Set.range} ( b.localizationLocalization R_s S A_s ) \\big) = \\operatorname{LinearMap.range}( \\mathrm{IsScalarTower.toAlgHom} \\; R \\; A \\; A_s )$$$

Lean4

theorem localizationLocalization_span {ι : Type*} (b : Basis ι R A) :
    Submodule.span R (Set.range (b.localizationLocalization Rₛ S Aₛ)) =
      LinearMap.range (IsScalarTower.toAlgHom R A Aₛ) :=
  b.ofIsLocalizedModule_span Rₛ S _

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