mathlibdocumentation

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.

• add_monoid_hom.extension: extends a continuous group morphism from G to a complete separated group H to completion G.
• add_monoid_hom.completion: promotes a continuous group morphism from G to H into a continuous group morphism from completion G to completion H.
@[protected, instance]
def uniform_space.completion.has_zero {α : Type u_3} [has_zero α] :
Equations
@[protected, instance]
noncomputable def uniform_space.completion.has_neg {α : Type u_3} [has_neg α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
noncomputable def uniform_space.completion.has_sub {α : Type u_3} [has_sub α] :
Equations
@[norm_cast]
theorem uniform_space.completion.coe_zero {α : Type u_3} [has_zero α] :
0 = 0
@[protected, instance]
noncomputable def uniform_space.completion.mul_action_with_zero {M : Type u_1} {α : Type u_3} [has_zero α] [ α]  :
Equations
@[norm_cast]
theorem uniform_space.completion.coe_neg {α : Type u_3} [add_group α] (a : α) :
@[norm_cast]
theorem uniform_space.completion.coe_sub {α : Type u_3} [add_group α] (a b : α) :
(a - b) = a - b
@[norm_cast]
theorem uniform_space.completion.coe_add {α : Type u_3} [add_group α] (a b : α) :
(a + b) = a + b
@[protected, instance]
Equations
@[protected, instance]
noncomputable def uniform_space.completion.sub_neg_monoid {α : Type u_3} [add_group α]  :
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
noncomputable def uniform_space.completion.distrib_mul_action {α : Type u_3} [add_group α] {M : Type u_1} [monoid M] [ α]  :
Equations
@[simp]
theorem uniform_space.completion.to_compl_apply {α : Type u_3} [add_group α] (ᾰ : α) :
def uniform_space.completion.to_compl {α : Type u_3} [add_group α]  :

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

Equations
@[protected, instance]
noncomputable def uniform_space.completion.add_comm_group {α : Type u_3}  :
Equations
@[protected, instance]
noncomputable def uniform_space.completion.module {R : Type u_2} {α : Type u_3} [semiring R] [ α]  :
Equations
noncomputable def add_monoid_hom.extension {α : Type u_3} {β : Type u_4} [add_group α] [add_group β] (f : α →+ β) (hf : continuous f) :

Extension to the completion of a continuous group hom.

Equations
theorem add_monoid_hom.extension_coe {α : Type u_3} {β : Type u_4} [add_group α] [add_group β] (f : α →+ β) (hf : continuous f) (a : α) :
(f.extension hf) a = f a
@[continuity]
theorem add_monoid_hom.continuous_extension {α : Type u_3} {β : Type u_4} [add_group α] [add_group β] (f : α →+ β) (hf : continuous f) :
noncomputable def add_monoid_hom.completion {α : Type u_3} {β : Type u_4} [add_group α] [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_3} {β : Type u_4} [add_group α] [add_group β] (f : α →+ β) (hf : continuous f) :
theorem add_monoid_hom.completion_coe {α : Type u_3} {β : Type u_4} [add_group α] [add_group β] (f : α →+ β) (hf : continuous f) (a : α) :
(f.completion hf) a = (f a)