zeroLocus_biInf_of_nonempty — Mathlib

English

If t is finite and nonempty, the zero locus of the infimum over i in t of I_i equals the union over i in t of the zero loci of I_i, inside U.

Русский

Если t конечно и ненулево, то нулевая локация inf по i в t идеалов I_i равна объединению нулевых локаций I_i по i в t, внутри U.

LaTeX

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

Lean4

theorem zeroLocus_biInf_of_nonempty {X : Scheme.{u}} {U : X.Opens} {ι : Type*} (I : ι → Ideal Γ(X, U)) {t : Set ι}
    (ht : t.Finite) (ht' : t.Nonempty) : X.zeroLocus (U := U) ↑(⨅ i ∈ t, I i) = ⋃ i ∈ t, X.zeroLocus (U := U) (I i) :=
  by
  rw [zeroLocus_biInf I ht, Set.union_eq_left]
  obtain ⟨i, hi⟩ := ht'
  exact fun x hx ↦
    Set.mem_iUnion₂_of_mem hi (codisjoint_iff_compl_le_left.mp (X.codisjoint_zeroLocus (U := U) (I i)) hx)

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