fromSpec_image_zeroLocus — Mathlib

English

Let X be a Scheme and U an affine-open. For a set s of global sections on X restricted to U, the image under the canonical map to X intersects the zero locus as X.zeroLocus(s) ∩ U.

Русский

Пусть X — схема, U — аффинно открытое. Для множества s глобальных секций на X, ограниченных на U, образ через каноническое отображение пересекает нулевую локацию: X.zeroLocus(s) ∩ U.

LaTeX

$$$h_U.fromSpec.base '' PrimeSpectrum.zeroLocus(s) = X.zeroLocus(s) \cap U$$$

Lean4

theorem fromSpec_image_zeroLocus {X : Scheme.{u}} {U : X.Opens} (hU : IsAffineOpen U) (s : Set Γ(X, U)) :
    hU.fromSpec.base '' PrimeSpectrum.zeroLocus s = X.zeroLocus s ∩ U := by
  rw [← hU.fromSpec_preimage_zeroLocus, Set.image_preimage_eq_inter_range, range_fromSpec]

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