English
If R is Jacobson, then its prime spectrum is a Jacobson space; closed sets can be determined via maximal ideals.
Русский
Если R является кольцом Якобсона, спектр его пprime — пространство Якобсона; замкнутые множества описываются максимальными идеалами.
LaTeX
$$IsJacobsonRing R \\Rightarrow JacobsonSpace (PrimeSpectrum R)$$
Lean4
instance [IsJacobsonRing R] : JacobsonSpace (PrimeSpectrum R) :=
by
rw [jacobsonSpace_iff_locallyClosed]
rintro S hS ⟨U, Z, hU, hZ, rfl⟩
simp only [← isClosed_compl_iff, isClosed_iff_zeroLocus_ideal, @compl_eq_comm _ U] at hU hZ
obtain ⟨⟨I, rfl⟩, ⟨J, rfl⟩⟩ := And.intro hU hZ
simp only [Set.nonempty_iff_ne_empty, ne_eq, Set.inter_assoc, ← Set.disjoint_iff_inter_eq_empty,
Set.disjoint_compl_left_iff_subset, zeroLocus_subset_zeroLocus_iff, Ideal.radical_eq_jacobson, Ideal.jacobson,
le_sInf_iff] at hS ⊢
contrapose! hS
rintro x ⟨hJx, hx⟩
exact @hS ⟨x, hx.isPrime⟩ ⟨hJx, (isClosed_singleton_iff_isMaximal _).mpr hx⟩
