# 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 from R to a complete separated group S to Completion R.
• UniformSpace.Completion.mapRingHom : 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 AbstractCompletion.

instance UniformSpace.Completion.one (α : Type u_1) [Ring α] [] :
Equations
• = { one := α 1 }
instance UniformSpace.Completion.mul (α : Type u_1) [Ring α] [] :
Equations
theorem UniformSpace.Completion.coe_one (α : Type u_1) [Ring α] [] :
α 1 = 1
theorem UniformSpace.Completion.coe_mul {α : Type u_1} [Ring α] [] [] (a : α) (b : α) :
α (a * b) = α a * α b
theorem UniformSpace.Completion.continuous_mul {α : Type u_1} [Ring α] [] [] [] :
Continuous fun (p : ) => p.1 * p.2
theorem UniformSpace.Completion.Continuous.mul {α : Type u_1} [Ring α] [] [] [] {β : Type u_2} [] {f : } {g : } (hf : ) (hg : ) :
Continuous fun (b : β) => f b * g b
instance UniformSpace.Completion.ring {α : Type u_1} [Ring α] [] [] [] :
Equations
• One or more equations did not get rendered due to their size.
def UniformSpace.Completion.coeRingHom {α : Type u_1} [Ring α] [] [] [] :

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

Equations
• UniformSpace.Completion.coeRingHom = { toMonoidHom := { toOneHom := { toFun := α, map_one' := }, map_mul' := }, map_zero' := , map_add' := }
Instances For
theorem UniformSpace.Completion.continuous_coeRingHom {α : Type u_1} [Ring α] [] [] [] :
Continuous UniformSpace.Completion.coeRingHom
def UniformSpace.Completion.extensionHom {α : Type u_1} [Ring α] [] [] [] {β : Type u} [] [Ring β] [] [] (f : α →+* β) (hf : ) [] [] :

The completion extension as a ring morphism.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance UniformSpace.Completion.topologicalRing {α : Type u_1} [Ring α] [] [] [] :
Equations
• =
def UniformSpace.Completion.mapRingHom {α : Type u_1} [Ring α] [] [] [] {β : Type u} [] [Ring β] [] [] (f : α →+* β) (hf : ) :

The completion map as a ring morphism.

Equations
Instances For
@[simp]
theorem UniformSpace.Completion.map_smul_eq_mul_coe (A : Type u_2) [Ring A] [] [] [] (R : Type u_3) [] [Algebra R A] (r : R) :
(UniformSpace.Completion.map fun (x : A) => r x) = fun (x : ) => A (() r) * x
instance UniformSpace.Completion.algebra (A : Type u_2) [Ring A] [] [] [] (R : Type u_3) [] [Algebra R A] :
Equations
theorem UniformSpace.Completion.algebraMap_def (A : Type u_2) [Ring A] [] [] [] (R : Type u_3) [] [Algebra R A] (r : R) :
() r = A (() r)
instance UniformSpace.Completion.commRing (R : Type u_2) [] [] [] [] :
Equations
• = let __src := UniformSpace.Completion.ring;
instance UniformSpace.Completion.algebra' (R : Type u_2) [] [] [] [] :

A shortcut instance for the common case

Equations
• = inferInstance
theorem UniformSpace.inseparableSetoid_ring (α : Type u_2) [] [] [] :
@[deprecated UniformSpace.inseparableSetoid_ring]
theorem UniformSpace.ring_sep_rel (α : Type u_2) [] [] [] :

Alias of UniformSpace.inseparableSetoid_ring.

@[deprecated UniformSpace.inseparableSetoid_ring]
theorem UniformSpace.ring_sep_quot (α : Type u) [r : ] [] [] :

Given a topological ring α equipped with a uniform structure that makes subtraction uniformly continuous, get an homeomorphism between the separated quotient of α and the quotient ring corresponding to the closure of zero.

Equations
• = { toEquiv := , continuous_toFun := , continuous_invFun := }
Instances For
instance UniformSpace.commRing {α : Type u_1} [] [] [] :
Equations
• UniformSpace.commRing =

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
Instances For
instance UniformSpace.topologicalRing {α : Type u_1} [] [] [] :
Equations
• =
noncomputable def DenseInducing.extendRingHom {α : Type u_1} [] [] {β : Type u_2} [] [] {γ : Type u_3} [] [] [] [] {i : α →+* β} {f : α →+* γ} (ue : ) (dr : ) (hf : ) :
β →+* γ

The dense inducing extension as a ring homomorphism.

Equations
• = { toMonoidHom := { toOneHom := { toFun := , map_one' := }, map_mul' := }, map_zero' := , map_add' := }
Instances For