lift_algebraMap_eq_algebraMap — Mathlib

English

Evaluating the algebraMap after localization equals evaluating the map constructed via map_submonoid at the same argument.

Русский

При выполнении algebraMap после локализации получаем то же самое, что и у отображения, сконструированного через map_submonoid.

LaTeX

$$$\text{algebraMap } R_m S_m x = \ map S_m (algebraMap R S) (\text{show } _ \leq (\text{Algebra.algebraMapSubmonoid } S M).comap _ from M.le_comap_map)\; x$$$

Lean4

theorem lift_algebraMap_eq_algebraMap :
    IsLocalization.lift (M := M) (IsLocalization.map_units_map_submonoid S Sₘ) = algebraMap Rₘ Sₘ :=
  IsLocalization.lift_unique _ fun _ => (IsScalarTower.algebraMap_apply _ _ _ _).symm

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