zeroLocus_eq_univ_iff_subset_nilradical

English

In a scheme, an element is nilpotent iff it lies in the nilradical of the global sections ring.

Русский

В схеме элемент нильпотентен тогда и только тогда, когда он лежит в нильрадикале кольца глобальных секций.

LaTeX

$$$\\text{IsNilpotent}(f) \\iff f \\in \\text{nilradical}(\\Gamma(X,\\mathcal{O}_X))$$$

Lean4

/-- The zero locus of a set of sections over a compact open of a scheme is `X` if and only if
`s` is contained in the nilradical of `Γ(X, U)`. -/
theorem zeroLocus_eq_univ_iff_subset_nilradical {X : Scheme.{u}} [CompactSpace X] (s : Set Γ(X, ⊤)) :
    X.zeroLocus s = Set.univ ↔ s ⊆ nilradical Γ(X, ⊤) :=
  zeroLocus_eq_univ_iff_subset_nilradical_of_isCompact (U := ⊤) (CompactSpace.isCompact_univ) s

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