Uniform structure on topological groups #
This file defines uniform groups and its additive counterpart. These typeclasses should be
preferred over using [TopologicalSpace α] [IsTopologicalGroup α]
since every topological
group naturally induces a uniform structure.
Main declarations #
IsUniformGroup
andIsUniformAddGroup
: Multiplicative and additive uniform groups, i.e., groups with uniformly continuous(*)
and(⁻¹)
/(+)
and(-)
.
Main results #
IsTopologicalAddGroup.toUniformSpace
andcomm_topologicalAddGroup_is_uniform
can be used to construct a canonical uniformity for a topological additive group.
See Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean
for further results.
A uniform group is a group in which multiplication and inversion are uniformly continuous.
- uniformContinuous_div : UniformContinuous fun (p : α × α) => p.1 / p.2
Instances
Alias of IsUniformGroup
.
A uniform group is a group in which multiplication and inversion are uniformly continuous.
Equations
Instances For
A uniform additive group is an additive group in which addition and negation are uniformly continuous.
- uniformContinuous_sub : UniformContinuous fun (p : α × α) => p.1 - p.2
Instances
Alias of IsUniformAddGroup
.
A uniform additive group is an additive group in which addition and negation are uniformly continuous.
Equations
Instances For
If f : ι → G × G
converges to the uniformity, then any g : ι → G × G
converges to the
uniformity iff f * g
does. This is often useful when f
is valued in the diagonal,
in which case its convergence is automatic.
If f : ι → G × G
converges to the uniformity, then any g : ι → G × G
converges to the uniformity iff f + g
does. This is often useful when f
is valued in the
diagonal, in which case its convergence is automatic.
If g : ι → G × G
converges to the uniformity, then any f : ι → G × G
converges to the
uniformity iff f * g
does. This is often useful when g
is valued in the diagonal,
in which case its convergence is automatic.
If g : ι → G × G
converges to the uniformity, then any f : ι → G × G
converges to the uniformity iff f + g
does. This is often useful when g
is valued in the
diagonal, in which case its convergence is automatic.
Alias of IsUniformAddGroup.to_topologicalAddGroup
.
Alias of IsUniformGroup.to_topologicalGroup
.
Alias of IsUniformAddGroup.ext
.
Alias of IsUniformGroup.ext
.
Alias of IsUniformAddGroup.ext_iff
.
Alias of IsUniformGroup.ext_iff
.
A group homomorphism (a bundled morphism of a type that implements MonoidHomClass
) between
two uniform groups is uniformly continuous provided that it is continuous at one. See also
continuous_of_continuousAt_one
.
An additive group homomorphism (a bundled morphism of a type that implements
AddMonoidHomClass
) between two uniform additive groups is uniformly continuous provided that it
is continuous at zero. See also continuous_of_continuousAt_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 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
IsUniformGroup
structure. Two important special cases where they do coincide are for
commutative groups (see isUniformGroup_of_commGroup
) and for compact groups (see
IsUniformGroup.of_compactSpace
).
Equations
- IsTopologicalGroup.toUniformSpace G = { toTopologicalSpace := inst✝¹, uniformity := Filter.comap (fun (p : G × G) => p.2 / p.1) (nhds 1), symm := ⋯, comp := ⋯, nhds_eq_comap_uniformity := ⋯ }
Instances For
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
IsUniformAddGroup
structure. Two important special cases where they do coincide are for
commutative additive groups (see isUniformAddGroup_of_addCommGroup
) and for compact
additive groups (see IsUniformAddGroup.of_compactSpace
).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Alias of isUniformGroup_of_commGroup
.
Alias of isUniformAddGroup_of_addCommGroup
.
Alias of isUniformGroup_of_commGroup
.