English
The zero locus of the infimum of two ideals I and J in Γ(X, U) equals the union of their zero loci: zeroLocus(I ⊓ J) = zeroLocus(I) ∪ zeroLocus(J).
Русский
Нулевая локация пересечения двух идеалов I и J в Γ(X, U) равна объединению нулевых локаций I и J.
LaTeX
$$$X.zeroLocus(U := U) \uparrow(I \inf J) = X.zeroLocus(U := U) I \cup X.zeroLocus(U := U) J$$$
Lean4
theorem zeroLocus_inf (X : Scheme.{u}) {U : X.Opens} (I J : Ideal Γ(X, U)) :
X.zeroLocus (U := U) ↑(I ⊓ J) = X.zeroLocus (U := U) I ∪ X.zeroLocus (U := U) J :=
by
suffices U.1 ↓∩ (X.zeroLocus (U := U) ↑(I ⊓ J)) = U.1 ↓∩ (X.zeroLocus (U := U) I ∪ X.zeroLocus (U := U) J)
by
ext x
by_cases hxU : x ∈ U
· simpa [hxU] using congr(⟨x, hxU⟩ ∈ $this)
·
simp only [Submodule.coe_inf, Set.mem_union,
codisjoint_iff_compl_le_left.mp (X.codisjoint_zeroLocus (U := U) (I ∩ J)) hxU,
codisjoint_iff_compl_le_left.mp (X.codisjoint_zeroLocus (U := U) I) hxU, true_or]
simp only [← U.toSpecΓ_preimage_zeroLocus, PrimeSpectrum.zeroLocus_inf I J, Set.preimage_union]