gc_homogeneousIdeal — Mathlib

English

For a graded algebra 𝒜, HomogeneousIdeal and projective spectrum form a Galois connection: I ≤ vanishingIdeal(zeroLocus(𝒜 I)).

Русский

Для градуированной алгебры 𝒜 класс однородных идеалов и проективного спектра образуют галуа-связь: I ≤ vanishingIdeal(zeroLocus(𝒜 I)).

LaTeX

$$$$ \\forall I \\in \\mathrm{HomogeneousIdeal}(\\mathcal{A}), \\ I \\le \\operatorname{vanishingIdeal}(\\mathrm{zeroLocus}(\\mathcal{A}, I)). $$$$

Lean4

theorem gc_homogeneousIdeal :
    @GaloisConnection (HomogeneousIdeal 𝒜) (Set (ProjectiveSpectrum 𝒜))ᵒᵈ _ _ (fun I => zeroLocus 𝒜 I) fun t =>
      vanishingIdeal t :=
  fun I t => by
  simpa [show I.toIdeal ≤ (vanishingIdeal t).toIdeal ↔ I ≤ vanishingIdeal t from Iff.rfl] using
    subset_zeroLocus_iff_le_vanishingIdeal t I.toIdeal

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