mem_supportSet_iff_of_mem — Mathlib

English

For any x in an affine open U, x is in the support of I if and only if x lies in the zero locus of I.U on U.

Русский

Для любого x в аффинном открытом участке U верно: x принадлежит поддержке I тогда и только тогда, когда x лежит в нулевой локусе I на U.

LaTeX

$$$x \in I.support \iff x \in X.zeroLocus(U := U.1)(I.ideal U)$$$

Lean4

theorem mem_supportSet_iff_of_mem {I : IdealSheafData X} {x} {U : X.affineOpens} (hxU : x ∈ U.1) :
    x ∈ I.supportSet ↔ x ∈ X.zeroLocus (U := U.1) (I.ideal U) :=
  ⟨I.supportSet_eq_iInter_zeroLocus ▸ fun h ↦ Set.iInter_subset _ U h, fun h ↦
    I.zeroLocus_inter_subset_supportSet U ⟨h, hxU⟩⟩

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