Noetherianity of adically complete rings and of adic completions

A ring R that is I-adically complete for a finitely generated ideal I is Noetherian as soon as R ⧸ I is. Consequently the adic completion of a Noetherian ring is Noetherian, and more generally the completion along a finitely generated ideal I is Noetherian when R ⧸ I is. These are the noetherianity inputs for adic rings of finite ideal type and for rings of definition of Huber rings, where completions of Noetherian rings appear throughout.

The complete-ring criterion supplies the Noetherian rings of definition needed when constructing adic rings, while its completion specialization applies directly to completions of Noetherian rings and to finitely generated ideals with Noetherian quotient.

Main results

• Ideal.isNoetherianRing_of_isAdicComplete: an I-adically complete ring with I finitely generated and R ⧸ I Noetherian is Noetherian.
• Ideal.isNoetherianRing_adicCompletion_of_fg: the completion along a finitely generated ideal I is Noetherian when R ⧸ I is.
• Ideal.isNoetherianRing_adicCompletion: the adic completion of a Noetherian ring is Noetherian.
• IsLocalRing.isNoetherianRing_adicCompletion_of_fg: the completion of a local ring with finitely generated maximal ideal is Noetherian.
• Ideal.isNoetherianRing_of_isAdicComplete_of_denseRange: an I-adically complete ring with separately continuous addition and I finitely generated and open is Noetherian as soon as it receives a ring map with dense range from a Noetherian semiring. This is the form used for topological completions.

References

• A. Grothendieck and J. Dieudonné, Éléments de géométrie algébrique I, Ch. 0, 7.2.6 and 7.2.12.
• M. F. Atiyah, I. G. Macdonald, Introduction to Commutative Algebra, Chapter 10.

theorem Ideal.isNoetherianRing_of_isAdicComplete {R : Type u_1} [CommRing R] (I : Ideal R) (hI : I.FG) [IsAdicComplete I R] [IsNoetherianRing (R ⧸ I)] : IsNoetherianRing R

Noetherianity of complete rings. A ring that is I-adically complete for a finitely generated ideal I is Noetherian as soon as R ⧸ I is Noetherian.

theorem Ideal.isNoetherianRing_adicCompletion_of_fg {R : Type u_1} [CommRing R] (I : Ideal R) (hI : I.FG) [IsNoetherianRing (R ⧸ I)] : IsNoetherianRing (AdicCompletion I R)

The adic completion along a finitely generated ideal I is Noetherian as soon as R ⧸ I is: it is complete for the extended ideal I • R̂, with quotient R̂ ⧸ I • R̂ ≃ R ⧸ I.

instance Ideal.isNoetherianRing_adicCompletion {R : Type u_1} [CommRing R] (I : Ideal R) [IsNoetherianRing R] : IsNoetherianRing (AdicCompletion I R)

The adic completion of a Noetherian ring along any ideal is Noetherian.

theorem Ideal.isNoetherianRing_of_isAdicComplete_of_denseRange {R : Type u_1} [CommRing R] {I : Ideal R} [TopologicalSpace R] [SeparatelyContinuousAdd R] (hI : I.FG) (hIo : IsOpen ↑I) [IsAdicComplete I R] {A : Type u_2} [Semiring A] [IsNoetherianRing A] {f : A →+* R} (hf : DenseRange ⇑f) : IsNoetherianRing R

Noetherianity of complete rings with a dense Noetherian subsemiring. A ring with separately continuous addition that is I-adically complete for a finitely generated open ideal I is Noetherian as soon as it receives a ring homomorphism with dense range from a Noetherian semiring.

theorem IsLocalRing.isNoetherianRing_adicCompletion_of_fg {R : Type u_1} [CommRing R] [IsLocalRing R] (h : (maximalIdeal R).FG) : IsNoetherianRing (AdicCompletion (maximalIdeal R) R)

The completion of a local ring at its finitely generated maximal ideal is Noetherian.