coe_vanishingIdeal — Mathlib

English

The vanishing ideal can be expressed as a double infimum over elements of t, i.e., as an iterated intersection of x.asHomogeneousIdeal.

Русский

VanishingIdeal можно выразить как двойной инфимум над элементами t, то есть как перебор пересечений x.asHomogeneousIdeal.

LaTeX

$$$$ \\operatorname{vanishingIdeal}(t) = \\bigwedge_{x \\in t} \\bigwedge_{x' \\in t} x.asHomogeneousIdeal $$$$

Lean4

theorem coe_vanishingIdeal (t : Set (ProjectiveSpectrum 𝒜)) :
    (vanishingIdeal t : Set A) = {f | ∀ x : ProjectiveSpectrum 𝒜, x ∈ t → f ∈ x.asHomogeneousIdeal} :=
  by
  ext f
  rw [vanishingIdeal, SetLike.mem_coe, ← HomogeneousIdeal.mem_iff, HomogeneousIdeal.toIdeal_iInf, Submodule.mem_iInf]
  refine forall_congr' fun x => ?_
  rw [HomogeneousIdeal.toIdeal_iInf, Submodule.mem_iInf, HomogeneousIdeal.mem_iff]

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