mk'_eq_algebraMap_mk'_of_submonoid_le

English

For M ≤ N with IsLocalization M S and IsLocalization N T, and x ∈ R with y ∈ {a ∈ R | a ∈ M}, mk' T x ⟨y, proof⟩ equals algebraMap S T (mk' S x y).

Русский

Для M ≤ N и локализаций выполняется равенство mk' T x ⟨y,⋯⟩ = algebraMap S T (mk' S x y).

LaTeX

$$mk' T x ⟨y, h⟩ = algebraMap S T (mk' S x y)$$

Lean4

theorem mk'_eq_algebraMap_mk'_of_submonoid_le {M N : Submonoid R} (h : M ≤ N) [IsLocalization M S] [IsLocalization N T]
    [Algebra S T] [IsScalarTower R S T] (x : R) (y : { a : R // a ∈ M }) :
    mk' T x ⟨y.1, h y.2⟩ = algebraMap S T (mk' S x y) :=
  mk'_eq_iff_eq_mul.mpr (by simp only [IsScalarTower.algebraMap_apply R S T, ← map_mul, mk'_spec])

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