ker_map — Mathlib

English

The kernel of the localized map is the extension of the kernel of the original map along the base change.

Русский

Ядро локализованного отображения равно расширению ядра исходного отображения вдоль базового перехода.

LaTeX

$$$\\ker(\\mathrm{IsLocalization.map}\\, Q\\, g\\, hy) = \\mathrm{Ideal.map}(\\alpha)\\big(\\ker g\\big),$$$

Lean4

theorem ker_map (hT : Submonoid.map g M = T) :
    RingHom.ker (IsLocalization.map Q g (hT.symm ▸ M.le_comap_map) : S →+* Q) = (RingHom.ker g).map (algebraMap R S) :=
  by
  ext x
  obtain ⟨x, s, rfl⟩ := IsLocalization.mk'_surjective M x
  simp [RingHom.mem_ker, IsLocalization.map_mk', IsLocalization.mk'_eq_zero_iff,
    IsLocalization.mk'_mem_map_algebraMap_iff, ← hT]

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