Topological groups #
This file defines the following typeclasses:
-
TopologicalGroup
,TopologicalAddGroup
: multiplicative and additive topological groups, i.e., groups with continuous(*)
and(⁻¹)
/(+)
and(-)
; -
ContinuousSub G
means thatG
has a continuous subtraction operation.
There is an instance deducing ContinuousSub
from TopologicalGroup
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.mulLeft
,
Homeomorph.mulRight
, 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.
Instances For
Multiplication from the left in a topological group as a homeomorphism.
Instances For
Addition from the right in a topological additive group as a homeomorphism.
Instances For
Multiplication from the right in a topological group as a homeomorphism.
Instances For
- continuous_neg : Continuous fun a => -a
Basic hypothesis to talk about a topological additive group. A topological additive group
over M
, for example, is obtained by requiring the instances AddGroup M
and
ContinuousAdd M
and ContinuousNeg M
.
Instances
- continuous_inv : Continuous fun a => a⁻¹
Basic hypothesis to talk about a topological group. A topological group over M
, for example,
is obtained by requiring the instances Group M
and ContinuousMul M
and
ContinuousInv M
.
Instances
If a function converges to a value in an additive topological group, then its negation converges to the negation of this value.
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'
.
A version of Pi.continuousNeg
for non-dependent functions. It is needed
because sometimes Lean fails to use Pi.continuousNeg
for non-dependent functions.
A version of Pi.continuousInv
for non-dependent functions. It is needed because sometimes
Lean fails to use Pi.continuousInv
for non-dependent functions.
Negation in a topological group as a homeomorphism.
Instances For
Inversion in a topological group as a homeomorphism.
Instances For
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.
A topological (additive) group is a group in which the addition and negation operations are continuous.
Instances
A topological group is a group in which the multiplication and inversion operations are continuous.
When you declare an instance that does not already have a UniformSpace
instance,
you should also provide an instance of UniformSpace
and UniformGroup
using
TopologicalGroup.toUniformSpace
and topologicalCommGroup_isUniform
.
Instances
Conjugation is jointly continuous on G × G
when both add
and neg
are continuous.
Conjugation is jointly continuous on G × G
when both mul
and inv
are continuous.
Conjugation by a fixed element is continuous when add
is continuous.
Conjugation by a fixed element is continuous when mul
is continuous.
Conjugation acting on fixed element of the additive group is continuous when both
add
and neg
are continuous.
Conjugation acting on fixed element of the group is continuous when both mul
and
inv
are continuous.
Instances For
If addition is continuous in α
, then it also is in αᵃᵒᵖ
.
If multiplication is continuous in α
, then it also is in αᵐᵒᵖ
.
The map (x, y) ↦ (x, x + y)
as a homeomorphism. This is a shear mapping.
Instances For
The map (x, y) ↦ (x, x * y)
as a homeomorphism. This is a shear mapping.
Instances For
The (topological-space) closure of an additive subgroup of a space M
with
ContinuousAdd
is itself an additive subgroup.
Instances For
The (topological-space) closure of a subgroup of a space M
with ContinuousMul
is
itself a subgroup.
Instances For
The topological closure of a normal additive subgroup is normal.
The topological closure of a normal subgroup is normal.
The connected component of 0 is a subgroup of G
.
Instances For
The connected component of 1 is a subgroup of G
.
Instances For
If a subgroup of an additive topological group is commutative, then so is its topological closure.
Instances For
If a subgroup of a topological group is commutative, then so is its topological closure.
Instances For
An additive monoid homomorphism (a bundled morphism of a type that implements
AddMonoidHomClass
) from an additive topological group to an additive topological monoid is
continuous provided that it is continuous at zero. See also
uniformContinuous_of_continuousAt_zero
.
A monoid homomorphism (a bundled morphism of a type that implements MonoidHomClass
) from a
topological group to a topological monoid is continuous provided that it is continuous at one. See
also uniformContinuous_of_continuousAt_one
.
Neighborhoods in the quotient are precisely the map of neighborhoods in the prequotient.
Neighborhoods in the quotient are precisely the map of neighborhoods in the prequotient.
Any first countable topological additive group has an antitone neighborhood basis
u : ℕ → set G
for which u (n + 1) + u (n + 1) ⊆ u n
.
The existence of such a neighborhood basis is a key tool for QuotientAddGroup.completeSpace
Any first countable topological group has an antitone neighborhood basis u : ℕ → Set G
for
which (u (n + 1)) ^ 2 ⊆ u n
. The existence of such a neighborhood basis is a key tool for
QuotientGroup.completeSpace
In a first countable topological additive group G
with normal additive subgroup
N
, 0 : G ⧸ N
has a countable neighborhood basis.
In a first countable topological group G
with normal subgroup N
, 1 : G ⧸ N
has a
countable neighborhood basis.
- continuous_sub : Continuous fun p => 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
.
Instances
- continuous_div' : Continuous fun p => 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 groups. Lemmas using this class have primes.
The unprimed version is for GroupWithZero
.
Instances
A version of Homeomorph.addLeft a (-b)
that is defeq to a - b
.
Instances For
A version of Homeomorph.mulLeft a b⁻¹
that is defeq to a / b
.
Instances For
A version of Homeomorph.addRight (-a) b
that is defeq to b - a
.
Instances For
A version of Homeomorph.mulRight a⁻¹ b
that is defeq to b / a
.
Instances For
Topological operations on pointwise sums and products #
A few results about interior and closure of the pointwise addition/multiplication of sets in groups
with continuous addition/multiplication. See also Submonoid.top_closure_mul_self_eq
in
Topology.Algebra.Monoid
.
One may expect a version of IsClosed.smul_left_of_isCompact
where t
is compact and s
is
closed, but such a lemma can't be true in this level of generality. For a counterexample, consider
ℚ
acting on ℝ
by translation, and let s : set ℚ := univ
, t : set ℝ := {0}
. Then s
is
closed and t
is compact, but s +ᵥ t
is the set of all rationals, which is definitely not
closed in ℝ
.
To fix the proof, we would need to make two additional assumptions:
- for any
x ∈ t
,s • {x}
is closed - for any
x ∈ t
, there is a continuous functiong : s • {x} → s
such that, for ally ∈ s • {x}
, we havey = (g y) • x
These are fairly specific hypotheses so we don't state this version of the lemmas, but an interesting fact is that these two assumptions are verified in the case of aNormedAddTorsor
(or really, anyAddTorsor
with continuous-ᵥ
). We prove this special case inIsClosed.vadd_right_of_isCompact
.
A subgroup S
of an additive topological group G
acts on G
properly
discontinuously on the left, if it is discrete in the sense that S ∩ K
is finite for all compact
K
. (See also DiscreteTopology
.
A subgroup S
of a topological group G
acts on G
properly discontinuously on the left, if
it is discrete in the sense that S ∩ K
is finite for all compact K
. (See also
DiscreteTopology
.)
A subgroup S
of an additive topological group G
acts on G
properly discontinuously
on the right, if it is discrete in the sense that S ∩ K
is finite for all compact K
.
(See also DiscreteTopology
.)
If G
is Hausdorff, this can be combined with t2Space_of_properlyDiscontinuousVAdd_of_t2Space
to show that the quotient group G ⧸ S
is Hausdorff.
A subgroup S
of a topological group G
acts on G
properly discontinuously on the right, if
it is discrete in the sense that S ∩ K
is finite for all compact K
. (See also
DiscreteTopology
.)
If G
is Hausdorff, this can be combined with t2Space_of_properlyDiscontinuousSMul_of_t2Space
to show that the quotient group G ⧸ S
is Hausdorff.
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 an open neighborhood V
of
0
such that K + V ⊆ U
.
Given a compact set K
inside an open set U
, there is an open neighborhood V
of 1
such that K * V ⊆ U
.
Given a compact set K
inside an open set U
, there is an open neighborhood V
of
0
such that V + K ⊆ U
.
Given a compact set K
inside an open set U
, there is an open neighborhood V
of 1
such that V * K ⊆ 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 weakly locally compact separable topological additive group is σ-compact. Note: this is not true if we drop the topological group hypothesis.
Every weakly locally compact separable topological group is σ-compact. Note: this is not true if we drop the topological group hypothesis.
Given two compact sets in a noncompact additive topological group, there is a translate of the second one that is disjoint from the first one.
Given two compact sets in a noncompact topological group, there is a translate of the second one that is disjoint from the first one.
A compact neighborhood of 0
in a topological additive group
admits a closed compact subset that is a neighborhood of 0
.
A compact neighborhood of 1
in a topological group admits a closed compact subset
that is a neighborhood of 1
.
In a locally compact additive group, any neighborhood of the identity contains a compact closed neighborhood of the identity, even without separation assumptions on the space.
In a locally compact group, any neighborhood of the identity contains a compact closed neighborhood of the identity, even without separation assumptions on the space.