mathlib documentation

topology.algebra.group_completion

theorem uniform_space.completion.coe_zero {α : Type u} [uniform_space α] [has_zero α] :
0 = 0
theorem uniform_space.completion.coe_neg {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] (a : α) :
theorem uniform_space.completion.coe_sub {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] (a b : α) :
(a - b) = a - b
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
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
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) :

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

Equations
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