map_of_surjective_of_ker_le — Mathlib

English

Let f be surjective and m a maximal ideal of R with ker f ≤ m. Then the image map f m is a maximal ideal of S.

Русский

Пусть f сюръективно, m — максимальный идеал R и ker f ≤ m. Тогда m.map f — максимальный идеал S.

LaTeX

$$$$ (m.map f).IsMaximal \\quad \\text{whenever } f \\text{ is surjective and } \\ker f \\le m.$$$$

Lean4

theorem map_of_surjective_of_ker_le {f : F} (hf : Function.Surjective f) {m : Ideal R} [m.IsMaximal]
    (hk : RingHom.ker f ≤ m) : (m.map f).IsMaximal :=
  by
  refine m.map_eq_top_or_isMaximal_of_surjective f hf ‹_› |>.resolve_left fun h => ?_
  apply congr_arg (comap f)at h
  rw [comap_map_of_surjective _ hf, comap_top, ← RingHom.ker_eq_comap_bot, sup_of_le_left hk] at h
  exact IsMaximal.ne_top ‹_› h

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