English
If R is Jacobson and there exists a surjective ring hom f: R → S, then S is Jacobson.
Русский
Если R является кольцом Якобсона и существует сюръективный гомоморфизм f: R → S, то S также является кольцом Якобсона.
LaTeX
$$$\\exists f: R \\to S \\, (\\text{surjective}) \\Rightarrow \\operatorname{IsJacobsonRing}(S).$$$
Lean4
/-- A ring is a Jacobson ring if and only if for all prime ideals `P`,
the Jacobson radical of `P` is equal to `P`. -/
theorem isJacobsonRing_iff_prime_eq : IsJacobsonRing R ↔ ∀ P : Ideal R, IsPrime P → P.jacobson = P :=
by
refine isJacobsonRing_iff.trans ⟨fun h I hI => h I hI.isRadical, ?_⟩
refine fun h I hI ↦ le_antisymm (fun x hx ↦ ?_) (fun x hx ↦ mem_sInf.mpr fun _ hJ ↦ hJ.left hx)
rw [← hI.radical, radical_eq_sInf I, mem_sInf]
intro P hP
rw [Set.mem_setOf_eq] at hP
rw [jacobson, mem_sInf] at hx
rw [← h P hP.right, jacobson, mem_sInf]
exact fun J hJ => hx ⟨le_trans hP.left hJ.left, hJ.right⟩
