zeroLocus_inf — Mathlib

English

For a graded algebra 𝒜 and a family of homogeneous ideals I_i, the vanishing locus of the supremum equals the intersection of the vanishing loci.

Русский

Для градуированной алгебры 𝒜 и семейства однородных идеалов I_i верхняя граница iSup даёт нуль-множество как пересечение.

LaTeX

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

Lean4

theorem zeroLocus_inf (I J : Ideal A) : zeroLocus 𝒜 ((I ⊓ J : Ideal A) : Set A) = zeroLocus 𝒜 I ∪ zeroLocus 𝒜 J :=
  Set.ext fun x => x.isPrime.inf_le

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