zeroLocus_span — Mathlib

English

Taking the span of a set s does not change its zero locus in ProjectiveSpectrum 𝒜.

Русский

Пространство натянутого множества s не изменяет его нулевую зону в ProjectiveSpectrum 𝒜.

LaTeX

$$$$ \\mathrm{zeroLocus}(\\mathcal{A}, \\operatorname{span}(s)) = \\mathrm{zeroLocus}(\\mathcal{A}, s) $$$$

Lean4

@[simp]
theorem zeroLocus_span (s : Set A) : zeroLocus 𝒜 (Ideal.span s) = zeroLocus 𝒜 s :=
  by
  ext x
  exact (Submodule.gi _ _).gc s x.asHomogeneousIdeal.toIdeal

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