# Completion of topological groups: #

This files endows the completion of a topological abelian group with a group structure. More precisely the instance UniformSpace.Completion.addGroup builds an abelian group structure on the completion of an abelian group endowed with a compatible uniform structure. Then the instance UniformSpace.Completion.uniformAddGroup proves this group structure is compatible with the completed uniform structure. The compatibility condition is UniformAddGroup.

## Main declarations: #

Beyond the instances explained above (that don't have to be explicitly invoked), the main constructions deal with continuous group morphisms.

• AddMonoidHom.extension: extends a continuous group morphism from G to a complete separated group H to Completion G.
• AddMonoidHom.completion: promotes a continuous group morphism from G to H into a continuous group morphism from Completion G to Completion H.
instance instZeroCompletion {α : Type u_3} [] [Zero α] :
Equations
• instZeroCompletion = { zero := α 0 }
instance instNegCompletion {α : Type u_3} [] [Neg α] :
Equations
Equations
instance instSubCompletion {α : Type u_3} [] [Sub α] :
Equations
theorem UniformSpace.Completion.coe_zero {α : Type u_3} [] [Zero α] :
α 0 = 0
Equations
• UniformSpace.Completion.instMulActionWithZeroOfUniformContinuousConstSMul = let __src := inferInstance;
theorem UniformSpace.Completion.coe_neg {α : Type u_3} [] [] [] (a : α) :
α (-a) = -α a
theorem UniformSpace.Completion.coe_sub {α : Type u_3} [] [] [] (a : α) (b : α) :
α (a - b) = α a - α b
theorem UniformSpace.Completion.coe_add {α : Type u_3} [] [] [] (a : α) (b : α) :
α (a + b) = α a + α b
instance UniformSpace.Completion.instAddMonoid {α : Type u_3} [] [] [] :
Equations
• UniformSpace.Completion.instAddMonoid = let __src := inferInstance; let __src_1 := inferInstance; AddMonoid.mk (fun (x : ) (x_1 : ) => x x_1)
instance UniformSpace.Completion.instSubNegMonoid {α : Type u_3} [] [] [] :
Equations
• One or more equations did not get rendered due to their size.
instance UniformSpace.Completion.addGroup {α : Type u_3} [] [] [] :
Equations
• UniformSpace.Completion.addGroup = let __src := inferInstance;
instance UniformSpace.Completion.uniformAddGroup {α : Type u_3} [] [] [] :
Equations
• =
Equations
• UniformSpace.Completion.instDistribMulActionOfUniformContinuousConstSMul = let __src := inferInstance;
@[simp]
theorem UniformSpace.Completion.toCompl_apply {α : Type u_3} [] [] [] :
∀ (a : α), UniformSpace.Completion.toCompl a = α a
def UniformSpace.Completion.toCompl {α : Type u_3} [] [] [] :

The map from a group to its completion as a group hom.

Equations
• UniformSpace.Completion.toCompl = { toFun := α, map_zero' := , map_add' := }
Instances For
theorem UniformSpace.Completion.continuous_toCompl {α : Type u_3} [] [] [] :
Continuous UniformSpace.Completion.toCompl
theorem UniformSpace.Completion.denseInducing_toCompl (α : Type u_3) [] [] [] :
DenseInducing UniformSpace.Completion.toCompl
instance UniformSpace.Completion.instAddCommGroup {α : Type u_3} [] [] [] :
Equations
• UniformSpace.Completion.instAddCommGroup = let __src := inferInstance;
instance UniformSpace.Completion.instModule {R : Type u_2} {α : Type u_3} [] [] [] [] [Module R α] :
Equations
• UniformSpace.Completion.instModule = let __src := inferInstance; let __src_1 := inferInstance;
def AddMonoidHom.extension {α : Type u_3} {β : Type u_4} [] [] [] [] [] [] [] [] (f : α →+ β) (hf : ) :

Extension to the completion of a continuous group hom.

Equations
• f.extension hf = let_fun hf := ; { toFun := , map_zero' := , map_add' := }
Instances For
theorem AddMonoidHom.extension_coe {α : Type u_3} {β : Type u_4} [] [] [] [] [] [] [] [] (f : α →+ β) (hf : ) (a : α) :
(f.extension hf) (α a) = f a
theorem AddMonoidHom.continuous_extension {α : Type u_3} {β : Type u_4} [] [] [] [] [] [] [] [] (f : α →+ β) (hf : ) :
Continuous (f.extension hf)
def AddMonoidHom.completion {α : Type u_3} {β : Type u_4} [] [] [] [] [] [] (f : α →+ β) (hf : ) :

Completion of a continuous group hom, as a group hom.

Equations
• f.completion hf = (UniformSpace.Completion.toCompl.comp f).extension
Instances For
theorem AddMonoidHom.continuous_completion {α : Type u_3} {β : Type u_4} [] [] [] [] [] [] (f : α →+ β) (hf : ) :
Continuous (f.completion hf)
theorem AddMonoidHom.completion_coe {α : Type u_3} {β : Type u_4} [] [] [] [] [] [] (f : α →+ β) (hf : ) (a : α) :
(f.completion hf) (α a) = β (f a)
theorem AddMonoidHom.completion_zero {α : Type u_3} {β : Type u_4} [] [] [] [] [] [] :
theorem AddMonoidHom.completion_add {α : Type u_3} [] [] [] {γ : Type u_5} [] [] [] (f : α →+ γ) (g : α →+ γ) (hf : ) (hg : ) :
(f + g).completion = f.completion hf + g.completion hg