English
Let f be surjective and ker f ≤ I. Then map f I.radical = (map f I).radical.
Русский
Пусть f сюръективно и ker f ≤ I. Тогда map f I.radical = (map f I).radical.
LaTeX
$$$$ \\operatorname{map} f I_{\\mathrm{radical}} = (\\operatorname{map} f I)_{\\mathrm{radical}}. $$$$
Lean4
theorem map_radical_of_surjective {f : R →+* S} (hf : Function.Surjective f) {I : Ideal R} (h : RingHom.ker f ≤ I) :
map f I.radical = (map f I).radical :=
by
rw [radical_eq_sInf, radical_eq_sInf]
have : ∀ J ∈ {J : Ideal R | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J := fun J hJ => h.trans hJ.left
convert map_sInf hf this
refine funext fun j => propext ⟨?_, ?_⟩
· rintro ⟨hj, hj'⟩
haveI : j.IsPrime := hj'
exact ⟨comap f j, ⟨⟨map_le_iff_le_comap.1 hj, comap_isPrime f j⟩, map_comap_of_surjective f hf j⟩⟩
· rintro ⟨J, ⟨hJ, hJ'⟩⟩
haveI : J.IsPrime := hJ.right
exact ⟨hJ' ▸ map_mono hJ.left, hJ' ▸ map_isPrime_of_surjective hf (le_trans h hJ.left)⟩
