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

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

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

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

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

theorem UniformSpace.Completion.coe_zero {α : Type u_3} [UniformSpace α] [Zero α] : ↑0 = 0

@[simp]

theorem UniformSpace.Completion.coe_eq_zero_iff {α : Type u_3} [UniformSpace α] [Zero α] [T0Space α] {x : α} : ↑x = 0 ↔ x = 0

instance UniformSpace.Completion.instMulActionWithZeroOfUniformContinuousConstSMul {M : Type u_1} {α : Type u_3} [UniformSpace α] [MonoidWithZero M] [Zero α] [MulActionWithZero M α] [UniformContinuousConstSMul M α] : MulActionWithZero M (Completion α)

theorem UniformSpace.Completion.coe_neg {α : Type u_3} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] (a : α) : ↑(-a) = -↑a

theorem UniformSpace.Completion.coe_sub {α : Type u_3} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] (a b : α) : ↑(a - b) = ↑a - ↑b

theorem UniformSpace.Completion.coe_add {α : Type u_3} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] (a b : α) : ↑(a + b) = ↑a + ↑b

instance UniformSpace.Completion.instAddMonoid {α : Type u_3} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] : AddMonoid (Completion α)

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

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

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

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

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

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

@[simp]

theorem UniformSpace.Completion.toCompl_apply {α : Type u_3} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] (a✝ : α) : toCompl a✝ = ↑a✝

theorem UniformSpace.Completion.continuous_toCompl {α : Type u_3} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] : Continuous ⇑toCompl

theorem UniformSpace.Completion.isDenseInducing_toCompl (α : Type u_3) [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] : IsDenseInducing ⇑toCompl

instance UniformSpace.Completion.instAddCommGroup {α : Type u_3} [UniformSpace α] [AddCommGroup α] [IsUniformAddGroup α] : AddCommGroup (Completion α)

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

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.

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

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)

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.

theorem AddMonoidHom.continuous_completion {α : Type u_3} {β : Type u_4} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] [UniformSpace β] [AddGroup β] [IsUniformAddGroup β] (f : α →+ β) (hf : Continuous ⇑f) : Continuous ⇑(f.completion hf)

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)

theorem AddMonoidHom.completion_zero {α : Type u_3} {β : Type u_4} [UniformSpace α] [AddGroup α] [IsUniformAddGroup α] [UniformSpace β] [AddGroup β] [IsUniformAddGroup β] : completion 0 ⋯ = 0

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