Uniform structure on topological groups #
This file defines uniform groups and its additive counterpart. These typeclasses should be
preferred over using [topological_space α] [topological_group α]
since every topological
group naturally induces a uniform structure.
Main declarations #
uniform_group
anduniform_add_group
: Multiplicative and additive uniform groups, that i.e., groups with uniformly continuous(*)
and(⁻¹)
/(+)
and(-)
.
Main results #
-
topological_add_group.to_uniform_space
andtopological_add_comm_group_is_uniform
can be used to construct a canonical uniformity for a topological add group. -
extension of ℤ-bilinear maps to complete groups (useful for ring completions)
- uniform_continuous_div : uniform_continuous (λ (p : α × α), p.fst / p.snd)
A uniform group is a group in which multiplication and inversion are uniformly continuous.
Instances of this typeclass
- uniform_continuous_sub : uniform_continuous (λ (p : α × α), p.fst - p.snd)
A uniform additive group is an additive group in which addition and negation are uniformly continuous.
A group homomorphism (a bundled morphism of a type that implements monoid_hom_class
) between
two uniform groups is uniformly continuous provided that it is continuous at one. See also
continuous_of_continuous_at_one
.
An additive group homomorphism (a bundled morphism of a type that implements
add_monoid_hom_class
) between two uniform additive groups is uniformly continuous provided that it
is continuous at zero. See also continuous_of_continuous_at_zero
.
A homomorphism from a uniform group to a discrete uniform group is continuous if and only if its kernel is open.
A homomorphism from a uniform additive group to a discrete uniform additive group is continuous if and only if its kernel is open.
The right uniformity on a topological additive group (as opposed to the left uniformity).
Warning: in general the right and left uniformities do not coincide and so one does not obtain a
uniform_add_group
structure. Two important special cases where they do coincide are for
commutative additive groups (see topological_add_comm_group_is_uniform
) and for compact Hausdorff
additive groups (see topological_add_comm_group_is_uniform_of_compact_space
).
Equations
- topological_add_group.to_uniform_space G = {to_topological_space := _inst_2, to_core := {uniformity := filter.comap (λ (p : G × G), p.snd - p.fst) (nhds 0), refl := _, symm := _, comp := _}, is_open_uniformity := _}
The right uniformity on a topological group (as opposed to the left uniformity).
Warning: in general the right and left uniformities do not coincide and so one does not obtain a
uniform_group
structure. Two important special cases where they do coincide are for
commutative groups (see topological_comm_group_is_uniform
) and for compact Hausdorff groups (see
topological_group_is_uniform_of_compact_space
).
Equations
- topological_group.to_uniform_space G = {to_topological_space := _inst_2, to_core := {uniformity := filter.comap (λ (p : G × G), p.snd / p.fst) (nhds 1), refl := _, symm := _, comp := _}, is_open_uniformity := _}
Bourbaki GT III.6.5 Theorem I: ℤ-bilinear continuous maps from dense images into a complete Hausdorff group extend by continuity. Note: Bourbaki assumes that α and β are also complete Hausdorff, but this is not necessary.