# mathlibdocumentation

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.

• uniform_space.completion.extension_hom: extends a continuous ring morphism from R to a complete separated group S to completion R.
• uniform_space.completion.map_ring_hom : promotes a continuous ring morphism from R to S into a continuous ring morphism from completion R to completion S.

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

@[protected, instance]
def uniform_space.completion.has_one (α : Type u_1) [ring α]  :
Equations
@[protected, instance]
noncomputable def uniform_space.completion.has_mul (α : Type u_1) [ring α]  :
Equations
@[norm_cast]
theorem uniform_space.completion.coe_one (α : Type u_1) [ring α]  :
1 = 1
@[norm_cast]
theorem uniform_space.completion.coe_mul {α : Type u_1} [ring α] (a b : α) :
(a * b) = a * b
theorem uniform_space.completion.continuous_mul {α : Type u_1} [ring α]  :
continuous (λ (p : , p.fst * p.snd)
theorem uniform_space.completion.continuous.mul {α : Type u_1} [ring α] {β : Type u_2} {f g : β → } (hf : continuous f) (hg : continuous g) :
continuous (λ (b : β), f b * g b)
@[protected, instance]
noncomputable def uniform_space.completion.ring {α : Type u_1} [ring α]  :
Equations
def uniform_space.completion.coe_ring_hom {α : Type u_1} [ring α]  :

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 α] {β : Type u} [ring β] (f : α →+* β) (hf : continuous f)  :

The completion extension as a ring morphism.

Equations
@[protected, instance]
def uniform_space.completion.top_ring_compl {α : Type u_1} [ring α]  :
noncomputable def uniform_space.completion.map_ring_hom {α : Type u_1} [ring α] {β : Type u} [ring β] (f : α →+* β) (hf : continuous f) :

The completion map as a ring morphism.

Equations
@[simp]
theorem uniform_space.completion.map_smul_eq_mul_coe (A : Type u_2) [ring A] (R : Type u_3) [ A] (r : R) :
@[protected, instance]
noncomputable def uniform_space.completion.algebra (A : Type u_2) [ring A] (R : Type u_3) [ A]  :
Equations
theorem uniform_space.completion.algebra_map_def (A : Type u_2) [ring A] (R : Type u_3) [ A] (r : R) :
r = ( A) r)
@[protected, instance]
noncomputable def uniform_space.completion.comm_ring (R : Type u_2) [comm_ring R]  :
Equations
@[protected, instance]
noncomputable def uniform_space.completion.algebra' (R : Type u_2) [comm_ring R]  :

A shortcut instance for the common case

Equations
theorem uniform_space.ring_sep_rel (α : Type u_1) [comm_ring α]  :
theorem uniform_space.ring_sep_quot (α : Type u) [r : comm_ring α]  :
def uniform_space.sep_quot_equiv_ring_quot (α : Type u_1) [r : comm_ring α]  :

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]
def uniform_space.comm_ring {α : Type u_1} [comm_ring α]  :
Equations
@[protected, instance]
def uniform_space.topological_ring {α : Type u_1} [comm_ring α]  :