English
In a Jacobson ring, every nonempty open set contains a closed singleton: there exists x in the set such that {x} is closed.
Русский
В кольце Якобсона любой непустой открытый множество содержит замкнутый синглтон: существует x в множестве, такое что {x} замкнуто.
LaTeX
$$$\\exists x \\in S\\; (\\{x\\} \\text{ is closed})$ for IsJacobsonRing$$
Lean4
theorem exists_isClosed_singleton_of_isJacobsonRing [IsJacobsonRing R] (s : (Set (PrimeSpectrum R))) (hs : IsOpen s)
(hs' : s.Nonempty) : ∃ x ∈ s, IsClosed { x } :=
by
simp_rw [isClosed_singleton_iff_isMaximal]
obtain ⟨I, hI'⟩ := (isClosed_iff_zeroLocus_ideal _).mp hs.isClosed_compl
simp_rw [← @Set.notMem_compl_iff _ s, hI', mem_zeroLocus]
have := hs'.ne_empty
contrapose! this
simp_rw [not_imp_not] at this
rw [← Set.compl_univ, eq_compl_comm, hI', eq_comm, ← zeroLocus_bot, zeroLocus_eq_iff, Ideal.radical_eq_jacobson,
Ideal.radical_eq_jacobson]
refine le_antisymm (le_sInf ?_) (Ideal.jacobson_mono bot_le)
rintro x ⟨-, hx⟩
exact sInf_le ⟨this ⟨x, hx.isPrime⟩ hx, hx⟩
