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.

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.

References

• N. Bourbaki, General Topology

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).

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_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)

@[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.

@[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.

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 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_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_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_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_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 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 properSMul_of_isClosedEmbedding {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 : Topology.IsClosedEmbedding ⇑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.

theorem properVAdd_of_isClosedEmbedding {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 : Topology.IsClosedEmbedding ⇑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.

@[deprecated properSMul_of_isClosedEmbedding]

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 : Topology.IsClosedEmbedding ⇑f) (f_compat : ∀ (h : H) (x : X), f h • x = h • x) : ProperSMul H X

Alias of properSMul_of_isClosedEmbedding.

---

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 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.

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.