zeroLocus_iInf_of_nonempty — Mathlib

English

If the index set is finite and nonempty, the zero locus of the infimum equals the union of the zero loci of the individual ideals.

Русский

Если множество индексов конечно и ненулево, нулевая локация инфимации равна объединению нулевых локаций отдельных идеалов.

LaTeX

$$X.zeroLocus(U := U) ↑(⨅ i, I i) = ⋃ i, X.zeroLocus(U := U) (I i)$$

Lean4

theorem zeroLocus_iInf_of_nonempty {X : Scheme.{u}} {U : X.Opens} {ι : Type*} (I : ι → Ideal Γ(X, U)) [Finite ι]
    [Nonempty ι] : X.zeroLocus (U := U) ↑(⨅ i, I i) = ⋃ i, X.zeroLocus (U := U) (I i) := by
  simpa using zeroLocus_biInf_of_nonempty I Set.finite_univ

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