preimage_zeroLocus — Mathlib

English

For a morphism f: X → Y and an open U ⊆ Y with s ⊆ Γ(Y, U), the preimage of the zero locus of s equals the zero locus of the pushforward of s along f restricted to U: f.base^{-1} Y.zeroLocus s = X.zeroLocus ((f.app U).hom '' s).

Русский

Для морфизма f: X → Y и открытого U ⊆ Y с s ⊆ Γ(Y, U) предобраз нулевой области s по f равен нулевой области образа s по f на U: f.base^{-1} Y.zeroLocus s = X.zeroLocus ((f.app U).hom '' s).

LaTeX

$$$f.base^{-1} Y.zeroLocus(s) = X.zeroLocus\big((f.app U).hom '' s\big)$$$

Lean4

theorem preimage_zeroLocus {X Y : Scheme.{u}} (f : X ⟶ Y) {U : Y.Opens} (s : Set Γ(Y, U)) :
    f.base ⁻¹' Y.zeroLocus s = X.zeroLocus ((f.app U).hom '' s) :=
  by
  ext
  simp [← Scheme.preimage_basicOpen]
  rfl

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