noetherianSpace_of_isAffineOpen — Mathlib

English

A locally Noetherian scheme is quasi-separated.

Русский

Локально Ноетерова схема является квазираздельной.

LaTeX

$$$\text{QuasiSeparatedSpace}(X) \quad\text{when } X \text{ is locally Noetherian.}$$$

Lean4

theorem noetherianSpace_of_isAffineOpen (U : X.Opens) (hU : IsAffineOpen U) [IsNoetherianRing Γ(X, U)] :
    NoetherianSpace U :=
  by
  have : IsNoetherianRing Γ(U, ⊤) :=
    isNoetherianRing_of_ringEquiv _ (Scheme.restrictFunctorΓ.app (op U)).symm.commRingCatIsoToRingEquiv
  exact @noetherianSpace_of_isAffine _ hU _

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