mathlib documentation

topology.algebra.group_completion

Completion of topological groups: #

This files endows the completion of a topological abelian group with a group structure. More precisely the instance uniform_space.completion.add_group builds an abelian group structure on the completion of an abelian group endowed with a compatible uniform structure. Then the instance uniform_space.completion.uniform_add_group proves this group structure is compatible with the completed uniform structure. The compatibility condition is uniform_add_group.

Main declarations: #

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

@[protected, instance]
noncomputable def uniform_space.completion.has_neg {α : Type u} [uniform_space α] [has_neg α] :
Equations
@[norm_cast]
theorem uniform_space.completion.coe_zero {α : Type u} [uniform_space α] [has_zero α] :
0 = 0
@[norm_cast]
theorem uniform_space.completion.coe_neg {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] (a : α) :
@[norm_cast]
theorem uniform_space.completion.coe_sub {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] (a b : α) :
(a - b) = a - b
@[norm_cast]
theorem uniform_space.completion.coe_add {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] (a b : α) :
(a + b) = a + b

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

Equations
noncomputable def add_monoid_hom.extension {α : Type u_1} {β : Type u_2} [uniform_space α] [add_group α] [uniform_add_group α] [uniform_space β] [add_group β] [uniform_add_group β] [complete_space β] [separated_space β] (f : α →+ β) (hf : continuous f) :

Extension to the completion of a continuous group hom.

Equations
theorem add_monoid_hom.extension_coe {α : Type u_1} {β : Type u_2} [uniform_space α] [add_group α] [uniform_add_group α] [uniform_space β] [add_group β] [uniform_add_group β] [complete_space β] [separated_space β] (f : α →+ β) (hf : continuous f) (a : α) :
(f.extension hf) a = f a
@[continuity]
theorem add_monoid_hom.continuous_extension {α : Type u_1} {β : Type u_2} [uniform_space α] [add_group α] [uniform_add_group α] [uniform_space β] [add_group β] [uniform_add_group β] [complete_space β] [separated_space β] (f : α →+ β) (hf : continuous f) :
noncomputable def add_monoid_hom.completion {α : Type u_1} {β : Type u_2} [uniform_space α] [add_group α] [uniform_add_group α] [uniform_space β] [add_group β] [uniform_add_group β] (f : α →+ β) (hf : continuous f) :

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

Equations
@[continuity]
theorem add_monoid_hom.continuous_completion {α : Type u_1} {β : Type u_2} [uniform_space α] [add_group α] [uniform_add_group α] [uniform_space β] [add_group β] [uniform_add_group β] (f : α →+ β) (hf : continuous f) :
theorem add_monoid_hom.completion_coe {α : Type u_1} {β : Type u_2} [uniform_space α] [add_group α] [uniform_add_group α] [uniform_space β] [add_group β] [uniform_add_group β] (f : α →+ β) (hf : continuous f) (a : α) :
(f.completion hf) a = (f a)
theorem add_monoid_hom.completion_add {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] {γ : Type u_2} [add_comm_group γ] [uniform_space γ] [uniform_add_group γ] (f g : α →+ γ) (hf : continuous f) (hg : continuous g) :
(f + g).completion _ = f.completion hf + g.completion hg