zeroLocus_eq_univ_iff_subset_nilradical_of_isCompact

English

In a compact scheme, a section is nilpotent iff its associated basic open is the bottom element of the frame of opens.

Русский

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

LaTeX

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

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_of_isCompact {X : Scheme.{u}} {U : X.Opens} (hU : IsCompact (U : Set X))
    (s : Set Γ(X, U)) : X.zeroLocus s = Set.univ ↔ s ⊆ nilradical Γ(X, U) := by
  simp [Scheme.zeroLocus_def, ← Scheme.isNilpotent_iff_basicOpen_eq_bot_of_isCompact hU, ← mem_nilradical,
    Set.subset_def]

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