Theory of topological groups
This file defines the following typeclasses:
has_continuous_sub Gmeans that
Ghas a continuous subtraction operation.
topological space, group, topological group
Groups with continuous multiplication
In this section we prove a few statements about groups with continuous
Multiplication from the left in a topological group as a homeomorphism.
Multiplication from the right in a topological group as a homeomorphism.
A topological group is a group in which the multiplication and inversion operations are
continuous. Topological additive groups are defined in the same way. Equivalently, we can require
that the division operation
λ x y, x * y⁻¹ (resp., subtraction) is continuous.
A topological (additive) group is a group in which the addition and negation operations are continuous.
A topological group is a group in which the multiplication and inversion operations are continuous.
If a function converges to a value in a multiplicative topological group, then its inverse
converges to the inverse of this value. For the version in normed fields assuming additionally
that the limit is nonzero, use
Inversion in a topological group as a homeomorphism.
A typeclass saying that
λ p : G × G, p.1 - p.2 is a continuous function. This property
automatically holds for topological additive groups but it also holds, e.g., for
- to_add_comm_group : add_comm_group G
- Z : filter G
- zero_Z : pure 0 ≤ add_group_with_zero_nhd.Z G
- sub_Z : filter.tendsto (λ (p : G × G), p.fst - p.snd) (add_group_with_zero_nhd.Z G ×ᶠ add_group_with_zero_nhd.Z G) (add_group_with_zero_nhd.Z G)
additive group with a neighbourhood around 0. Only used to construct a topology and uniform space.
This is currently only available for commutative groups, but it can be extended to non-commutative groups too.
Some results about an open set containing the product of two sets in a topological group.
Given a compact set
K inside an open set
U, there is a open neighborhood
K + V ⊆ U.
A compact set is covered by finitely many left additive translates of a set with non-empty interior.
A compact set is covered by finitely many left multiplicative translates of a set with non-empty interior.