localizationLocalization_repr_algebraMap

English

For x ∈ A and i ∈ ι, the i-th coordinate of the representation of algebraMap_A^A_s(x) in the localized basis equals algebraMap_R^R_s applied to the i-th coordinate of x with respect to b.

Русский

Для x ∈ A и i ∈ ι i‑й координате представления образа algebraMap_A^A_s(x) в локализованном базисе соответствует algebraMap_R^R_s применённому к i‑й координате x по базису b.

LaTeX

$$$\\big( (b.localizationLocalization R_s S A_s).repr (\\mathrm{algebraMap}_{A}^{A_s} x) \\big) i = \\mathrm{algebraMap}_{R}^{R_s} (b.repr x i)$$$

Lean4

@[simp]
theorem localizationLocalization_repr_algebraMap {ι : Type*} (b : Basis ι R A) (x i) :
    (b.localizationLocalization Rₛ S Aₛ).repr (algebraMap A Aₛ x) i = algebraMap R Rₛ (b.repr x i) :=
  b.ofIsLocalizedModule_repr_apply Rₛ S _ _ i

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