The completion of a Huber ring #
The Hausdorff completion  of a Huber ring A is again a Huber ring. If (A₀, I) is a pair of
definition for A, then the closure Â₀ of the image of A₀ is an open subring of Â, and the
ideal Î of Â₀ generated by the image of I is an ideal of definition for it.
That Huber structure rests on one identity: the n-th power Îⁿ is exactly the closure of the
image of Iⁿ (TauCeti.Huber.PairOfDefinition.completionIdeal_pow). Those closures are a
neighbourhood basis of zero in Â, so the identity gives both halves of IsAdic Î at once. Read
from right to left it also makes the extension of an open ideal of A to  open: the closure of
the image of Iⁿ is the ideal of Â₀ generated by that image, so an ideal of  containing the
image already contains that closure, which is an open neighbourhood of zero.
The inclusion Îⁿ ⊆ closure (Iⁿ) is formal. The reverse inclusion is the substantial point, and
it is the only place where finite generation of I enters the proof of completionIdeal_pow:
fixing a finite family G generating Iⁿ, an element of the closure is approximated to order
n + k, for every k, by a combination of the same family G with coefficients in Iᵏ.
Finite generation is used once more, and directly, to see that Î is itself finitely generated
(TauCeti.Huber.PairOfDefinition.fg_completionIdeal). The coefficients accumulate to series which
converge because  is complete, and their sums exhibit the element as a combination of G.
Main definitions #
TauCeti.Huber.PairOfDefinition.completionRingOfDefinitionandTauCeti.Huber.PairOfDefinition.completionIdeal: the ring and the ideal of definition ofÂ.TauCeti.Huber.PairOfDefinition.completionIdealImage: the closure inÂof the image ofIⁿ, andTauCeti.Huber.PairOfDefinition.completionIdealImageIdeal, the ideal ofÂ₀it cuts out.TauCeti.Huber.PairOfDefinition.toCompletionRingOfDefinition: the completion map restricted toA₀and corestricted toÂ₀.TauCeti.Huber.PairOfDefinition.completion: the pair of definition ofÂthey assemble into.TauCeti.Huber.completionPlus: the plus ringÂ⁺of the completion, the closure of the image ofA⁺. It is opaque;completionPlus_defis its characterisation.
Main results #
TauCeti.Huber.PairOfDefinition.hasBasis_nhds_zero_completion: the closures of the images of the powersIⁿare a neighbourhood basis of zero inÂ;mem_nhds_completion_iffandexists_coe_sub_mem_completionIdealImageare its forms at an arbitrary point ofÂ.TauCeti.Huber.PairOfDefinition.completionIdeal_pow:Îⁿis the closure of the image ofIⁿ.TauCeti.Huber.PairOfDefinition.exists_sub_toCompletionRingOfDefinition_mem_completionIdeal_pow: every point ofÂ₀is congruent moduloÎⁿto the image of a point ofA₀.TauCeti.Huber.PairOfDefinition.isAdicComplete_completionIdeal:Â₀isÎ-adically complete.TauCeti.Huber.PairOfDefinition.completionIdealImage_le_of_image_subsetandTauCeti.Huber.isOpen_map_coeRingHom: an ideal ofÂcontaining the image ofIⁿcontains the whole closure of that image, so the ideal ofÂgenerated by the image of an open ideal ofAis open.TauCeti.Huber.IsHuberRing.completion: the completion of a Huber ring is a Huber ring, andTauCeti.Huber.IsTateRing.completion: the completion of a Tate ring is a Tate ring.TauCeti.Huber.topologicalClosure_map_coeRingHom_le_powerBoundedSubringandTauCeti.Huber.IsRingOfIntegralElements.completion: the closure inÂof the image of a subring ofA⁰lies inÂ⁰, and the closure of the image of a ring of integral elements ofAis a ring of integral elements ofÂ.TauCeti.Huber.topologicalClosure_map_coeRingHom_powerBoundedSubring: forA⁰itself the closure of the image is all ofÂ⁰.TauCeti.Huber.Pair.completionandTauCeti.Huber.Pair.completionHom: the completed Huber pair(Â, Â⁺), withÂ⁺the closure of the image ofA⁺, and the completion map as a morphism of Huber pairs.TauCeti.Huber.Pair.Hom.extensionextends a morphism into a complete Hausdorff Huber pair along it, uniquely byTauCeti.Huber.Pair.Hom.ext_completion, and agrees with it onAbyTauCeti.Huber.Pair.Hom.extension_toRingHom_coe.
References #
- Wedhorn, Adic Spaces, Remark 6.8 and Lemma 7.47.
- The Stacks Project, Lemma 10.96.3 (tag
05GG), the successive-approximation argument
behind the private
completionIdealImageIdeal_lebelow. - Mathlib's
Mathlib/Topology/Algebra/Nonarchimedean/Completion.lean, whoseCompletion.isDenseInducing_coeneighbourhood pattern is whatUniformSpace.Completion.isOpen_closure_image_coeadapts, and whichTauCeti.Huber.PairOfDefinition.hasBasis_nhds_zero_completionthen builds on.
The ring of definition of the completion: the closure in  of the image of A₀.
Instances For
Â₀ is the closure of the image of A₀, by definition.
Membership in Â₀.
An element of A whose image in  lies in Â₀ already lies in A₀. There is no
separation hypothesis on A: A₀ is open, hence closed, in A, so it is the preimage of the
closure of its image in Â.
The ring of definition of the completion is open.
The closure in  of the image of Iⁿ, as an additive subgroup. These closures are the
neighbourhood basis of zero of the completion, and they turn out to be the powers of the ideal of
definition of the completion (completionIdeal_pow).
Instances For
completionIdealImage is the closure of the image of Iⁿ, by definition.
The closure of the image of Iⁿ is open in Â.
The image of Iⁿ lies in its closure.
An element of A lies in the closure of the image of Iⁿ in  exactly when it lies in the
image of Iⁿ. There is no separation hypothesis on A, so this holds even when A → Â is not
injective; the implication from right to left is coe_mem_completionIdealImage.
The closures of the images of the Iⁿ decrease with n.
The closure of the image of Iⁿ lies in the ring of definition of the completion.
Wedhorn Remark 6.8: the closures of the images of the powers of the ideal of definition are a neighbourhood basis of zero in the completion.
A set is a neighbourhood of x in  exactly when it contains the translate by x of one of
the closures completionIdealImage n. This is hasBasis_nhds_zero_completion at the point x.
Approximation from A. Every point of  lies within completionIdealImage n of the image
of some element of A, for each n: the image of A is dense, and completionIdealImage n is a
neighbourhood of zero.
The closure of the image of Iⁿ absorbs multiplication by the ring of definition of the
completion, because Iⁿ is an ideal of A₀ and multiplication is continuous.
The closure of the image of Iⁿ, viewed as an ideal of the ring of definition of the
completion.
Instances For
Membership in the ideal cut out by the closure of the image of Iⁿ.
The completion map, restricted to a ring of definition and corestricted to the ring of definition of the completion.
Instances For
The corestricted completion map agrees with the completion map on A₀.
The ideal of definition of the completion: the ideal of Â₀ generated by the image of I.
Instances For
Unfolding lemma for TauCeti.Huber.PairOfDefinition.completionIdeal.
Membership in Î is membership in the ideal spanned by the image of I.
The image of an element of I lies in Î.
The ideal of definition of the completion is finitely generated.
Wedhorn Remark 6.8: the n-th power of the ideal of definition of the completion is exactly
the closure of the image of Iⁿ.
Approximation from A₀. Every point of Â₀ is congruent modulo Îⁿ to the image of a
point of A₀, for each n.
Wedhorn Remark 6.8: the subspace topology on the ring of definition of the completion is the adic topology of the ideal of definition of the completion.
Wedhorn Remark 6.8: a pair of definition of A induces one of the completion of A, with the
closure of the image of A₀ as ring of definition and the ideal generated by the image of I as
ideal of definition.
Instances For
The ring of definition of the induced pair is Â₀.
Membership in the ideal of definition of the completed pair is membership in I · Â₀.
Stated as a membership characterisation rather than an equation because the type of
idealOfDefinition depends on ringOfDefinition, which the opaque body of completion does not
expose.
Â₀ is Î-adically complete (Wedhorn, Remark 6.8). This is the completeness of the ring of
definition of the complete Hausdorff Huber ring Â, for the completed pair.
An ideal of  that contains the image of Iⁿ contains the whole closure of that image. The
hypothesis constrains J only at the points of  that come from A.
The extension of an open ideal along the completion map is open: for an open ideal J of
a Huber ring A, the ideal of  generated by the image of J is open.
Wedhorn Remark 6.8: the completion of a Huber ring is a Huber ring.
Wedhorn Remark 6.8: the completion of a Tate ring is a Tate ring.
The closure in  of the image of a subring of A⁰ lies in Â⁰: the image lies in Â⁰
by isPowerBounded_completion_coe_of_isPowerBounded, and Â⁰ is open, hence closed.
Â⁰ is the closure in  of the image of A⁰, for a Huber ring A. This upgrades the
inclusion topologicalClosure_map_coeRingHom_le_powerBoundedSubring, taken for R = A⁰, to an
equality.
Completion preserves rings of integral elements (Wedhorn, Lemma 7.47): the closure in Â
of the image of a ring of integral elements of a Huber ring A is a ring of integral elements of
Â.
The plus ring of the completion: the closure in  of the image of A⁺. When A⁺ is a ring
of integral elements so is this, by TauCeti.Huber.IsRingOfIntegralElements.completion, which is
Wedhorn's Lemma 7.47.
Instances For
completionPlus is the closure of the image of A⁺. The unbundled statements, whose plus ring
is spelled out, go through this lemma: completionPlus is opaque outside this module.
The completion map carries A⁺ into Â⁺: this is the hplus argument spaComap takes
along A → Â.
The completion of a Huber pair #
The completion (Â, Â⁺) of a Huber pair (A, A⁺): Â⁺ is the closure in  of the
image of A⁺, a ring of integral elements by TauCeti.Huber.IsRingOfIntegralElements.completion
(Wedhorn, Lemma 7.47).
Instances For
The plus ring of the completed pair is completionPlus A⁺, the closure of the image of A⁺.
The completion map (A, A⁺) → (Â, Â⁺) as a morphism of Huber pairs.
Instances For
The underlying ring homomorphism of the completion morphism is the completion map.
A morphism into a complete Hausdorff Huber pair extends to the completed pair: the
continuous extension  → B of f carries Â⁺ into B⁺, since B⁺ is open and hence closed.
Instances For
The underlying ring homomorphism of the extension is the continuous extension of f.
The extension of f agrees with f on the image of A.
The extension of f agrees with f after the completion morphism.
The extension of f restricts to f along the completion map.
Morphisms out of the completed pair are determined on A: two morphisms into a Hausdorff
Huber pair that agree after the completion map are equal.