English
For a finite index set t and a family of ideals I_i, the zero locus of the infimum over i in t equals the union over i in t of the zero loci of I_i together with the complement of U.
Русский
Для конечного множителя t и семейства идеалов I_i нулевая локация инфимации по i в t равна объединению нулевых локаций I_i по i в t вместе с дополнением к U.
LaTeX
$$X.zeroLocus(U := U) ↑(⨅ i ∈ t, I i) = (⋃ i ∈ t, X.zeroLocus(U := U) (I i)) ∪ (↑U)ᶜ$$
Lean4
theorem zeroLocus_biInf {X : Scheme.{u}} {U : X.Opens} {ι : Type*} (I : ι → Ideal Γ(X, U)) {t : Set ι} (ht : t.Finite) :
X.zeroLocus (U := U) ↑(⨅ i ∈ t, I i) = (⋃ i ∈ t, X.zeroLocus (U := U) (I i)) ∪ (↑U)ᶜ :=
by
refine ht.induction_on _ (by simp) fun {i t} hit ht IH ↦ ?_
simp only [Set.mem_insert_iff, Set.iUnion_iUnion_eq_or_left, ← IH, ← zeroLocus_inf, Submodule.coe_inf,
Set.union_assoc]
congr!
simp
