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
  • One or more equations did not get rendered due to their size.
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
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
Equations
  • One or more equations did not get rendered due to their size.
@[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 = { toZeroHom := { toFun := α, map_zero' := (_ : α 0 = 0) }, map_add' := (_ : ∀ (a b : α), α (a + b) = α a + α b) }
Instances For
    theorem UniformSpace.Completion.continuous_toCompl {α : Type u_3} [UniformSpace α] [AddGroup α] [UniformAddGroup α] :
    Continuous UniformSpace.Completion.toCompl
    theorem UniformSpace.Completion.denseInducing_toCompl (α : Type u_3) [UniformSpace α] [AddGroup α] [UniformAddGroup α] :
    DenseInducing UniformSpace.Completion.toCompl
    Equations
    Equations
    • One or more equations did not get rendered due to their size.

    Extension to the completion of a continuous group hom.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem AddMonoidHom.extension_coe {α : Type u_3} {β : Type u_4} [UniformSpace α] [AddGroup α] [UniformAddGroup α] [UniformSpace β] [AddGroup β] [UniformAddGroup β] [CompleteSpace β] [SeparatedSpace β] (f : α →+ β) (hf : Continuous f) (a : α) :
      (AddMonoidHom.extension f hf) (α a) = f a

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

      Equations
      Instances For
        theorem AddMonoidHom.completion_coe {α : Type u_3} {β : Type u_4} [UniformSpace α] [AddGroup α] [UniformAddGroup α] [UniformSpace β] [AddGroup β] [UniformAddGroup β] (f : α →+ β) (hf : Continuous f) (a : α) :
        (AddMonoidHom.completion f hf) (α a) = β (f a)
        theorem AddMonoidHom.completion_zero {α : Type u_3} {β : Type u_4} [UniformSpace α] [AddGroup α] [UniformAddGroup α] [UniformSpace β] [AddGroup β] [UniformAddGroup β] :
        AddMonoidHom.completion 0 (_ : Continuous fun (x : α) => AddZeroClass.toZero.1) = 0
        theorem AddMonoidHom.completion_add {α : Type u_3} [UniformSpace α] [AddGroup α] [UniformAddGroup α] {γ : Type u_5} [AddCommGroup γ] [UniformSpace γ] [UniformAddGroup γ] (f : α →+ γ) (g : α →+ γ) (hf : Continuous f) (hg : Continuous g) :