English
Let R be a commutative ring. The image of the map toPrimeSpectrum is exactly the set of prime spectrum points that are closed as singletons in the Zariski topology.
Русский
Пусть R — коммутативное кольцо. Образ отображения toPrimeSpectrum равен множеству точек спектра простых, которые являются замкнутыми одиночками в зариcковской топологии.
LaTeX
$$$\\\\operatorname{range}(\\\\operatorname{toPrimeSpectrum}) = \\\\{ x \\\\in \\\\operatorname{PrimeSpectrum}(R) \\\\mid \\\\operatorname{IsClosed}(\\\\{x\\\\}) \\\}$$$
Lean4
theorem toPrimeSpectrum_range : Set.range (@toPrimeSpectrum R _) = {x | IsClosed ({ x } : Set <| PrimeSpectrum R)} :=
by
simp only [isClosed_singleton_iff_isMaximal]
ext ⟨x, _⟩
exact ⟨fun ⟨y, hy⟩ => hy ▸ y.isMaximal, fun hx => ⟨⟨x, hx⟩, rfl⟩⟩