# Documentation

Mathlib.Topology.Algebra.GroupCompletion

# 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 α] :
instance instNegCompletion {α : Type u_3} [] [Neg α] :
instance instSubCompletion {α : Type u_3} [] [Sub α] :
theorem UniformSpace.Completion.coe_zero {α : Type u_3} [] [Zero α] :
α 0 = 0
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.addGroup {α : Type u_3} [] [] [] :
@[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.

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.instModule {R : Type u_2} {α : Type u_3} [] [] [] [] [Module R α] :
def AddMonoidHom.extension {α : Type u_3} {β : Type u_4} [] [] [] [] [] [] [] [] (f : α →+ β) (hf : ) :

Extension to the completion of a continuous group hom.

Instances For
theorem AddMonoidHom.extension_coe {α : Type u_3} {β : Type u_4} [] [] [] [] [] [] [] [] (f : α →+ β) (hf : ) (a : α) :
↑() (α a) = f a
theorem AddMonoidHom.continuous_extension {α : Type u_3} {β : Type u_4} [] [] [] [] [] [] [] [] (f : α →+ β) (hf : ) :
def AddMonoidHom.completion {α : Type u_3} {β : Type u_4} [] [] [] [] [] [] (f : α →+ β) (hf : ) :

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

Instances For
theorem AddMonoidHom.continuous_completion {α : Type u_3} {β : Type u_4} [] [] [] [] [] [] (f : α →+ β) (hf : ) :
theorem AddMonoidHom.completion_coe {α : Type u_3} {β : Type u_4} [] [] [] [] [] [] (f : α →+ β) (hf : ) (a : α) :
↑() (α a) = ↑((fun x => β) a) (f a)
theorem AddMonoidHom.completion_zero {α : Type u_3} {β : Type u_4} [] [] [] [] [] [] :