English
The Zariski topology on the prime spectrum of a commutative ring is defined by its closed sets, which are exactly the zero loci of subsets of the ring.
Русский
Zariski топология на спектре примар коммутативного кольца задаётся как замкнутые множества, являющиеся нулевыми локациями некоторого подмножества кольца.
LaTeX
$$$\\{Z : Z \\subseteq \\operatorname{PrimeSpectrum}(R) \\mid Z = \\operatorname{ZeroLocus}(S) \\text{ for some } S \\subseteq R\\}$ является множеством замкнутых множеств$$
Lean4
/-- The Zariski topology on the prime spectrum of a commutative (semi)ring is defined
via the closed sets of the topology: they are exactly those sets that are the zero locus
of a subset of the ring. -/
instance zariskiTopology : TopologicalSpace (PrimeSpectrum R) :=
TopologicalSpace.ofClosed (Set.range PrimeSpectrum.zeroLocus) ⟨Set.univ, by simp⟩
(by
intro Zs h
rw [Set.sInter_eq_iInter]
choose f hf using fun i : Zs => h i.prop
simp only [← hf]
exact ⟨_, zeroLocus_iUnion _⟩)
(by
rintro _ ⟨s, rfl⟩ _ ⟨t, rfl⟩
exact ⟨_, (union_zeroLocus s t).symm⟩)
