gc_ideal — Mathlib

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

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