subset_zeroLocus_iff_subset_vanishingIdeal

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

theorem subset_zeroLocus_iff_subset_vanishingIdeal (t : Set (ProjectiveSpectrum 𝒜)) (s : Set A) :
    t ⊆ zeroLocus 𝒜 s ↔ s ⊆ vanishingIdeal t :=
  (gc_set _) s t

Похожие утверждения