English
If there exists a surjective ring hom f: R → S and R is Jacobson, then S is Jacobson.
Русский
Если существует сюръективный гомоморфизм f: R → S и R — кольцо Якобсона, то S также является кольцом Якобсона.
LaTeX
$$$\\exists f: R \\to S, \\text{Surjective} \\Rightarrow IsJacobsonRing(S).$$$
Lean4
theorem isJacobsonRing_of_surjective [H : IsJacobsonRing R] :
(∃ f : R →+* S, Function.Surjective ↑f) → IsJacobsonRing S :=
by
rintro ⟨f, hf⟩
rw [isJacobsonRing_iff_sInf_maximal]
intro p hp
use map f '' {J : Ideal R | comap f p ≤ J ∧ J.IsMaximal}
use fun j ⟨J, hJ, hmap⟩ => hmap ▸ (map_eq_top_or_isMaximal_of_surjective f hf hJ.right).symm
have : p = map f (comap f p).jacobson :=
(IsJacobsonRing.out' _ <| hp.isRadical.comap f).symm ▸ (map_comap_of_surjective f hf p).symm
exact this.trans (map_sInf hf fun J ⟨hJ, _⟩ => le_trans (Ideal.ker_le_comap f) hJ)
