Completion of topological groups: #
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 fromG
to a complete separated groupH
tocompletion G
.add_monoid_hom.completion
: promotes a continuous group morphism fromG
toH
into a continuous group morphism fromcompletion G
tocompletion H
.
Equations
Equations
- uniform_space.completion.has_neg = {neg := uniform_space.completion.map (λ (a : α), -a)}
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 := _}
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' := _}
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' := _}
Equations
- uniform_space.completion.add_group = {add := sub_neg_monoid.add uniform_space.completion.sub_neg_monoid, add_assoc := _, zero := sub_neg_monoid.zero uniform_space.completion.sub_neg_monoid, zero_add := _, add_zero := _, nsmul := sub_neg_monoid.nsmul uniform_space.completion.sub_neg_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := sub_neg_monoid.neg uniform_space.completion.sub_neg_monoid, sub := sub_neg_monoid.sub uniform_space.completion.sub_neg_monoid, sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul uniform_space.completion.sub_neg_monoid, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _}
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_add := _, smul_zero := _}
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' := _}
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 := _}
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_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
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' := _}
Completion of a continuous group hom, as a group hom.
Equations
- f.completion hf = (uniform_space.completion.to_compl.comp f).extension _