Completion of topological rings: #
This files endows the completion of a topological ring with a ring structure.
More precisely the instance UniformSpace.Completion.ring
builds a ring structure
on the completion of a ring endowed with a compatible uniform structure in the sense of
UniformAddGroup
. There is also a commutative version when the original ring is commutative.
Moreover, if a topological ring is an algebra over a commutative semiring, then so is its
UniformSpace.Completion
.
The last part of the file builds a ring structure on the biggest separated quotient of a ring.
Main declarations: #
Beyond the instances explained above (that don't have to be explicitly invoked), the main constructions deal with continuous ring morphisms.
UniformSpace.Completion.extensionHom
: extends a continuous ring morphism fromR
to a complete separated groupS
toCompletion R
.UniformSpace.Completion.mapRingHom
: promotes a continuous ring morphism fromR
toS
into a continuous ring morphism fromCompletion R
toCompletion S
.
TODO: Generalise the results here from the concrete Completion
to any AbstractCompletion
.
The map from a uniform ring to its completion, as a ring homomorphism.
Instances For
The completion extension as a ring morphism.
Instances For
The completion map as a ring morphism.
Instances For
A shortcut instance for the common case
Given a topological ring α
equipped with a uniform structure that makes subtraction uniformly
continuous, get an equivalence between the separated quotient of α
and the quotient ring
corresponding to the closure of zero.
Instances For
The dense inducing extension as a ring homomorphism.