English
The Zariski topology on the projective spectrum 𝒜 is defined by declaring the closed sets to be precisely the zero loci of subsets of A.
Русский
Zariski топология на проектном спектре 𝒜 определяется как множество нуль-множества точек, соответствующее подмножествам A.
LaTeX
$$$ \text{ClosedSets}(\mathrm{Proj}_{\mathcal{A}}) = \{ \operatorname{zeroLocus}_{\mathcal{A}}(S) : S \subseteq A \}$$$
Lean4
/-- The Zariski topology on the prime spectrum of a commutative 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 (ProjectiveSpectrum 𝒜) :=
TopologicalSpace.ofClosed (Set.range (ProjectiveSpectrum.zeroLocus 𝒜)) ⟨Set.univ, by simp⟩
(by
intro Zs h
rw [Set.sInter_eq_iInter]
let f : Zs → Set _ := fun i => Classical.choose (h i.2)
have H : (Set.iInter fun i ↦ zeroLocus 𝒜 (f i)) ∈ Set.range (zeroLocus 𝒜) := ⟨_, zeroLocus_iUnion 𝒜 _⟩
convert H using 2
funext i
exact (Classical.choose_spec (h i.2)).symm)
(by
rintro _ ⟨s, rfl⟩ _ ⟨t, rfl⟩
exact ⟨_, (union_zeroLocus 𝒜 s t).symm⟩)
