fromSpec_preimage_zeroLocus — Mathlib

English

If U is affine-open, then the preimage of the zero locus of a set of global sections on X under the map from U to Γ(X, U) identifies with the zero locus of the same set in Spec of the global sections.

Русский

Если U — аффинно-открытое подмножество, то предобраз нулевой локации множества глобальных секций на X под маппингом от U к Γ(X, U) совпадает с нулевой локацией того же множества в Spec Γ(X, U).

LaTeX

$$If [IsAffineOpen U], then $h_U.fromSpec.base^{-1}' X.zeroLocus(s) = \operatorname{PrimeSpectrum.zeroLocus}(s)$.$$

Lean4

theorem fromSpec_preimage_zeroLocus {X : Scheme.{u}} {U : X.Opens} (hU : IsAffineOpen U) (s : Set Γ(X, U)) :
    hU.fromSpec.base ⁻¹' X.zeroLocus s = PrimeSpectrum.zeroLocus s :=
  by
  ext x
  suffices (∀ f ∈ s, ¬f ∉ x.asIdeal) ↔ s ⊆ x.asIdeal by simpa [← hU.fromSpec_image_basicOpen, -not_not] using this
  simp_rw [not_not]
  rfl

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