zeroLocus_iSup_ideal — Mathlib

English

For any indexer γ and family of ideals I_i, the vanishing locus of the supremum of the family equals the intersection of the vanishing loci.

Русский

Для семейства идеалов I_i, нуль-множество над верхушкой iSup равно пересечению нуль-множеств каждого.

LaTeX

$$$ \operatorname{zeroLocus}_{\mathcal{A}}(\bigvee_{i} I_i) = \bigcap_{i} \operatorname{zeroLocus}_{\mathcal{A}}(I_i) $$$

Lean4

theorem zeroLocus_iSup_ideal {γ : Sort*} (I : γ → Ideal A) :
    zeroLocus _ ((⨆ i, I i : Ideal A) : Set A) = ⋂ i, zeroLocus 𝒜 (I i) :=
  (gc_ideal 𝒜).l_iSup

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