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.

• 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 α)

Equations

• instZeroCompletion = { zero := ↑α 0 }

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

Equations

• instNegCompletion = { neg := UniformSpace.Completion.map fun a => -a }

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

Equations

• instAddCompletion = { add := UniformSpace.Completion.map₂ fun x x_1 => x + x_1 }

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

Equations

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

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

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

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

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

Equations

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

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

Equations

• UniformSpace.Completion.instSubNegMonoidCompletion = let src := inferInstance; let src_1 := inferInstance; let src_2 := inferInstance; SubNegMonoid.mk fun x x_1 => x • x_1

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

Equations

• UniformSpace.Completion.addGroup = let src := inferInstance; AddGroup.mk (_ : ∀ (a : UniformSpace.Completion α), -a + a = 0)

instance UniformSpace.Completion.uniformAddGroup {α : Type u_3} [UniformSpace α] [AddGroup α] [UniformAddGroup α] : UniformAddGroup (UniformSpace.Completion α)

Equations

• @UniformSpace.Completion.uniformAddGroup = @UniformSpace.Completion.uniformAddGroup.proof_1

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

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

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

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) }

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

instance UniformSpace.Completion.instAddCommGroupCompletion {α : Type u_3} [UniformSpace α] [AddCommGroup α] [UniformAddGroup α] : AddCommGroup (UniformSpace.Completion α)

Equations

• UniformSpace.Completion.instAddCommGroupCompletion = let src := inferInstance; AddCommGroup.mk (_ : ∀ (a b : UniformSpace.Completion α), a + b = b + a)

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

Equations

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

def AddMonoidHom.extension {α : Type u_3} {β : Type u_4} [UniformSpace α] [AddGroup α] [UniformAddGroup α] [UniformSpace β] [AddGroup β] [UniformAddGroup β] [CompleteSpace β] [SeparatedSpace β] (f : α →+ β) (hf : Continuous ↑f) : UniformSpace.Completion α →+ β

Extension to the completion of a continuous group hom.

Equations

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

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

theorem AddMonoidHom.continuous_extension {α : Type u_3} {β : Type u_4} [UniformSpace α] [AddGroup α] [UniformAddGroup α] [UniformSpace β] [AddGroup β] [UniformAddGroup β] [CompleteSpace β] [SeparatedSpace β] (f : α →+ β) (hf : Continuous ↑f) : Continuous ↑(AddMonoidHom.extension f hf)

def AddMonoidHom.completion {α : Type u_3} {β : Type u_4} [UniformSpace α] [AddGroup α] [UniformAddGroup α] [UniformSpace β] [AddGroup β] [UniformAddGroup β] (f : α →+ β) (hf : Continuous ↑f) : UniformSpace.Completion α →+ UniformSpace.Completion β

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

Equations

• AddMonoidHom.completion f hf = AddMonoidHom.extension (AddMonoidHom.comp UniformSpace.Completion.toCompl f) (_ : Continuous (↑UniformSpace.Completion.toCompl ∘ fun x => ↑f x))

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

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) = ↑((fun x => β) 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) : AddMonoidHom.completion (f + g) (_ : Continuous fun x => ↑f x + ↑g x) = AddMonoidHom.completion f hf + AddMonoidHom.completion g hg