English
ZeroLocus and VanishingIdeal form a Galois connection between ideals of A and sets of points.
Русский
ZeroLocus и VanishingIdeal образуют галуа-связь между идеалами A и множествами точек.
LaTeX
$$$$ \\forall I \\subseteq A, \\forall t \\subseteq \\mathrm{ProjSpec}(\\mathcal{A}), \\quad \\mathrm{zeroLocus}(\\mathcal{A}, I) \\subseteq t \\iff I \\le \\operatorname{vanishingIdeal}(t). $$$$
Lean4
/-- `zeroLocus` and `vanishingIdeal` form a Galois connection. -/
theorem gc_set :
@GaloisConnection (Set A) (Set (ProjectiveSpectrum 𝒜))ᵒᵈ _ _ (fun s => zeroLocus 𝒜 s) fun t => vanishingIdeal t :=
by
have ideal_gc : GaloisConnection Ideal.span _ := (Submodule.gi A _).gc
simpa [zeroLocus_span, Function.comp_def] using GaloisConnection.compose ideal_gc (gc_ideal 𝒜)