zeroLocus_iSup_homogeneousIdeal — 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_iSup_homogeneousIdeal {γ : Sort*} (I : γ → HomogeneousIdeal 𝒜) :
    zeroLocus _ ((⨆ i, I i : HomogeneousIdeal 𝒜) : Set A) = ⋂ i, zeroLocus 𝒜 (I i) :=
  (gc_homogeneousIdeal 𝒜).l_iSup

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