exists_of_res_zero_of_qcqs — Mathlib

English

If a localization of a section f equals zero on a qcqs open, then some power of f kills the witness; i.e., there exists n with s^n f = 0.

Русский

Если локализация секции f равна нулю на qcqs открытом, то некоторый показатель степени f аннигилируется: существует n, такое что s^n f = 0.

LaTeX

$$$$\\exists n, s^{n} \\cdot f = 0$$$$

Lean4

theorem exists_of_res_zero_of_qcqs {X : Scheme.{u}} {U : TopologicalSpace.Opens X} (hU : IsCompact U.carrier)
    (hU' : IsQuasiSeparated U.carrier) {f s : Γ(X, U)} (hf : f |_ X.basicOpen s = 0) : ∃ n, s ^ n * f = 0 :=
  by
  suffices h : ∃ n, s ^ n * f = s ^ n * 0 by simpa using h
  apply exists_of_res_eq_of_qcqs hU hU'
  simpa

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