When a proper action is properly discontinuous

This file proves that if a discrete group acts on a T2 space X such that X × X is compactly generated, and if the action is continuous in the second variable, then the action is properly discontinuous if and only if it is proper. This is in particular true if X is first-countable or weakly locally compact.

Main statement

• properlyDiscontinuousSMul_iff_properSMul: If a discrete group acts on a T2 space X such that X × X is compactly generated, and if the action is continuous in the second variable, then the action is properly discontinuous if and only if it is proper.

Tags

grouup action, proper action, properly discontinuous, compactly generated

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] [CompactlyGeneratedSpace (X × X)] : ProperlyDiscontinuousSMul G X ↔ ProperSMul G X

If a discrete group acts on a T2 space X such that X × X is compactly generated, and if the action is continuous in the second variable, then the action is properly discontinuous if and only if it is proper. This is in particular true if X is first-countable or weakly locally compact.

There was an older version of this theorem which was changed to this one to make use of the CompactlyGeneratedSpace typeclass. (since 2024-11-10)