English
If f is surjective and I is a prime ideal with ker f ≤ I, then map f I is a prime ideal.
Русский
Если f сюръективно, и I — простой идеал с ker f ≤ I, тогда map f I — простой идеал.
LaTeX
$$$$ \\text{If } f: R \\to S \\text{ is surjective and } I \\triangleleft R \\text{ with } \\ker f \\le I, \\text{ then } \\operatorname{map} f I \\triangleleft S \\text{ is prime}.$$$$
Lean4
theorem map_isPrime_of_surjective {f : F} (hf : Function.Surjective f) {I : Ideal R} [H : IsPrime I]
(hk : RingHom.ker f ≤ I) : IsPrime (map f I) :=
by
refine ⟨fun h => H.ne_top (eq_top_iff.2 ?_), fun {x y} => ?_⟩
· replace h := congr_arg (comap f) h
rw [comap_map_of_surjective _ hf, comap_top] at h
exact h ▸ sup_le (le_of_eq rfl) hk
· refine fun hxy => (hf x).recOn fun a ha => (hf y).recOn fun b hb => ?_
rw [← ha, ← hb, ← map_mul f, mem_map_iff_of_surjective _ hf] at hxy
rcases hxy with ⟨c, hc, hc'⟩
rw [← sub_eq_zero, ← map_sub] at hc'
have : a * b ∈ I := by
convert I.sub_mem hc (hk (hc' : c - a * b ∈ RingHom.ker f)) using 1
abel
exact (H.mem_or_mem this).imp (fun h => ha ▸ mem_map_of_mem f h) fun h => hb ▸ mem_map_of_mem f h
