localizationLocalization_apply — Mathlib

English

For a basis b and index i, the i-th coordinate of the localized basis vector equals algebraMap A A_s applied to the original i-th coordinate.

Русский

Для базиса b и индекса i i‑й координате локализованного базиса сопоставляется алгебраическое отображение A → A_s, применённое к i‑й координате исходного базиса.

LaTeX

$$$\\big(b.localizationLocalization R_s S A_s\\big)\\,i = \\ algebraMap A A_s (b\\,i) $$$

Lean4

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

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