English
A subset s of the prime spectrum is compact and open if and only if it can be written as the complement of the zero locus of some finite set of ring elements; equivalently, there exists a finite set t ⊆ R such that s = (zeroLocus t)ᶜ.
Русский
Подмножество s спектра простых идеалов компактно и открыто тогда и только тогда, когда его можно записать как дополнение к нуль-множеству некоторого конечного набора элементов кольца; эквивалентно, существует конечный набор t ⊆ R such that s = (zeroLocus t)ᶜ.
LaTeX
$$$$ \text{IsCompact}(s) \wedge \text{IsOpen}(s) \iff \exists t \in \operatorname{Finset} R, (\operatorname{zeroLocus} t)^{c} = s. $$$$
Lean4
theorem isCompact_isOpen_iff {s : Set (PrimeSpectrum R)} :
IsCompact s ∧ IsOpen s ↔ ∃ t : Finset R, (zeroLocus t)ᶜ = s :=
by
rw [isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis _ isTopologicalBasis_basic_opens isCompact_basicOpen]
simp only [basicOpen_eq_zeroLocus_compl, ← Set.compl_iInter₂, ← zeroLocus_iUnion₂, Set.biUnion_of_singleton]
exact ⟨fun ⟨s, hs, e⟩ ↦ ⟨hs.toFinset, by simpa using e.symm⟩, fun ⟨s, e⟩ ↦ ⟨s, s.finite_toSet, by simpa using e.symm⟩⟩
