instIsLocallyNoetherianSpecOfIsNoetherianRingCarrier

English

If Spec R is locally Noetherian, then R is Noetherian.

Русский

Если Spec R локально Ноетерова, то R — Ноetherian.

LaTeX

$$$[\text{IsLocallyNoetherian}(\operatorname{Spec} R)] \Rightarrow [\text{IsNoetherianRing} R].$$$

Lean4

/-- If `R` is a Noetherian ring, `Spec R` is a locally Noetherian scheme. -/
instance {R : CommRingCat} [IsNoetherianRing R] : IsLocallyNoetherian (Spec R) :=
  by
  apply isLocallyNoetherian_of_affine_cover (ι := Fin 1) (S := fun _ => ⟨⊤, isAffineOpen_top (Spec R)⟩)
  · exact iSup_const
  · intro
    apply isNoetherianRing_of_ringEquiv R
    apply CategoryTheory.Iso.commRingCatIsoToRingEquiv
    exact (Scheme.ΓSpecIso R).symm

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