Noetherianity of completions of adic rings and of rings of definition

Let R be a commutative ring whose topology is the I-adic topology for a finitely generated ideal I. Its Hausdorff completion R̂ (Mathlib's UniformSpace.Completion) carries the adic topology of the extended ideal I·R̂, and is complete for it. If R is Noetherian, so is R̂.

The same argument applies to a ring of definition A₀ of a Huber ring A: if A₀ is Noetherian, then so is the ring of definition Â₀ of the completion Â, namely the closure of the image of A₀ (TauCeti.Huber.PairOfDefinition.completion). Consequently the completion of a Huber ring of noetherian type is again of noetherian type. This is the form in which a noetherian hypothesis on a possibly incomplete Huber ring reaches its completion, as in Huber's sheafiness theorem for rings with a noetherian ring of definition.

In both cases the completed ring is adically complete for a finitely generated open ideal, and its quotient by that ideal is the quotient of the original ring. More precisely, Â₀ is the I-adic completion of A₀ in the algebraic sense: it is Î-adically complete and separated, where Î is the ideal generated by the image of I, and the completion map induces ring isomorphisms A₀ ⧸ Iⁿ ≃ Â₀ ⧸ Îⁿ for every n, because Îⁿ is the closure of the image of Iⁿ (TauCeti.Huber.PairOfDefinition.completionIdeal_pow). With the noetherianity criterion for complete rings (Ideal.isNoetherianRing_of_isAdicComplete), Â₀ is therefore Noetherian as soon as A₀ ⧸ I is, and likewise R̂ is Noetherian as soon as R ⧸ I is, for I finitely generated. The Noetherian results above are the special cases where A₀, respectively R, is Noetherian.

Main results

• IsAdic.map_coeRingHom: the topology of R̂ is the I·R̂-adic topology, for I finitely generated.
• IsAdic.isAdicComplete_map_coeRingHom: R̂ is I·R̂-adically complete.
• IsAdic.isNoetherianRing_completion: the completion of a Noetherian ring for an adic topology is Noetherian.
• TauCeti.Huber.PairOfDefinition.isNoetherianRing_completion: the completion of a Noetherian ring of definition is a Noetherian ring of definition of the completion.
• TauCeti.Huber.PairOfDefinition.quotientPowEquivCompletion: the isomorphism A₀ ⧸ Iⁿ ≃+* Â₀ ⧸ Îⁿ induced by the completion map.
• TauCeti.Huber.PairOfDefinition.isNoetherianRing_completionRingOfDefinition_of_quotient: Â₀ is Noetherian as soon as A₀ ⧸ I is.
• IsAdic.isNoetherianRing_completion_of_quotient: the completion of an adic ring is Noetherian as soon as R ⧸ I is, for I finitely generated.
• TauCeti.Huber.IsNoetherianType.completion: the completion of a Huber ring of noetherian type is of noetherian type.

References

• The Stacks Project, Lemma 10.96.3 (tag 05GG).
• A. Grothendieck and J. Dieudonné, Éléments de géométrie algébrique I, Ch. 0, (7.2.6) and (7.3.1).
• R. Huber, A generalization of formal schemes and rigid analytic varieties, Math. Z. 217 (1994), §2, Theorem 2.2.
• T. Wedhorn, Adic Spaces, Remark 6.8, Proposition 6.35 and Remark 6.37.

theorem IsAdic.map_coeRingHom {R : Type u_1} [CommRing R] [UniformSpace R] [IsUniformAddGroup R] [IsTopologicalRing R] {I : Ideal R} (hI : IsAdic I) (hfg : I.FG) : IsAdic (Ideal.map UniformSpace.Completion.coeRingHom I)

The completion of an adic ring is adic for the extended ideal (Stacks, Tag 05GG). If the topology of R is I-adic for a finitely generated ideal I, the topology of its Hausdorff completion R̂ is the I·R̂-adic topology.

theorem IsAdic.isAdicComplete_map_coeRingHom {R : Type u_1} [CommRing R] [UniformSpace R] [IsUniformAddGroup R] [IsTopologicalRing R] {I : Ideal R} (hI : IsAdic I) (hfg : I.FG) : IsAdicComplete (Ideal.map UniformSpace.Completion.coeRingHom I) (UniformSpace.Completion R)

The completion of an adic ring is adically complete for the extended ideal (Stacks, Tag 05GG). If the topology of R is I-adic for a finitely generated ideal I, its Hausdorff completion R̂ is I·R̂-adically complete and separated.

theorem TauCeti.Huber.PairOfDefinition.mk_comp_toCompletionRingOfDefinition_surjective {R : Type u_1} [CommRing R] [UniformSpace R] [IsUniformAddGroup R] [IsTopologicalRing R] (P : PairOfDefinition R) (n : ℕ) : Function.Surjective ⇑((Ideal.Quotient.mk (P.completionIdeal ^ n)).comp P.toCompletionRingOfDefinition)

The completion map A₀ → Â₀ ⧸ Îⁿ is surjective: every point of Â₀ is congruent modulo the open ideal Îⁿ to the image of a point of A₀.

theorem TauCeti.Huber.PairOfDefinition.ker_mk_comp_toCompletionRingOfDefinition {R : Type u_1} [CommRing R] [UniformSpace R] [IsUniformAddGroup R] [IsTopologicalRing R] (P : PairOfDefinition R) (n : ℕ) : RingHom.ker ((Ideal.Quotient.mk (P.completionIdeal ^ n)).comp P.toCompletionRingOfDefinition) = P.idealOfDefinition ^ n

The kernel of the completion map A₀ → Â₀ ⧸ Îⁿ is Iⁿ.

noncomputable def TauCeti.Huber.PairOfDefinition.quotientPowEquivCompletion {R : Type u_1} [CommRing R] [UniformSpace R] [IsUniformAddGroup R] [IsTopologicalRing R] (P : PairOfDefinition R) (n : ℕ) : ↥P.ringOfDefinition ⧸ P.idealOfDefinition ^ n ≃+* ↥P.completionRingOfDefinition ⧸ P.completionIdeal ^ n

A₀ ⧸ Iⁿ ≃ Â₀ ⧸ Îⁿ (EGA I, Ch. 0, (7.3.1)). The completion map induces an isomorphism of each quotient of the ring of definition by a power of the ideal of definition with the corresponding quotient of the ring of definition of the completion.

@[simp]

theorem TauCeti.Huber.PairOfDefinition.quotientPowEquivCompletion_mk {R : Type u_1} [CommRing R] [UniformSpace R] [IsUniformAddGroup R] [IsTopologicalRing R] (P : PairOfDefinition R) (n : ℕ) (x : ↥P.ringOfDefinition) : (P.quotientPowEquivCompletion n) ((Ideal.Quotient.mk (P.idealOfDefinition ^ n)) x) = (Ideal.Quotient.mk (P.completionIdeal ^ n)) (P.toCompletionRingOfDefinition x)

The isomorphism A₀ ⧸ Iⁿ ≃ Â₀ ⧸ Îⁿ is induced by the completion map.

theorem TauCeti.Huber.PairOfDefinition.isNoetherianRing_completionRingOfDefinition_of_quotient {R : Type u_1} [CommRing R] [UniformSpace R] [IsUniformAddGroup R] [IsTopologicalRing R] (P : PairOfDefinition R) [IsNoetherianRing (↥P.ringOfDefinition ⧸ P.idealOfDefinition)] : IsNoetherianRing ↥P.completionRingOfDefinition

The ring of definition of the completion is Noetherian as soon as A₀ ⧸ I is (EGA I, Ch. 0, (7.2.6)): Â₀ is complete for the finitely generated ideal Î, and Â₀ ⧸ Î ≃ A₀ ⧸ I.

instance TauCeti.Huber.PairOfDefinition.isNoetherianRing_completion {R : Type u_1} [CommRing R] [UniformSpace R] [IsUniformAddGroup R] [IsTopologicalRing R] (P : PairOfDefinition R) [IsNoetherianRing ↥P.ringOfDefinition] : IsNoetherianRing ↥P.completion.ringOfDefinition

The completion of a Noetherian ring of definition is Noetherian (EGA I, Ch. 0, (7.2.6)). If a pair of definition (A₀, I) of R has A₀ Noetherian, the ring of definition Â₀ of the completed pair P.completion, the closure of the image of A₀ in R̂, is Noetherian.

instance TauCeti.Huber.IsNoetherianType.completion {R : Type u_1} [CommRing R] [UniformSpace R] [IsUniformAddGroup R] [IsTopologicalRing R] [IsHuberRing R] [IsNoetherianType R] : IsNoetherianType (UniformSpace.Completion R)

The completion of a Huber ring of noetherian type is of noetherian type. A Noetherian ring of definition of R completes to a Noetherian ring of definition of R̂ (TauCeti.Huber.PairOfDefinition.isNoetherianRing_completion), and a strongly noetherian Tate ring completes to a strongly noetherian Tate ring.

theorem IsAdic.isNoetherianRing_completion_of_quotient {R : Type u_1} [CommRing R] [UniformSpace R] [IsUniformAddGroup R] [IsTopologicalRing R] {I : Ideal R} (hI : IsAdic I) (hfg : I.FG) [IsNoetherianRing (R ⧸ I)] : IsNoetherianRing (UniformSpace.Completion R)

The completion of an adic ring is Noetherian as soon as R ⧸ I is (EGA I, Ch. 0, (7.2.6)), for a finitely generated ideal I defining the topology.

theorem IsAdic.isNoetherianRing_completion {R : Type u_1} [CommRing R] [UniformSpace R] [IsUniformAddGroup R] [IsTopologicalRing R] {I : Ideal R} [IsNoetherianRing R] (hI : IsAdic I) : IsNoetherianRing (UniformSpace.Completion R)

The completion of a Noetherian ring for an adic topology is Noetherian (EGA I, Ch. 0, (7.3.1)). If the topology of a Noetherian ring R is I-adic for some ideal I, its Hausdorff completion is Noetherian.