zeroLocus_inf — Mathlib

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]

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