English
A ring is Jacobson if and only if its prime spectrum is a Jacobson space.
Русский
Кольцо является Якобсоновым тогда и только тогда, когда спектр его п является пространством Якобсона.
LaTeX
$$$IsJacobsonRing R \\iff JacobsonSpace (PrimeSpectrum R)$$$
Lean4
theorem isJacobsonRing_iff_jacobsonSpace : IsJacobsonRing R ↔ JacobsonSpace (PrimeSpectrum R) :=
by
refine ⟨fun _ ↦ inferInstance, fun H ↦ ⟨fun I hI ↦ le_antisymm ?_ Ideal.le_jacobson⟩⟩
rw [← I.isRadical_jacobson.radical]
conv_rhs => rw [← hI.radical]
simp_rw [← vanishingIdeal_zeroLocus_eq_radical]
apply vanishingIdeal_anti_mono
rw [← H.1 (isClosed_zeroLocus I), (isClosed_zeroLocus _).closure_subset_iff]
rintro x ⟨hx : I ≤ x.asIdeal, hx'⟩
change jacobson I ≤ x.asIdeal
exact sInf_le ⟨hx, (isClosed_singleton_iff_isMaximal _).mp hx'⟩