algebraMap_mk' — Mathlib

English

For all compatible towers, the lift of an algebra map equals the algebra map on the appropriate level.

Русский

Для всех совместимых башен тензорный лифт отображения совпадает с алгебраическим отображением на соответствующем уровне.

LaTeX

$$$\operatorname{IsLocalization.lift}(M := M)(\text{IsLocalization.map_units_map_submonoid } S S_m) = \text{algebraMap} R_m S_m$$$

Lean4

theorem algebraMap_mk' (x : R) (y : M) :
    algebraMap Rₘ Sₘ (IsLocalization.mk' Rₘ x y) =
      IsLocalization.mk' Sₘ (algebraMap R S x) ⟨algebraMap R S y, Algebra.mem_algebraMapSubmonoid_of_mem y⟩ :=
  by
  rw [IsLocalization.eq_mk'_iff_mul_eq, Subtype.coe_mk, ← IsScalarTower.algebraMap_apply, ←
    IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R Rₘ Sₘ, IsScalarTower.algebraMap_apply R Rₘ Sₘ, ←
    map_mul, mul_comm, IsLocalization.mul_mk'_eq_mk'_of_mul]
  exact congr_arg (algebraMap Rₘ Sₘ) (IsLocalization.mk'_mul_cancel_left x y)

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