The completion A⟨T/s⟩ #
The separated completion of Aₛ under locTopology is Wedhorn's A⟨T/s⟩. It is a Huber ring,
and the universal property of LocalizationTopology.UniversalProperty extends across it for
complete Hausdorff targets.
Main definitions #
locUniformSpace P T s S: the uniformitylocTopologydetermines, packaged so thatUniformSpace.Completion Scan be written down.toCompletionLoc P T s S: the structure mapA → A⟨T/s⟩.localizationUniform P T s S: the pairlocalization, transported to the topologylocUniformSpaceinduces, so that no statement aboutA⟨T/s⟩carries the transport.completionLocalization P T s S: the pair of definitionA⟨T/s⟩carries.
Main results #
locUniformSpace_toTopologicalSpace: the topologylocUniformSpaceinduces islocTopology. This is what a proof rewrites against, so no body in this file needs exposing.isUniformAddGroup_locUniformSpaceandisTopologicalRing_locUniformSpace: the two companions oflocUniformSpace. SincelocTopologyis not an instance, a statement aboutA⟨T/s⟩has to name its structures; these three declarations are what it names.localizationUniform_ringOfDefinitionandmem_localizationUniform_idealOfDefinition, withcompletionLocalization_ringOfDefinitionandmem_completionLocalization_idealOfDefinition: the completed pair's API, reducing to the concreteDandJ.continuous_toCompletionLoc: the structure mapA → A⟨T/s⟩is continuous.isHuberRing_completion_locTopology:A⟨T/s⟩is a Huber ring — the completed pair above is a pair of definition for it.isTateRing_completion_locTopology_of_isTopologicallyNilpotent: a topologically nilpotent denominator becomes a pseudouniformiser, so the completed localization is Tate.existsUnique_continuous_ringHom_completion_locTopology: the universal property, for complete Hausdorff targets.completion_locTopology_ringHom_ext_of_continuous: two continuous ring homomorphisms out ofA⟨T/s⟩agreeing onAare equal, so a map out ofA⟨T/s⟩is determined by its restriction toA. Unlike the universal property this needs no hypothesis onsor the fractions — those govern which maps exist, not when two agree — and its target need only be a semiring carrying a Hausdorff topology.eq_id_of_comp_toCompletionLoc_eq_selfandeq_comp_of_comp_toCompletionLoc_eq: two corollaries of the previous item, saying that a continuous map compatible with the structure maps is forced to be the identity, respectively the composite. These are not roadmap Layer 3.1's identity and composition laws for restriction maps: no restriction map is constructed here, and these are conditional uniqueness statements about whatever compatible maps happen to exist. They are what those laws will be proved from once the restriction maps themselves are built.
Provenance #
A⟨T/s⟩ and its universal property are this repository's own, built on the localisation topology
of LocalizationTopology.Basic, which is the AINTLIB port — see that module's Provenance section
for the source file and commit.
References #
- T. Wedhorn, Adic Spaces, Proposition and Definition 5.51, §5.6
Mathlib.Topology.Algebra.Valued.ValuationTopology,Valued.mk'— the model for the instance setup here. It layersIsTopologicalAddGroup.rightUniformSpaceandisUniformAddGroup_of_addCommGroupon a topology built from aRingSubgroupsBasis, passing that topology positionally because it is not an instance;locTopologyis in the same position.
The completion A⟨T/s⟩ #
The canonical uniformity on Aₛ, the one its topology determines.
locTopology is not an instance, so a consumer of the completion has to name the uniform structure
explicitly. This packages the construction, and it takes three declarations to state anything
about A⟨T/s⟩: locUniformSpace makes UniformSpace.Completion S well-formed,
isUniformAddGroup_locUniformSpace makes the completion an additive group, and
isTopologicalRing_locUniformSpace is what its ring structure is inferred from. The first two
alone do not suffice.
locUniformSpace_toTopologicalSpace is the characteristic property — the topology it induces is
locTopology — so the body is not exposed and a proof rewrites against that lemma instead.
It is the uniformity, not merely one compatible with the topology:
IsUniformAddGroup.rightUniformSpace_eq identifies it with any uniformity making Aₛ a uniform
additive group, so a consumer arriving with its own such structure rewrites rather than
transports.
Equations
- P.locUniformSpace T s S hden = IsTopologicalAddGroup.rightUniformSpace S
Instances For
The topology locUniformSpace induces is locTopology. This is the characteristic property
of the packaged uniformity: it lets a statement made at one be rewritten to the other.
Aₛ is a uniform additive group for locUniformSpace. The companion of locUniformSpace:
the two together are what UniformSpace.Completion S needs.
Aₛ is a topological ring for the topology locUniformSpace induces. Stated at that
topology rather than at locTopology, so that it applies where the packaged uniformity is in
scope.
Aₛ is a Huber ring for the topology locUniformSpace induces. The third companion of
locUniformSpace, alongside the two above. A consumer working at the uniformity can reach the
locTopology-stated form by transporting along locUniformSpace_toTopologicalSpace; this
restates it so that it does not have to, which is what makes powerBoundedSubring S convenient to
name there.
The image of a power-bounded element of A is power-bounded in Aₛ, at the uniformity's
topology. isPowerBounded_algebraMap_of_isPowerBounded states this at locTopology; this is the
same fact restated so that a consumer holding the uniformity need not transport along
locUniformSpace_toTopologicalSpace itself.
Each distinguished fraction t/s is power-bounded in Aₛ, at the uniformity's topology.
The locUniformSpace companion of isPowerBounded_divBy.
The structure map A → A⟨T/s⟩, the localisation map followed by the completion map. This
is the canonical ring homomorphism the universal property extends.
Equations
- P.toCompletionLoc T s S hden = UniformSpace.Completion.coeRingHom.comp (algebraMap A S)
Instances For
The structure map is the localisation map followed by the completion map. The body of
toCompletionLoc is not exported, so this is how a consumer computes with it.
The localisation pair localization, transported along locUniformSpace_toTopologicalSpace
to the topology the packaged uniformity induces.
localization is stated at locTopology and the completion is taken at locUniformSpace. The
two topologies are equal, but not syntactically, so the transport has to be named: naming it here
keeps the cast out of every statement about A⟨T/s⟩ below.
Equations
- P.localizationUniform T s S hden = ⋯ ▸ P.localization T s S hden
Instances For
The ring of definition of localizationUniform is D, as for localization: the transport
is along an equality of topologies and ringOfDefinition is a Subring S, which does not depend
on one. This is what makes the completed pair's API reduce to the concrete data.
Membership in the ideal of definition of localizationUniform is membership in J, as for
localization. With localizationUniform_ringOfDefinition this reduces the completed pair's
characteristic lemmas to the concrete D and J.
The pair of definition on A⟨T/s⟩, the completion of the pair localization carries on
Aₛ. This is the completed counterpart of localization, and it is what makes A⟨T/s⟩ Huber.
Its ring of definition and ideal of definition are characterised by
completionLocalization_ringOfDefinition and mem_completionLocalization_idealOfDefinition,
which are how a consumer computes with it — the body is not exposed.
Equations
- P.completionLocalization T s S hden = (P.localizationUniform T s S hden).completion
Instances For
The ring of definition of completionLocalization is the one PairOfDefinition.completion
supplies for the localisation pair: the closure of the image of D.
Membership in the ideal of definition of A⟨T/s⟩ is membership in J · D̂.
Stated as a membership characterisation rather than an equation because the type of
idealOfDefinition depends on ringOfDefinition, which the opaque body of completionLocalization
does not expose — the same shape as PairOfDefinition.mem_completion_idealOfDefinition, which
this delegates to.
The structure map A → A⟨T/s⟩ is continuous: it is the continuous localisation map
followed by the completion map.
A⟨T/s⟩ is a Huber ring: the separated completion of Aₛ under locTopology —
Wedhorn's A⟨T/s⟩ — carries a pair of definition.
The statement introduces locUniformSpace, isUniformAddGroup_locUniformSpace and
isTopologicalRing_locUniformSpace, because locTopology is not an instance and
UniformSpace.Completion S is not well-formed without them.
A topologically nilpotent denominator becomes a pseudouniformiser in the completed localization: it is inverted by localization and remains topologically nilpotent under the continuous structure map.
The completed localization at a topologically nilpotent denominator is a Tate ring.
Maps out of A⟨T/s⟩ are determined on A. Two continuous ring homomorphisms into a
semiring carrying a Hausdorff topology that agree after composing with the structure map
from A are equal.
This is TauCeti.completion_localization_ringHom_ext_of_continuous at Submonoid.powers s. The
bridge it crosses is the unexported body of toCompletionLoc, namely
UniformSpace.Completion.coeRingHom.comp (algebraMap A S): reassociating that composition turns
g.comp (toCompletionLoc …) into (g.comp coeRingHom).comp (algebraMap A S), which is the
hypothesis that lemma takes. Nothing is unfolded at the level of coercions — the argument stays
with bundled RingHoms throughout. Crossing the unexported body once here keeps it out of every
consumer.
The universal property of A⟨T/s⟩, for complete Hausdorff targets: a ring homomorphism
φ : A →+* B continuous at zero, with φ s a unit and each fraction φ t / φ s power-bounded,
extends to the completion in exactly one continuous way.
The hypotheses are those of existsUnique_continuous_ringHom_locTopology together with B
complete and separated, which is what an extension across the completion requires. As there, the
condition on the fractions is sufficient and is not claimed to be necessary.
The identity law. A continuous ring endomorphism of A⟨T/s⟩ fixing the structure map from
A is the identity, since the identity fixes it too.
As with the composition law below, this constructs no restriction map: it says that at most one continuous endomorphism is compatible with the structure map, and names it.
The composition law. If g carries the structure map of A⟨T/s⟩ to a map φ', and h
carries φ' on to φ'', then any continuous k carrying the structure map to φ'' is h.comp g.
Only the source is a completed localisation — that is where extensionality is applied — so the
middle and target objects are arbitrary topological semirings, with φ' and φ'' the ring
homomorphisms out of A they are equipped with. At the roadmap's intended instance these are the
completed localisations of two further presentations and their structure maps, but nothing here
requires that, and no restriction map is constructed: this is a uniqueness statement about maps
compatible with the structure maps, not Layer 3.1's composition law for restriction maps.