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 group G acts properly on a topological space X if the map (g, x) ↦ (g • x, x) is proper, in the sense of IsProperMap.

Main statements

• t2Space_quotient_mulAction_of_properSMul: If a group G acts properly on a topological space X, 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 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. This in particular true if X 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

• [N. Bourbaki, General Topology][bourbaki1966]

Tags

Hausdorff, group action, proper action

class ProperVAdd (G : Type u_1) (X : Type u_2) [TopologicalSpace G] [TopologicalSpace X] [AddGroup G] [AddAction G X] : Prop

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 (see IsProperMap).

theorem ProperVAdd.isProperMap_vadd_pair {G : Type u_1} {X : Type u_2} : ∀ {inst : TopologicalSpace G} {inst_1 : TopologicalSpace X} {inst_2 : AddGroup G} {inst_3 : AddAction G X} [self : ProperVAdd G X], 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 (see IsProperMap).

theorem properSMul_iff (G : Type u_1) (X : Type u_2) [TopologicalSpace G] [TopologicalSpace X] [Group G] [MulAction G X] : ProperSMul G X ↔ IsProperMap fun (gx : G × X) => (gx.1 • gx.2, gx.2)

theorem properVAdd_iff (G : Type u_1) (X : Type u_2) [TopologicalSpace G] [TopologicalSpace X] [AddGroup G] [AddAction G X] : ProperVAdd G X ↔ IsProperMap fun (gx : G × X) => (gx.1 +ᵥ gx.2, gx.2)

class ProperSMul (G : Type u_1) (X : Type u_2) [TopologicalSpace G] [TopologicalSpace X] [Group G] [MulAction G X] : Prop

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 (see IsProperMap).

theorem ProperSMul.isProperMap_smul_pair {G : Type u_1} {X : Type u_2} : ∀ {inst : TopologicalSpace G} {inst_1 : TopologicalSpace X} {inst_2 : Group G} {inst_3 : MulAction G X} [self : ProperSMul G X], 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 (see IsProperMap).

@[instance 100]

instance ProperVAdd.toContinuousVAdd {G : Type u_1} {X : Type u_2} [AddGroup G] [AddAction G X] [TopologicalSpace G] [TopologicalSpace X] [ProperVAdd G X] : ContinuousVAdd G X

If a group acts properly then in particular it acts continuously.

Equations

• ⋯ = ⋯

@[instance 100]

instance ProperSMul.toContinuousSMul {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace G] [TopologicalSpace X] [ProperSMul G X] : ContinuousSMul G X

If a group acts properly then in particular it acts continuously.

Equations

• ⋯ = ⋯

theorem properVAdd_iff_continuousVAdd_ultrafilter_tendsto {G : Type u_1} {X : Type u_2} [AddGroup G] [AddAction G X] [TopologicalSpace G] [TopologicalSpace X] : ProperVAdd G X ↔ ContinuousVAdd G X ∧ ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X), Filter.Tendsto (fun (gx : G × X) => (gx.1 +ᵥ gx.2, gx.2)) (↑𝒰) (nhds (x₁, x₂)) → ∃ (g : G), g +ᵥ x₂ = x₁ ∧ Filter.Tendsto Prod.fst (↑𝒰) (nhds g)

A group G acts 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.

theorem properSMul_iff_continuousSMul_ultrafilter_tendsto {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace G] [TopologicalSpace X] : ProperSMul G X ↔ ContinuousSMul G X ∧ ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X), Filter.Tendsto (fun (gx : G × X) => (gx.1 • gx.2, gx.2)) (↑𝒰) (nhds (x₁, x₂)) → ∃ (g : G), g • x₂ = x₁ ∧ Filter.Tendsto Prod.fst (↑𝒰) (nhds 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.

theorem properSMul_iff_continuousSMul_ultrafilter_tendsto_t2 {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace G] [TopologicalSpace X] [T2Space X] : ProperSMul G X ↔ ContinuousSMul G X ∧ ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X), Filter.Tendsto (fun (gx : G × X) => (gx.1 • gx.2, gx.2)) (↑𝒰) (nhds (x₁, x₂)) → ∃ (g : G), Filter.Tendsto Prod.fst (↑𝒰) (nhds 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.

theorem t2Space_quotient_addAction_of_properVAdd {G : Type u_1} {X : Type u_2} [AddGroup G] [AddAction G X] [TopologicalSpace G] [TopologicalSpace X] [ProperVAdd G X] : T2Space (Quotient (AddAction.orbitRel G X))

If G acts properly on X, then the quotient space is Hausdorff (T2).

theorem t2Space_quotient_mulAction_of_properSMul {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace G] [TopologicalSpace X] [ProperSMul G X] : T2Space (Quotient (MulAction.orbitRel G X))

If G acts properly on X, then the quotient space is Hausdorff (T2).

theorem t2Space_of_properVAdd_of_t2AddGroup {G : Type u_1} {X : Type u_2} [AddGroup G] [AddAction G X] [TopologicalSpace G] [TopologicalSpace X] [h_proper : ProperVAdd G X] [T2Space G] : T2Space X

If a T2 group acts properly on a topological space, then this topological space is T2.

theorem t2Space_of_properSMul_of_t2Group {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace G] [TopologicalSpace X] [h_proper : ProperSMul G X] [T2Space G] : T2Space X

If a T2 group acts properly on a topological space, then this topological space is T2.

theorem properVAdd_of_closedEmbedding {G : Type u_1} {X : Type u_2} [AddGroup G] [AddAction G X] [TopologicalSpace G] [TopologicalSpace X] {H : Type u_3} [AddGroup H] [AddAction H X] [TopologicalSpace H] [ProperVAdd G X] (f : H →+ G) (f_clemb : ClosedEmbedding ⇑f) (f_compat : ∀ (h : H) (x : X), f h +ᵥ x = h +ᵥ x) : ProperVAdd H 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.

theorem properSMul_of_closedEmbedding {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace G] [TopologicalSpace X] {H : Type u_3} [Group H] [MulAction H X] [TopologicalSpace H] [ProperSMul G X] (f : H →* G) (f_clemb : ClosedEmbedding ⇑f) (f_compat : ∀ (h : H) (x : X), f h • x = h • x) : ProperSMul H 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.

instance instProperVAddSubtypeMemAddSubgroupOfIsClosedCoe {G : Type u_1} {X : Type u_2} [AddGroup G] [AddAction G X] [TopologicalSpace G] [TopologicalSpace X] {H : AddSubgroup G} [ProperVAdd G X] [H_closed : IsClosed ↑H] : ProperVAdd (↥H) X

If H is a closed subgroup of G and G acts properly on X then so does H.

Equations

• ⋯ = ⋯

instance instProperSMulSubtypeMemSubgroupOfIsClosedCoe {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace G] [TopologicalSpace X] {H : Subgroup G} [ProperSMul G X] [H_closed : IsClosed ↑H] : ProperSMul (↥H) X

If H is a closed subgroup of G and G acts properly on X then so does H.

Equations

• ⋯ = ⋯

theorem properlyDiscontinuousSMul_iff_properSMul {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace G] [TopologicalSpace X] [T2Space X] [DiscreteTopology G] [ContinuousConstSMul G X] (compactlyGenerated : ∀ (s : Set (X × X)), IsClosed s ↔ ∀ ⦃K : Set (X × X)⦄, IsCompact K → IsClosed (s ∩ K)) : ProperlyDiscontinuousSMul G X ↔ ProperSMul G X

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.

theorem WeaklyLocallyCompactSpace.properlyDiscontinuousSMul_iff_properSMul {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace G] [TopologicalSpace X] [T2Space X] [WeaklyLocallyCompactSpace X] [DiscreteTopology G] [ContinuousConstSMul G X] : ProperlyDiscontinuousSMul G X ↔ ProperSMul G X

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.

theorem FirstCountableTopology.properlyDiscontinuousSMul_iff_properSMul {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace G] [TopologicalSpace X] [T2Space X] [FirstCountableTopology X] [DiscreteTopology G] [ContinuousConstSMul G X] : ProperlyDiscontinuousSMul G X ↔ ProperSMul G X

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.