isLocallyNoetherian_iff_of_iSup_eq_top

English

A scheme is locally Noetherian iff all rings of sections over an affine iSup cover are Noetherian.

Русский

Схема локально Ноетерова тогда и только тогда, когда все кольца секций над афинными покрывающими элементами iSup являются Ноетериновыми.

LaTeX

$$$\text{IsLocallyNoetherian}(X) \iff \forall i, \text{IsNoetherianRing}(\Gamma(X, S_i)).$$$

Lean4

/-- A scheme is locally Noetherian if and only if it is covered by affine opens whose sections
are Noetherian rings.

See [Har77], Proposition II.3.2. -/
theorem isLocallyNoetherian_iff_of_iSup_eq_top {ι} {S : ι → X.affineOpens} (hS : (⨆ i, S i : X.Opens) = ⊤) :
    IsLocallyNoetherian X ↔ ∀ i, IsNoetherianRing Γ(X, S i) :=
  ⟨fun _ i => IsLocallyNoetherian.component_noetherian (S i), isLocallyNoetherian_of_affine_cover hS⟩

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