English
The isomorphism between compact open sets inside Spec(R) and finite-generated zero loci expresses that the spectrum's compact-open subsets are exactly the complements of finite unions of basic zeros. More precisely, IsCompact s ∧ IsOpen s holds iff there exists a finite set t with s = (zeroLocus t)ᶜ.
Русский
Связанные компактно-открытые множества спектра удовлетворяют: существует конечный набор t, такой что 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 basicOpen_eq_zeroLocus_of_mul_add (e f : R) (mul : e * f = 0) (add : e + f = 1) :
basicOpen e = zeroLocus { f } := by
ext p
suffices e ∉ p.asIdeal ↔ f ∈ p.asIdeal by simpa
refine ⟨(p.2.mem_or_mem_of_mul_eq_zero mul).resolve_left, fun h₁ h₂ ↦ p.2.1 ?_⟩
rw [Ideal.eq_top_iff_one, ← add]
exact add_mem h₂ h₁
