instIsNoetherianRingCarrierOfIsLocallyNoetherianSpec

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

instance (priority := 100) {R : CommRingCat} [IsLocallyNoetherian (Spec R)] : IsNoetherianRing R :=
  by
  have := IsLocallyNoetherian.component_noetherian ⟨⊤, AlgebraicGeometry.isAffineOpen_top (Spec R)⟩
  apply isNoetherianRing_of_ringEquiv Γ(Spec R, ⊤)
  apply CategoryTheory.Iso.commRingCatIsoToRingEquiv
  exact Scheme.ΓSpecIso R

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