isNilpotent_iff_basicOpen_eq_bot — Mathlib

English

A global section on a compact scheme is nilpotent if and only if its basic open is empty.

Русский

Глобальная секция на компактной схеме нильпотентна тогда и только тогда, когда её базовый открытый пуст.

LaTeX

$$$IsNilpotent(f) \\iff X.basicOpen(f) = ⊥$ for a suitable f$$

Lean4

/-- A global section of a quasi-compact scheme is nilpotent if and only if its associated
basic open is empty. -/
theorem isNilpotent_iff_basicOpen_eq_bot {X : Scheme.{u}} [CompactSpace X] (f : Γ(X, ⊤)) :
    IsNilpotent f ↔ X.basicOpen f = ⊥ :=
  isNilpotent_iff_basicOpen_eq_bot_of_isCompact (U := ⊤) (CompactSpace.isCompact_univ) f

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