exists_of_res_zero_of_qcqs_of_top

English

Top-level variant: if a localized restriction of f is zero on the top level, then a power of f is zero on the top level as well.

Русский

В верхнем уровне локализации: если локализация f равна нулю на вершине, то и f в итоге обнулится после некоторой степени.

LaTeX

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

Lean4

theorem exists_of_res_zero_of_qcqs_of_top {X : Scheme} [CompactSpace X] [QuasiSeparatedSpace X] {f s : Γ(X, ⊤)}
    (hf : f |_ X.basicOpen s = 0) : ∃ n, s ^ n * f = 0 :=
  exists_of_res_zero_of_qcqs (U := ⊤) CompactSpace.isCompact_univ isQuasiSeparated_univ hf

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