English
ZeroLocus and VanishingIdeal form a Galois connection between sets of A and sets of points in ProjectiveSpectrum 𝒜.
Русский
ZeroLocus и VanishingIdeal образуют галуа-связь между множествами в A и точками в ProjectiveSpectrum 𝒜.
LaTeX
$$$$ \\forall s,t \\ \mathrm{zeroLocus}(\\mathcal{A}, s) \\subseteq t \\iff s \\subseteq \\operatorname{vanishingIdeal}(t). $$$$
Lean4
/-- `zeroLocus` and `vanishingIdeal` form a Galois connection. -/
theorem gc_ideal :
@GaloisConnection (Ideal A) (Set (ProjectiveSpectrum 𝒜))ᵒᵈ _ _ (fun I => zeroLocus 𝒜 I) fun t =>
(vanishingIdeal t).toIdeal :=
fun I t => subset_zeroLocus_iff_le_vanishingIdeal t I