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.
Main results #
TauCeti.Huber.isBounded_image_completion_coe_of_isBoundedandTauCeti.Huber.isPowerBounded_completion_coe_of_isPowerBounded: boundedness and power-boundedness transfer fromAto its completion along the canonical map. Both are stated for a Huber ring, with no pair of definition in the signature.TauCeti.Huber.isBounded_of_isBounded_image_completion_coeandTauCeti.Huber.isPowerBounded_of_isPowerBounded_completion_coe: the converses, which come back down toAthrough the open-subgroup correspondenceUniformSpace.Completion.preimage_closure_image_coe.TauCeti.Huber.isPowerBounded_completion_coe_iff: the two power-bounded directions together — Wedhorn's Lemma 7.47(1) at the level of elements, thatA⁰is the preimage ofÂ⁰.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.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Â.
References #
- Wedhorn, Adic Spaces, Remark 6.8.
- 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₀.
Equations
Instances For
Â₀ is the closure of the image of A₀, by definition.
Membership 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).
Equations
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.
Equations
- P.completionIdealImageIdeal n = { carrier := {y : ↥P.completionRingOfDefinition | ↑y ∈ P.completionIdealImage n}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
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.
Equations
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.
Equations
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ⁿ.
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.
Equations
- One or more equations did not get rendered due to their size.
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.
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.
The image of a bounded subset of A is bounded in Â.
Stated for a Huber ring rather than for a chosen pair of definition: the conclusion does not mention one, so the choice is internal to the proof.
The closure argument follows AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0, branch
dev/adic-spaces at 37bbdaeb9), projects/AdicSpaces/Adic spaces/LocalizationTopology.lean:545,
where it is stated for the rational-localisation completion. No proof was copied.
The converse of isBounded_image_completion_coe_of_isBounded. A set whose image in  is
bounded was already bounded in A.
A power-bounded element of A stays power-bounded in Â.
The converse of isPowerBounded_completion_coe_of_isPowerBounded. An element of A whose
image in  is power-bounded was already power-bounded.
Wedhorn Lemma 7.47(1), at the level of elements: A⁰ is the preimage of Â⁰. An element of
A is power-bounded exactly when its image in the completion is.
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.
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
Â.