English
If a finite set of elements generates the unit ideal in R, and all localizations along them are Noetherian, then R is Noetherian.
Русский
Если конечная система элементов порождает единичный идеал в R, и все локализации по ним Ноетериевые, тогда и сам R Ноetherиев.
LaTeX
$$$\text{IsNoetherianRing}(R) \wedge (S:\text{Finset} R) \Rightarrow \text{Under localization along S, finite-Noetherian implies Noetherian}.$$$
Lean4
/-- A scheme is Noetherian if and only if it is covered by finitely many affine opens whose
sections are Noetherian rings. -/
theorem isNoetherian_iff_of_finite_iSup_eq_top {ι} [Finite ι] {S : ι → X.affineOpens} (hS : (⨆ i, S i : X.Opens) = ⊤) :
IsNoetherian X ↔ ∀ i, IsNoetherianRing Γ(X, S i) :=
by
constructor
· intro h i
apply (isLocallyNoetherian_iff_of_iSup_eq_top hS).mp
exact h.toIsLocallyNoetherian
· intro h
convert IsNoetherian.mk
· exact isLocallyNoetherian_of_affine_cover hS h
· constructor
rw [← Opens.coe_top, ← hS, Opens.iSup_mk]
apply isCompact_iUnion
intro i
apply isCompact_iff_isCompact_univ.mpr
convert CompactSpace.isCompact_univ
have : NoetherianSpace (S i) := by apply noetherianSpace_of_isAffineOpen (S i).1 (S i).2
apply NoetherianSpace.compactSpace (S i)
