mem_vanishingIdeal — Mathlib

English

For a set t and an ideal I, t is contained in zeroLocus 𝒜 I iff I is below vanishingIdeal t (as an ideal).

Русский

Для множества t и идеала I выполняется: t ⊆ zeroLocus 𝒜 I эквивалентно I ≤ vanishingIdeal t.

LaTeX

$$$$ t \\subseteq \\mathrm{zeroLocus}(\\mathcal{A}, I) \\iff I \\le (\\operatorname{vanishingIdeal}(t)).toIdeal $$$$

Lean4

theorem mem_vanishingIdeal (t : Set (ProjectiveSpectrum 𝒜)) (f : A) :
    f ∈ vanishingIdeal t ↔ ∀ x : ProjectiveSpectrum 𝒜, x ∈ t → f ∈ x.asHomogeneousIdeal := by
  rw [← SetLike.mem_coe, coe_vanishingIdeal, Set.mem_setOf_eq]

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