English
Let R be a commutative semiring. The prime spectrum of R, endowed with the Zariski topology, is a compact topological space.
Русский
Пусть R — коммутативное полукольцо. Спектр простых идеалов R, снабжённый топологией Зари, является компактным топологическим пространством.
LaTeX
$$$\\operatorname{Spec}(R)$ is a compact topological space.$$
Lean4
/-- The prime spectrum of a commutative (semi)ring is a compact topological space. -/
instance compactSpace : CompactSpace (PrimeSpectrum R) :=
by
refine compactSpace_of_finite_subfamily_closed fun S S_closed S_empty ↦ ?_
choose I hI using fun i ↦ (isClosed_iff_zeroLocus_ideal (S i)).mp (S_closed i)
simp_rw [hI, ← zeroLocus_iSup, zeroLocus_empty_iff_eq_top, ← top_le_iff] at S_empty ⊢
exact Ideal.isCompactElement_top.exists_finset_of_le_iSup _ _ S_empty
