gc_set — Mathlib

English

The pair of Galois connections between sets and the prime spectrum holds: gc_set.

Русский

Существует связующая пара Галуа между множествами и спектром простых точек.

LaTeX

$$$\\forall R,\\; GaloisConnection( zeroLocus, vanishingIdeal )$$$

Lean4

/-- `zeroLocus` and `vanishingIdeal` form a Galois connection. -/
theorem gc_set :
    @GaloisConnection (Set R) (Set (PrimeSpectrum R))ᵒᵈ _ _ (fun s => zeroLocus s) fun t => vanishingIdeal t :=
  by
  have ideal_gc : GaloisConnection Ideal.span _ := (Submodule.gi R R).gc
  simpa [zeroLocus_span, Function.comp_def] using ideal_gc.compose (gc R)

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