Theory of topological groups
This file defines the following typeclasses:
topological_group
,topological_add_group
: multiplicative and additive topological groups, i.e., groups with continuous(*)
and(⁻¹)
/(+)
and(-)
;has_continuous_sub G
means thatG
has a continuous subtraction operation.
There is an instance deducing has_continuous_sub
from topological_group
but we use a separate
typeclass because, e.g., ℕ
and ℝ≥0
have continuous subtraction but are not additive groups.
We also define homeomorph
versions of several equiv
s: homeomorph.mul_left
,
homeomorph.mul_right
, homeomorph.inv
, and prove a few facts about neighbourhood filters in
groups.
Tags
topological space, group, topological group
Groups with continuous multiplication
In this section we prove a few statements about groups with continuous (*)
.
Addition from the left in a topological additive group as a homeomorphism.
Multiplication from the left in a topological group as a homeomorphism.
Equations
- homeomorph.mul_left a = {to_equiv := {to_fun := (equiv.mul_left a).to_fun, inv_fun := (equiv.mul_left a).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
Addition from the right in a topological additive group as a homeomorphism.
Multiplication from the right in a topological group as a homeomorphism.
Equations
- homeomorph.mul_right a = {to_equiv := {to_fun := (equiv.mul_right a).to_fun, inv_fun := (equiv.mul_right a).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
Topological groups
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.
- to_has_continuous_add : has_continuous_add G
- continuous_neg : continuous (λ (a : G), -a)
A topological (additive) group is a group in which the addition and negation operations are continuous.
Instances
- uniform_add_group.to_topological_add_group
- add_group_with_zero_nhd.topological_add_group
- topological_ring.to_topological_add_group
- linear_ordered_add_comm_group.topological_add_group
- normed_top_group
- prod.topological_add_group
- topological_add_group_quotient
- additive.topological_add_group
- real.topological_add_group
- rat.topological_add_group
- tangent_space.topological_add_group
- to_has_continuous_mul : has_continuous_mul G
- continuous_inv : continuous has_inv.inv
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 tendsto.inv'
.
Negation in a topological group as a homeomorphism.
Inversion in a topological group as a homeomorphism.
Equations
- homeomorph.inv G = {to_equiv := {to_fun := (equiv.inv G).to_fun, inv_fun := (equiv.inv G).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
The map (x, y) ↦ (x, xy)
as a homeomorphism. This is a shear mapping.
Equations
- homeomorph.shear_mul_right G = {to_equiv := {to_fun := ((equiv.refl G).prod_shear equiv.mul_left).to_fun, inv_fun := ((equiv.refl G).prod_shear equiv.mul_left).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
The map (x, y) ↦ (x, x + y)
as a homeomorphism.
This is a shear mapping.
- continuous_sub : continuous (λ (p : G × G), p.fst - p.snd)
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 ℝ≥0
.
- 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.
Equations
- add_group_with_zero_nhd.topological_space G = topological_space.mk_of_nhds (λ (a : G), filter.map (λ (x : G), x + a) (add_group_with_zero_nhd.Z G))
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 V
of 0
such that K + V ⊆ U
.
Given a compact set K
inside an open set U
, there is a open neighborhood V
of 1
such that KV ⊆ 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.
Every locally compact separable topological group is σ-compact. Note: this is not true if we drop the topological group hypothesis.