toKerIsLocalization_apply — Mathlib

English

Evaluating the canonical localization map on an element of ker g yields its image under algebraMap to the ambient localization.

Русский

Применение канонического отображения локализации к элементу из ядра $g$ даёт изображение через алгебраическое отображение в локализации.

LaTeX

$$$\\big( \\mathrm{toKerIsLocalization}(S, Q, g, hy)(x) \\big).\\text{val} = \\mathrm{algebraMap}_{R,S}(x) \\qquad (x \\in \\ker g)$$$

Lean4

@[simp]
theorem toKerIsLocalization_apply (hy : M ≤ Submonoid.comap g T) (r : RingHom.ker g) :
    (RingHom.toKerIsLocalization S Q g hy r).val = algebraMap R S r :=
  rfl

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