localizationLocalization — Mathlib

English

If A has an R-basis b, then the localized module A_s over R_s has a basis given by localizationLocalization(b).

Русский

Если у A есть база над R, то локализованный модуль A_s над R_s имеет базис, полученный локализацией localizationLocalization(b).

LaTeX

$$$\\text{localizationLocalization}(b) := b.ofIsLocalizedModule R_s S ( \\mathrm{IsScalarTower.toAlgHom} R A A_s ).toLinearMap$$$

Lean4

/-- If `A` has an `R`-basis, then localizing `A` at `S` has a basis over `R` localized at `S`.

A suitable instance for `[Algebra A Aₛ]` is `localizationAlgebra`.
-/
noncomputable def localizationLocalization {ι : Type*} (b : Basis ι R A) : Basis ι Rₛ Aₛ :=
  b.ofIsLocalizedModule Rₛ S (IsScalarTower.toAlgHom R A Aₛ).toLinearMap

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