# Completion of topological groups: #

This file 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.isUniformAddGroup` proves this group structure is compatible with the completed uniform structure. The compatibility condition is `IsUniformAddGroup`.

## 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`.

source
instance instZeroCompletion {α : Type u_3} [UniformSpace α] [Zero α] :
Zero (UniformSpace.Completion α)
Equations

- instZeroCompletion = { zero := ↑0 }

source
instance instNegCompletion {α : Type u_3} [UniformSpace α] [Neg α] :
Neg (UniformSpace.Completion α)
Equations

- instNegCompletion = { neg := UniformSpace.Completion.map fun (a : α) => -a }

source
instance instAddCompletion {α : Type u_3} [UniformSpace α] [Add α] :
Add (UniformSpace.Completion α)
Equations

- instAddCompletion = { add := UniformSpace.Completion.map₂ fun (x1 x2 : α) => x1 + x2 }

source
instance instSubCompletion {α : Type u_3} [UniformSpace α] [Sub α] :
Sub (UniformSpace.Completion α)
Equations

- instSubCompletion = { sub := UniformSpace.Completion.map₂ Sub.sub }

source
theorem UniformSpace.Completion.coe_zero {α : Type u_3} [UniformSpace α] [Zero α] :
↑0 = 0
source
@[simp]
theorem UniformSpace.Completion.coe_eq_zero_iff {α : Type u_3} [UniformSpace α] [Zero α] [T0Space α] {x : α} :
↑x = 0 ↔ x = 0
source
instance UniformSpace.Completion.instMulActionWithZeroOfUniformContinuousConstSMul {M : Type u_1} {α : Type u_3} [UniformSpace α] [MonoidWithZero M] [Zero α] [MulActionWithZero M α] [UniformContinuousConstSMul M α] :
MulActionWithZero M (Completion α)
Equations

- UniformSpace.Completion.instMulActionWithZeroOfUniformContinuousConstSMul = { toMulAction := inferInstance, smul_zero := ⋯, zero_smul := ⋯ }

source
theorem UniformSpace.Completion.coe_neg {α : Type u_3} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] (a : α) :
↑(-a) = -↑a
source
theorem UniformSpace.Completion.coe_sub {α : Type u_3} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] (a b : α) :
↑(a - b) = ↑a - ↑b
source
theorem UniformSpace.Completion.coe_add {α : Type u_3} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] (a b : α) :
↑(a + b) = ↑a + ↑b
source
instance UniformSpace.Completion.instAddMonoid {α : Type u_3} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] :
AddMonoid (Completion α)
Equations

- One or more equations did not get rendered due to their size.

source
instance UniformSpace.Completion.instSubNegMonoid {α : Type u_3} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] :
SubNegMonoid (Completion α)
Equations

- One or more equations did not get rendered due to their size.

source
instance UniformSpace.Completion.addGroup {α : Type u_3} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] :
AddGroup (Completion α)
Equations

- UniformSpace.Completion.addGroup = { toSubNegMonoid := inferInstance, neg_add_cancel := ⋯ }

source
instance UniformSpace.Completion.isUniformAddGroup {α : Type u_3} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] :
IsUniformAddGroup (Completion α)
source
instance UniformSpace.Completion.instDistribMulActionOfUniformContinuousConstSMul {α : Type u_3} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {M : Type u_5} [Monoid M] [DistribMulAction M α] [UniformContinuousConstSMul M α] :
DistribMulAction M (Completion α)
Equations

- UniformSpace.Completion.instDistribMulActionOfUniformContinuousConstSMul = { toMulAction := inferInstance, smul_zero := ⋯, smul_add := ⋯ }

source
def UniformSpace.Completion.toCompl {α : Type u_3} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] :
α →+ Completion α

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

Equations

- UniformSpace.Completion.toCompl = { toFun := UniformSpace.Completion.coe', map_zero' := ⋯, map_add' := ⋯ }

Instances For

source
@[simp]
theorem UniformSpace.Completion.toCompl_apply {α : Type u_3} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] (a✝ : α) :
toCompl a✝ = ↑a✝
source
theorem UniformSpace.Completion.continuous_toCompl {α : Type u_3} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] :
Continuous ⇑toCompl
source
theorem UniformSpace.Completion.isDenseInducing_toCompl (α : Type u_3) [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] :
IsDenseInducing ⇑toCompl
source
instance UniformSpace.Completion.instAddCommGroup {α : Type u_3} [UniformSpace α] [AddCommGroup α] [IsUniformAddGroup α] :
AddCommGroup (Completion α)
Equations

- UniformSpace.Completion.instAddCommGroup = { toAddGroup := inferInstance, add_comm := ⋯ }

source
instance UniformSpace.Completion.instModule {R : Type u_2} {α : Type u_3} [UniformSpace α] [AddCommGroup α] [IsUniformAddGroup α] [Semiring R] [Module R α] [UniformContinuousConstSMul R α] :
Module R (Completion α)
Equations

- UniformSpace.Completion.instModule = { toDistribMulAction := inferInstance, add_smul := ⋯, zero_smul := ⋯ }

source
def AddMonoidHom.extension {α : Type u_3} {β : Type u_4} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] [UniformSpace β] [AddGroup β] [IsUniformAddGroup β] [CompleteSpace β] [T0Space β] (f : α →+ β) (hf : Continuous ⇑f) :
UniformSpace.Completion α →+ β

Extension to the completion of a continuous group hom.

Equations

- f.extension hf = { toFun := UniformSpace.Completion.extension ⇑f, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source
theorem AddMonoidHom.extension_coe {α : Type u_3} {β : Type u_4} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] [UniformSpace β] [AddGroup β] [IsUniformAddGroup β] [CompleteSpace β] [T0Space β] (f : α →+ β) (hf : Continuous ⇑f) (a : α) :
(f.extension hf) ↑a = f a
source
theorem AddMonoidHom.continuous_extension {α : Type u_3} {β : Type u_4} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] [UniformSpace β] [AddGroup β] [IsUniformAddGroup β] [CompleteSpace β] [T0Space β] (f : α →+ β) (hf : Continuous ⇑f) :
Continuous ⇑(f.extension hf)
source
def AddMonoidHom.completion {α : Type u_3} {β : Type u_4} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] [UniformSpace β] [AddGroup β] [IsUniformAddGroup β] (f : α →+ β) (hf : Continuous ⇑f) :
UniformSpace.Completion α →+ UniformSpace.Completion β

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

Equations

- f.completion hf = (UniformSpace.Completion.toCompl.comp f).extension ⋯

Instances For

source
theorem AddMonoidHom.continuous_completion {α : Type u_3} {β : Type u_4} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] [UniformSpace β] [AddGroup β] [IsUniformAddGroup β] (f : α →+ β) (hf : Continuous ⇑f) :
Continuous ⇑(f.completion hf)
source
theorem AddMonoidHom.completion_coe {α : Type u_3} {β : Type u_4} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] [UniformSpace β] [AddGroup β] [IsUniformAddGroup β] (f : α →+ β) (hf : Continuous ⇑f) (a : α) :
(f.completion hf) ↑a = ↑(f a)
source
theorem AddMonoidHom.completion_zero {α : Type u_3} {β : Type u_4} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] [UniformSpace β] [AddGroup β] [IsUniformAddGroup β] :
completion 0 ⋯ = 0
source
theorem AddMonoidHom.completion_add {α : Type u_3} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] {γ : Type u_5} [AddCommGroup γ] [UniformSpace γ] [IsUniformAddGroup γ] (f g : α →+ γ) (hf : Continuous ⇑f) (hg : Continuous ⇑g) :
(f + g).completion ⋯ = f.completion hf + g.completion hg