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
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 from
Rto a complete separated group
UniformSpace.Completion.mapRingHom: promotes a continuous ring morphism from
Sinto a continuous ring morphism from
TODO: Generalise the results here from the concrete
Completion to any
The completion extension as a ring morphism.
The completion map as a ring morphism.
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.
The dense inducing extension as a ring homomorphism.