mem_compl_zeroLocus_iff_notMem — Mathlib

English

A point I lies outside the zero locus of {f} if and only if f is not in the homogeneous ideal of I.

Русский

Точка I лежит вне нуль-множества {f} тогда и только тогда, когда f не входит в однородный идеал I.

LaTeX

$$$ I \in (\operatorname{zeroLocus}_{\mathcal{A}}(\{f\}) )^{c} \iff f \notin I.asHomogeneousIdeal $$$

Lean4

theorem mem_compl_zeroLocus_iff_notMem {f : A} {I : ProjectiveSpectrum 𝒜} :
    I ∈ (zeroLocus 𝒜 { f } : Set (ProjectiveSpectrum 𝒜))ᶜ ↔ f ∉ I.asHomogeneousIdeal := by
  rw [Set.mem_compl_iff, mem_zeroLocus, Set.singleton_subset_iff]; rfl

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