Documentation

Mathlib.Topology.Algebra.GroupCompletion

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.uniformAddGroup proves this group structure is compatible with the completed uniform structure. The compatibility condition is UniformAddGroup.

Main declarations: #

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

Equations
  • instZeroCompletion = { zero := α 0 }
Equations
Equations
Equations
theorem UniformSpace.Completion.coe_zero {α : Type u_3} [UniformSpace α] [Zero α] :
α 0 = 0
Equations
theorem UniformSpace.Completion.coe_neg {α : Type u_3} [UniformSpace α] [AddGroup α] [UniformAddGroup α] (a : α) :
α (-a) = -α a
theorem UniformSpace.Completion.coe_sub {α : Type u_3} [UniformSpace α] [AddGroup α] [UniformAddGroup α] (a : α) (b : α) :
α (a - b) = α a - α b
theorem UniformSpace.Completion.coe_add {α : Type u_3} [UniformSpace α] [AddGroup α] [UniformAddGroup α] (a : α) (b : α) :
α (a + b) = α a + α b
Equations
Equations
Equations
Equations
  • UniformSpace.Completion.instDistribMulActionOfUniformContinuousConstSMul = DistribMulAction.mk
@[simp]
theorem UniformSpace.Completion.toCompl_apply {α : Type u_3} [UniformSpace α] [AddGroup α] [UniformAddGroup α] :
∀ (a : α), UniformSpace.Completion.toCompl a = α a

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

Equations
  • UniformSpace.Completion.toCompl = { toFun := α, map_zero' := , map_add' := }
Instances For
    theorem UniformSpace.Completion.continuous_toCompl {α : Type u_3} [UniformSpace α] [AddGroup α] [UniformAddGroup α] :
    Continuous UniformSpace.Completion.toCompl
    theorem UniformSpace.Completion.isDenseInducing_toCompl (α : Type u_3) [UniformSpace α] [AddGroup α] [UniformAddGroup α] :
    IsDenseInducing UniformSpace.Completion.toCompl
    Equations
    Equations
    • UniformSpace.Completion.instModule = Module.mk
    def AddMonoidHom.extension {α : Type u_3} {β : Type u_4} [UniformSpace α] [AddGroup α] [UniformAddGroup α] [UniformSpace β] [AddGroup β] [UniformAddGroup β] [CompleteSpace β] [T0Space β] (f : α →+ β) (hf : Continuous f) :

    Extension to the completion of a continuous group hom.

    Equations
    Instances For
      theorem AddMonoidHom.extension_coe {α : Type u_3} {β : Type u_4} [UniformSpace α] [AddGroup α] [UniformAddGroup α] [UniformSpace β] [AddGroup β] [UniformAddGroup β] [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 α] [UniformAddGroup α] [UniformSpace β] [AddGroup β] [UniformAddGroup β] [CompleteSpace β] [T0Space β] (f : α →+ β) (hf : Continuous f) :
      Continuous (f.extension hf)

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

      Equations
      • f.completion hf = (UniformSpace.Completion.toCompl.comp f).extension
      Instances For
        theorem AddMonoidHom.continuous_completion {α : Type u_3} {β : Type u_4} [UniformSpace α] [AddGroup α] [UniformAddGroup α] [UniformSpace β] [AddGroup β] [UniformAddGroup β] (f : α →+ β) (hf : Continuous f) :
        Continuous (f.completion hf)
        theorem AddMonoidHom.completion_coe {α : Type u_3} {β : Type u_4} [UniformSpace α] [AddGroup α] [UniformAddGroup α] [UniformSpace β] [AddGroup β] [UniformAddGroup β] (f : α →+ β) (hf : Continuous f) (a : α) :
        (f.completion hf) (α a) = β (f a)
        theorem AddMonoidHom.completion_add {α : Type u_3} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {γ : Type u_5} [AddCommGroup γ] [UniformSpace γ] [UniformAddGroup γ] (f : α →+ γ) (g : α →+ γ) (hf : Continuous f) (hg : Continuous g) :
        (f + g).completion = f.completion hf + g.completion hg