gc — Mathlib · SciLib

English

The maps Z ↦ vanishingIdeal(Z) and I ↦ I.support form a Galois connection between closed subsets of X and ideal data on X; equivalently, for all I and Z, Z ≤ I.support iff I ≤ vanishingIdeal(Z).

Русский

Отображения Z ↦ vanishingIdeal(Z) и I ↦ I.support образуют Галуа-соотношение между множествами закрытых подмножеств X и данными идеалов. Для любых I и Z верно: Z ≤ Supp(I) ⇔ I ≤ vanishingIdeal(Z).

LaTeX

$$$Z \\subseteq \\mathrm{Supp}(I) \\iff I \\subseteq \\operatorname{vanishingIdeal}(Z)$$$

Lean4

/-- `support` and `vanishingIdeal` forms a Galois connection.
This is the global version of `PrimeSpectrum.gc`. -/
theorem gc : @GaloisConnection X.IdealSheafData (Closeds X)ᵒᵈ _ _ (support ·) (vanishingIdeal ·) := fun _ _ ↦
  le_support_iff_le_vanishingIdeal

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