The trivial presentation: A⟨T/1⟩ is the completion of A #
This file identifies the completed localisation A⟨T/1⟩ with the Hausdorff completion of A.
Everything rests on one computation: for numerators lying in the ring of definition, the
localisation topology at the denominator 1 is the topology A already carries.
locSubring P T 1 A = A₀ the candidate ring of definition is A₀ itself
locIdealImage P T 1 A n = Iⁿ so the basic neighbourhoods are those of A
locTopology P T 1 A _ = ‹TopologicalSpace A› and the two topologies agree
The uniformities then agree as well, so A⟨T/1⟩ is the Hausdorff completion  of A, and
when A is already complete and Hausdorff the structure map A → A⟨T/1⟩ is an isomorphism of
topological rings.
The hypothesis on the numerators #
The exact subring and ideal computations ask the numerators to lie in P.ringOfDefinition, not
merely to be power-bounded. That is the honest hypothesis for a fixed pair of definition P: an
element of A° outside A₀ enlarges D = A₀[T] past A₀, and locSubring P T 1 A = A₀ is then
false. The topology and uniformity computations only require the numerators to be power-bounded:
adjoining a finite power-bounded family gives the same D and extended ideal as the localisation
construction, and the enlarged pair still induces the original topology. The universal-property
identification with A likewise does not change P.
Main results #
TauCeti.Huber.PairOfDefinition.hasDenominatorPower_denom_one: at the denominator1the standing hypothesis of the construction is automatic, for every numerator set and every localisation.TauCeti.Huber.PairOfDefinition.locSubring_denom_oneandTauCeti.Huber.PairOfDefinition.locIdealImage_denom_one: the candidate ring of definition and the basic neighbourhoods of zero are those ofA.TauCeti.Huber.PairOfDefinition.locTopology_denom_one: the localisation topology at the denominator1is the topology ofA, andTauCeti.Huber.PairOfDefinition.locUniformSpace_denom_onesays the same of the uniformity, soA⟨T/1⟩is the Hausdorff completion ofA.TauCeti.Huber.PairOfDefinition.toCompletionLoc_denom_one_bijectiveandTauCeti.Huber.PairOfDefinition.toCompletionLocEquivDenomOne:A ≃+* A⟨T/1⟩. ForAcomplete and Hausdorff the structure mapA → A⟨T/1⟩is a ring isomorphism, for every localisation ofAaway from1. Its inverse is continuous (TauCeti.Huber.PairOfDefinition.continuous_toCompletionLocEquivDenomOne_symm), andTauCeti.Huber.PairOfDefinition.toCompletionLocHomeomorphDenomOneupgrades it to a homeomorphism, so the isomorphism is one of topological rings.
References #
- T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Proposition and Definition 5.51.
At the denominator 1 the standing hypothesis is automatic. Every b/1 is the image of
b, and the elements of I already lie in A₀ ⊆ D, so N = 1 works — for every numerator set
and every localisation away from 1.
The candidate ring of definition of the trivial presentation is A₀. The adjoined
fractions t/1 are the numerators themselves, and those were assumed to lie in A₀.
The basic neighbourhoods of the trivial presentation are those of A. With D = A₀ the
ideal J = I · D is I itself, so the n-th neighbourhood of zero is the image of Iⁿ.
The localisation topology at the denominator 1 is the topology of A.
The localisation's basic neighbourhoods are the ideal images for the pair obtained by adjoining
the power-bounded numerators to P. That pair still defines the topology of A, so the two ring
topologies are equal.
The uniformity of the trivial presentation is the uniformity of A. Both are the right
uniformity of one and the same topological group topology, by locTopology_denom_one and
IsUniformAddGroup.rightUniformSpace_eq.
This is what makes A⟨T/1⟩ equal to, and not merely isomorphic to, the Hausdorff completion
 of A: the completion is formed from the uniformity, and the two uniformities agree.
The structure map of the trivial presentation is bijective.
A ≃+* A⟨T/1⟩. For a complete Hausdorff A the structure map A → A⟨T/1⟩ is a ring
isomorphism.
The proof is the universal property, not the topology computation above. A is itself a complete
Hausdorff target through which the identity factors, and A⟨T/1⟩ admits at most one continuous
endomorphism over A, so the retraction obtained is a two-sided inverse of the structure map.
Equations
- P.toCompletionLocEquivDenomOne T hTpb S = { toFun := ⇑(P.toCompletionLoc T 1 S ⋯), invFun := ⇑⋯.choose, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
Instances For
The isomorphism is the structure map.
The inverse of toCompletionLocEquivDenomOne is continuous: it is the retraction, which the
universal property produced continuous.
A ≃ₜ A⟨T/1⟩. The ring isomorphism of
toCompletionLocEquivDenomOne is a homeomorphism for A's own topology: the structure map is
continuous by continuous_toCompletionLoc, and its inverse is the retraction, which the universal
property produced continuous.
Equations
- P.toCompletionLocHomeomorphDenomOne T hTpb S = { toFun := ⇑(P.toCompletionLoc T 1 S ⋯), invFun := ⇑⋯.choose, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
The homeomorphism is the structure map.