Proper group action #
In this file we define proper action of a group on a topological space, and we prove that in this
case the quotient space is T2. We also give equivalent definitions of proper action using
ultrafilters and show the transfer of proper action to a closed subgroup.
We give sufficient conditions on the topological space such that the action is properly
discontinuous (see ProperlyDiscontinuousSMul
) if and only if it is continuous in
the first variable (see ContinuousConstSMul
) and proper in the sense defined here.
Main definitions #
ProperSMul
: a groupG
acts properly on a topological spaceX
if the map(g, x) ↦ (g • x, x)
is proper, in the sense ofIsProperMap
.
Main statements #
t2Space_quotient_mulAction_of_properSMul
: If a groupG
acts properly on a topological spaceX
, then the quotient space is Hausdorff (T2).t2Space_of_properSMul_of_t2Group
: If a T2 group acts properly on a topological space, then this topological space is T2.properlyDiscontinuousSMul_iff_properSMul
: If a discrete group acts on a T2 spaceX
such thatX × X
is compactly generated, then the action is properly discontinuous if and only if it is continuous in the second variable and proper. This in particular true ifX
is locally compact or first-countable.
Implementation notes #
Concerning properlyDiscontinuousSMul_iff_properSMul
, this result should be the only one needed
to link properly discontinuous and proper actions.
TODO: Replace the compactly generated hypothesis by a typeclass instance such that
WeaklyLocallyCompactSpace.isProperMap_iff_isCompact_preimage
and
SequentialSpace.isProperMap_iff_isCompact_preimage
are inferred by typeclass inference.
References #
Tags #
Hausdorff, group action, proper action
Proper group action in the sense of Bourbaki:
the map G × X → X × X
is a proper map (see IsProperMap
).
- isProperMap_vadd_pair : IsProperMap fun (gx : G × X) => (gx.1 +ᵥ gx.2, gx.2)
Proper group action in the sense of Bourbaki: the map
G × X → X × X
is a proper map (seeIsProperMap
).
Instances
Proper group action in the sense of Bourbaki:
the map G × X → X × X
is a proper map (see IsProperMap
).
Proper group action in the sense of Bourbaki:
the map G × X → X × X
is a proper map (see IsProperMap
).
- isProperMap_smul_pair : IsProperMap fun (gx : G × X) => (gx.1 • gx.2, gx.2)
Proper group action in the sense of Bourbaki: the map
G × X → X × X
is a proper map (seeIsProperMap
).
Instances
Proper group action in the sense of Bourbaki:
the map G × X → X × X
is a proper map (see IsProperMap
).
If a group acts properly then in particular it acts continuously.
Equations
- ⋯ = ⋯
If a group acts properly then in particular it acts continuously.
Equations
- ⋯ = ⋯
A group acts G
properly on a topological space X
if and only if
for all ultrafilters 𝒰
on X
, if 𝒰
converges to (x₁, x₂)
along the map (g, x) ↦ (g • x, x)
, then there exists g : G
such that g • x₂ = x₁
and 𝒰.fst
converges to g
.
A group G
acts properly on a topological space X
if and only if for all ultrafilters
𝒰
on X × G
, if 𝒰
converges to (x₁, x₂)
along the map (g, x) ↦ (g • x, x)
,
then there exists g : G
such that g • x₂ = x₁
and 𝒰.fst
converges to g
.
A group G
acts properly on a T2 topological space X
if and only if for all ultrafilters
𝒰
on X × G
, if 𝒰
converges to (x₁, x₂)
along the map (g, x) ↦ (g • x, x)
,
then there exists g : G
such that 𝒰.fst
converges to g
.
If G
acts properly on X
, then the quotient space is Hausdorff (T2).
If G
acts properly on X
, then the quotient space is Hausdorff (T2).
If a T2 group acts properly on a topological space, then this topological space is T2.
If a T2 group acts properly on a topological space, then this topological space is T2.
If two groups H
and G
act on a topological space X
such that G
acts properly
and there exists a group homomorphims H → G
which is a closed embedding compatible with the
actions, then H
also acts properly on X
.
If two groups H
and G
act on a topological space X
such that G
acts properly and
there exists a group homomorphims H → G
which is a closed embedding compatible with the actions,
then H
also acts properly on X
.
If H
is a closed subgroup of G
and G
acts properly on X then so does H
.
Equations
- ⋯ = ⋯
If H
is a closed subgroup of G
and G
acts properly on X then so does H
.
Equations
- ⋯ = ⋯
If a discrete group acts on a T2 space X
such that X × X
is compactly generated,
then the action is properly discontinuous if and only if it is continuous in the second variable
and proper.
If a discrete group acts on a T2 and locally compact space X
,
then the action is properly discontinuous if and only if it is continuous in the second variable
and proper.
If a discrete group acts on a T2 and first-countable space X
,
then the action is properly discontinuous if and only if it is continuous in the second variable
and proper.