union_zeroLocus — Mathlib

English

A repeated formulation: the vanishing locus of the supremum of homogeneous ideals equals the intersection of their vanishing loci.

Русский

Повторная формулировка: нуль-множество верхней границы однородных идеалов равно пересечению нуль-множеств каждого.

LaTeX

$$$ \operatorname{zeroLocus}_{\mathcal{A}}(\operatorname{setLike}(I_i)_{i}^{\vee}) = \bigcap_i \operatorname{zeroLocus}_{\mathcal{A}}(I_i) $$$

Lean4

theorem union_zeroLocus (s s' : Set A) :
    zeroLocus 𝒜 s ∪ zeroLocus 𝒜 s' = zeroLocus 𝒜 (Ideal.span s ⊓ Ideal.span s' : Ideal A) :=
  by
  rw [zeroLocus_inf]
  simp

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