mathlib documentation

topology.algebra.uniform_ring

Completion of topological rings: #

This files endows the completion of a topological ring with a ring structure. More precisely the instance uniform_space.completion.ring builds a ring structure on the completion of a ring endowed with a compatible uniform structure in the sense of uniform_add_group. 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 uniform_space.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.

TODO: Generalise the results here from the concrete completion to any abstract_completion.

@[protected, instance]
Equations
@[norm_cast]
theorem uniform_space.completion.coe_one (α : Type u_1) [ring α] [uniform_space α] :
1 = 1
@[norm_cast]
theorem uniform_space.completion.coe_mul {α : Type u_1} [ring α] [uniform_space α] [topological_ring α] (a b : α) :
(a * b) = a * b
theorem uniform_space.completion.continuous.mul {α : Type u_1} [ring α] [uniform_space α] [topological_ring α] [uniform_add_group α] {β : Type u_2} [topological_space β] {f g : β → uniform_space.completion α} (hf : continuous f) (hg : continuous g) :
continuous (λ (b : β), f b * g b)
@[protected, instance]
Equations

The map from a uniform ring to its completion, as a ring homomorphism.

Equations
noncomputable def uniform_space.completion.extension_hom {α : Type u_1} [ring α] [uniform_space α] [topological_ring α] [uniform_add_group α] {β : Type u} [uniform_space β] [ring β] [uniform_add_group β] [topological_ring β] (f : α →+* β) (hf : continuous f) [complete_space β] [separated_space β] :

The completion extension as a ring morphism.

Equations
@[protected, instance]

A shortcut instance for the common case

Equations

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.

Equations
@[protected, instance]
Equations