gc_set — Mathlib

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 𝒜)

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