gc — Mathlib · SciLib

English

ZeroLocus and vanishingIdeal form a Galois connection.

Русский

ZeroLocus и vanishingIdeal образуют связь Галуа.

LaTeX

$$$\\forall R,\\; GaloisConnection(\\\\operatorname{zeroLocus}, \\\\operatorname{vanishingIdeal})$$$

Lean4

/-- `zeroLocus` and `vanishingIdeal` form a Galois connection. -/
theorem gc :
    @GaloisConnection (Ideal R) (Set (PrimeSpectrum R))ᵒᵈ _ _ (fun I => zeroLocus I) fun t => vanishingIdeal t :=
  fun I t => subset_zeroLocus_iff_le_vanishingIdeal t I

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