germ_eq_zero_of_pow_mul_eq_zero — Mathlib

English

If the germ at x of f is considered in the basic open defined by s and s^n f = 0, then the germ vanishes: germ U x x.2 f = 0.

Русский

Если на точке x в базовом открытом множестве, заданном s, выполняется s^n f = 0, то локальная обобщение (germ) f в x равно нулю.

LaTeX

$$$X.presheaf.germ U x x.2 f = 0$ under the assumption $x \in X.basicOpen s$ and $s^n f = 0$ for some n.$$

Lean4

theorem germ_eq_zero_of_pow_mul_eq_zero {X : Scheme.{u}} {U : Opens X} (x : U) {f s : Γ(X, U)}
    (hx : x.val ∈ X.basicOpen s) {n : ℕ} (hf : s ^ n * f = 0) : X.presheaf.germ U x x.2 f = 0 :=
  by
  rw [Scheme.mem_basicOpen X s x x.2] at hx
  have hu : IsUnit (X.presheaf.germ _ x x.2 (s ^ n)) :=
    by
    rw [map_pow]
    exact IsUnit.pow n hx
  rw [← hu.mul_right_eq_zero, ← map_mul, hf, map_zero]

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