mathlib3 documentation

topology.algebra.group_completion

Completion of topological groups: #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This files endows the completion of a topological abelian group with a group structure. More precisely the instance uniform_space.completion.add_group builds an abelian group structure on the completion of an abelian group endowed with a compatible uniform structure. Then the instance uniform_space.completion.uniform_add_group proves this group structure is compatible with the completed uniform structure. The compatibility condition is uniform_add_group.

Main declarations: #

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

add_monoid_hom.extension: extends a continuous group morphism from G to a complete separated group H to completion G.
add_monoid_hom.completion: promotes a continuous group morphism from G to H into a continuous group morphism from completion G to completion H.

@[protected, instance]

def uniform_space.completion.has_zero {α : Type u_3} [uniform_space α] [has_zero α] :

has_zero (uniform_space.completion α)

Equations

uniform_space.completion.has_zero = {zero := ↑0}

@[protected, instance]

noncomputable def uniform_space.completion.has_neg {α : Type u_3} [uniform_space α] [has_neg α] :

has_neg (uniform_space.completion α)

Equations

uniform_space.completion.has_neg = {neg := uniform_space.completion.map (λ (a : α), -a)}

@[protected, instance]

noncomputable def uniform_space.completion.has_add {α : Type u_3} [uniform_space α] [has_add α] :

has_add (uniform_space.completion α)

Equations

uniform_space.completion.has_add = {add := uniform_space.completion.map₂ has_add.add}

@[protected, instance]

noncomputable def uniform_space.completion.has_sub {α : Type u_3} [uniform_space α] [has_sub α] :

has_sub (uniform_space.completion α)

Equations

uniform_space.completion.has_sub = {sub := uniform_space.completion.map₂ has_sub.sub}

@[norm_cast]

theorem uniform_space.completion.coe_zero {α : Type u_3} [uniform_space α] [has_zero α] :

↑0 = 0

@[protected, instance]

noncomputable def uniform_space.completion.mul_action_with_zero {M : Type u_1} {α : Type u_3} [uniform_space α] [monoid_with_zero M] [has_zero α] [mul_action_with_zero M α] [has_uniform_continuous_const_smul M α] :

mul_action_with_zero M (uniform_space.completion α)

Equations

uniform_space.completion.mul_action_with_zero = {to_mul_action := {to_has_smul := {smul := has_smul.smul (uniform_space.completion.has_smul M α)}, one_smul := _, mul_smul := _}, smul_zero := _, zero_smul := _}

@[norm_cast]

theorem uniform_space.completion.coe_neg {α : Type u_3} [uniform_space α] [add_group α] [uniform_add_group α] (a : α) :

@[norm_cast]

theorem uniform_space.completion.coe_sub {α : Type u_3} [uniform_space α] [add_group α] [uniform_add_group α] (a b : α) :

↑(a - b) = ↑a - ↑b

@[norm_cast]

theorem uniform_space.completion.coe_add {α : Type u_3} [uniform_space α] [add_group α] [uniform_add_group α] (a b : α) :

↑(a + b) = ↑a + ↑b

@[protected, instance]

noncomputable def uniform_space.completion.add_monoid {α : Type u_3} [uniform_space α] [add_group α] [uniform_add_group α] :

add_monoid (uniform_space.completion α)

Equations

uniform_space.completion.add_monoid = {add := has_add.add uniform_space.completion.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := has_smul.smul (uniform_space.completion.has_smul ℕ α), nsmul_zero' := _, nsmul_succ' := _}

@[protected, instance]

noncomputable def uniform_space.completion.sub_neg_monoid {α : Type u_3} [uniform_space α] [add_group α] [uniform_add_group α] :

sub_neg_monoid (uniform_space.completion α)

Equations

uniform_space.completion.sub_neg_monoid = {add := add_monoid.add uniform_space.completion.add_monoid, add_assoc := _, zero := add_monoid.zero uniform_space.completion.add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul uniform_space.completion.add_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg uniform_space.completion.has_neg, sub := has_sub.sub uniform_space.completion.has_sub, sub_eq_add_neg := _, zsmul := has_smul.smul (uniform_space.completion.has_smul ℤ α), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _}

@[protected, instance]

noncomputable def uniform_space.completion.add_group {α : Type u_3} [uniform_space α] [add_group α] [uniform_add_group α] :

add_group (uniform_space.completion α)

Equations

@[protected, instance]

def uniform_space.completion.uniform_add_group {α : Type u_3} [uniform_space α] [add_group α] [uniform_add_group α] :

uniform_add_group (uniform_space.completion α)

@[protected, instance]

noncomputable def uniform_space.completion.distrib_mul_action {α : Type u_3} [uniform_space α] [add_group α] [uniform_add_group α] {M : Type u_1} [monoid M] [distrib_mul_action M α] [has_uniform_continuous_const_smul M α] :

distrib_mul_action M (uniform_space.completion α)

Equations

uniform_space.completion.distrib_mul_action = {to_mul_action := {to_has_smul := {smul := has_smul.smul (uniform_space.completion.has_smul M α)}, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}

@[simp]

theorem uniform_space.completion.to_compl_apply {α : Type u_3} [uniform_space α] [add_group α] [uniform_add_group α] (ᾰ : α) :

⇑uniform_space.completion.to_compl ᾰ = ↑ᾰ

def uniform_space.completion.to_compl {α : Type u_3} [uniform_space α] [add_group α] [uniform_add_group α] :

α →+ uniform_space.completion α

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

Equations

uniform_space.completion.to_compl = {to_fun := coe coe_to_lift, map_zero' := _, map_add' := _}

theorem uniform_space.completion.continuous_to_compl {α : Type u_3} [uniform_space α] [add_group α] [uniform_add_group α] :

continuous ⇑uniform_space.completion.to_compl

theorem uniform_space.completion.dense_inducing_to_compl (α : Type u_3) [uniform_space α] [add_group α] [uniform_add_group α] :

dense_inducing ⇑uniform_space.completion.to_compl

@[protected, instance]

noncomputable def uniform_space.completion.add_comm_group {α : Type u_3} [uniform_space α] [add_comm_group α] [uniform_add_group α] :

add_comm_group (uniform_space.completion α)

Equations

uniform_space.completion.add_comm_group = {add := add_group.add uniform_space.completion.add_group, add_assoc := _, zero := add_group.zero uniform_space.completion.add_group, zero_add := _, add_zero := _, nsmul := add_group.nsmul uniform_space.completion.add_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg uniform_space.completion.add_group, sub := add_group.sub uniform_space.completion.add_group, sub_eq_add_neg := _, zsmul := add_group.zsmul uniform_space.completion.add_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}

@[protected, instance]

noncomputable def uniform_space.completion.module {R : Type u_2} {α : Type u_3} [uniform_space α] [add_comm_group α] [uniform_add_group α] [semiring R] [module R α] [has_uniform_continuous_const_smul R α] :

module R (uniform_space.completion α)

Equations

uniform_space.completion.module = {to_distrib_mul_action := {to_mul_action := {to_has_smul := {smul := has_smul.smul (uniform_space.completion.has_smul R α)}, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}, add_smul := _, zero_smul := _}

noncomputable def add_monoid_hom.extension {α : Type u_3} {β : Type u_4} [uniform_space α] [add_group α] [uniform_add_group α] [uniform_space β] [add_group β] [uniform_add_group β] [complete_space β] [separated_space β] (f : α →+ β) (hf : continuous ⇑f) :

uniform_space.completion α →+ β

Extension to the completion of a continuous group hom.

Equations

f.extension hf = have hf : uniform_continuous ⇑f, from _, {to_fun := uniform_space.completion.extension ⇑f, map_zero' := _, map_add' := _}

theorem add_monoid_hom.extension_coe {α : Type u_3} {β : Type u_4} [uniform_space α] [add_group α] [uniform_add_group α] [uniform_space β] [add_group β] [uniform_add_group β] [complete_space β] [separated_space β] (f : α →+ β) (hf : continuous ⇑f) (a : α) :

⇑(f.extension hf) ↑a = ⇑f a

@[continuity]

theorem add_monoid_hom.continuous_extension {α : Type u_3} {β : Type u_4} [uniform_space α] [add_group α] [uniform_add_group α] [uniform_space β] [add_group β] [uniform_add_group β] [complete_space β] [separated_space β] (f : α →+ β) (hf : continuous ⇑f) :

continuous ⇑(f.extension hf)

noncomputable def add_monoid_hom.completion {α : Type u_3} {β : Type u_4} [uniform_space α] [add_group α] [uniform_add_group α] [uniform_space β] [add_group β] [uniform_add_group β] (f : α →+ β) (hf : continuous ⇑f) :

uniform_space.completion α →+ uniform_space.completion β

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

Equations

f.completion hf = (uniform_space.completion.to_compl.comp f).extension _

@[continuity]

theorem add_monoid_hom.continuous_completion {α : Type u_3} {β : Type u_4} [uniform_space α] [add_group α] [uniform_add_group α] [uniform_space β] [add_group β] [uniform_add_group β] (f : α →+ β) (hf : continuous ⇑f) :

continuous ⇑(f.completion hf)

theorem add_monoid_hom.completion_coe {α : Type u_3} {β : Type u_4} [uniform_space α] [add_group α] [uniform_add_group α] [uniform_space β] [add_group β] [uniform_add_group β] (f : α →+ β) (hf : continuous ⇑f) (a : α) :

⇑(f.completion hf) ↑a = ↑(⇑f a)

theorem add_monoid_hom.completion_zero {α : Type u_3} {β : Type u_4} [uniform_space α] [add_group α] [uniform_add_group α] [uniform_space β] [add_group β] [uniform_add_group β] :

0.completion continuous_const = 0

theorem add_monoid_hom.completion_add {α : Type u_3} [uniform_space α] [add_group α] [uniform_add_group α] {γ : Type u_1} [add_comm_group γ] [uniform_space γ] [uniform_add_group γ] (f g : α →+ γ) (hf : continuous ⇑f) (hg : continuous ⇑g) :

(f + g).completion _ = f.completion hf + g.completion hg