Uniform structure on topological groups #
Main results #
extension of ℤ-bilinear maps to complete groups (useful for ring completions)
QuotientGroup.completeSpace
andQuotientAddGroup.completeSpace
guarantee that quotients of first countable topological groups by normal subgroups are themselves complete. In particular, the quotient of a Banach space by a subspace is complete.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Alias of isUniformEmbedding_translate_mul
.
Alias of IsUniformInducing.uniformGroup
.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
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.
The quotient G ⧸ N
of a complete first countable topological additive group
G
by a normal additive subgroup is itself complete. Consequently, quotients of Banach spaces by
subspaces are complete. N. Bourbaki, General Topology, IX.3.1 Proposition 4
Because an additive topological group is not equipped with a UniformSpace
instance by default,
we must explicitly provide it in order to consider completeness. See
QuotientAddGroup.completeSpace
for a version in which G
is already equipped with a uniform
structure.
Equations
- ⋯ = ⋯
The quotient G ⧸ N
of a complete first countable topological group G
by a normal subgroup
is itself complete. N. Bourbaki, General Topology, IX.3.1 Proposition 4
Because a topological group is not equipped with a UniformSpace
instance by default, we must
explicitly provide it in order to consider completeness. See QuotientGroup.completeSpace
for a
version in which G
is already equipped with a uniform structure.
Equations
- ⋯ = ⋯
The quotient G ⧸ N
of a complete first countable uniform additive group
G
by a normal additive subgroup is itself complete. Consequently, quotients of Banach spaces by
subspaces are complete. In contrast to QuotientAddGroup.completeSpace'
, in this version
G
is already equipped with a uniform structure.
N. Bourbaki, General Topology, IX.3.1 Proposition 4
Even though G
is equipped with a uniform structure, the quotient G ⧸ N
does not inherit a
uniform structure, so it is still provided manually via TopologicalAddGroup.toUniformSpace
.
In the most common use case ─ quotients of normed additive commutative groups by subgroups ─
significant care was taken so that the uniform structure inherent in that setting coincides
(definitionally) with the uniform structure provided here.
Equations
- ⋯ = ⋯
The quotient G ⧸ N
of a complete first countable uniform group G
by a normal subgroup
is itself complete. In contrast to QuotientGroup.completeSpace'
, in this version G
is
already equipped with a uniform structure.
N. Bourbaki, General Topology, IX.3.1 Proposition 4
Even though G
is equipped with a uniform structure, the quotient G ⧸ N
does not inherit a
uniform structure, so it is still provided manually via TopologicalGroup.toUniformSpace
.
In the most common use cases, this coincides (definitionally) with the uniform structure on the
quotient obtained via other means.
Equations
- ⋯ = ⋯