isNoetherian_iff_of_finite_affine_openCover

English

A scheme is Noetherian iff it is covered by finitely many affine opens whose sections are Noetherian rings.

Русский

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

LaTeX

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

Lean4

/-- A version of `isNoetherian_iff_of_finite_iSup_eq_top` using `Scheme.OpenCover`. -/
theorem isNoetherian_iff_of_finite_affine_openCover {𝒰 : Scheme.OpenCover.{v, u} X} [Finite 𝒰.I₀]
    [∀ i, IsAffine (𝒰.X i)] : IsNoetherian X ↔ ∀ (i : 𝒰.I₀), IsNoetherianRing Γ(𝒰.X i, ⊤) :=
  by
  constructor
  · intro h i
    apply (isLocallyNoetherian_iff_of_affine_openCover _).mp
    exact h.toIsLocallyNoetherian
  · intro hNoeth
    convert IsNoetherian.mk
    · exact (isLocallyNoetherian_iff_of_affine_openCover _).mpr hNoeth
    · exact Scheme.OpenCover.compactSpace 𝒰

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