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 statements

• 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.
• MulAction.properSMul_iff_isCompact_setOf_inter_nonempty: if G is a topological group acting continuously on a T2 space X such that X × X is compactly generated, then the action is proper iff, for each pair of compacts U, V ⊆ X, the set of g : G such that g • U intersects V is compact.

Tags

group action, proper action, properly discontinuous, compactly generated

theorem MulAction.properSMul_iff_isCompact_setOf_inter_nonempty {G : Type u_1} {X : Type u_2} [TopologicalSpace X] [Group G] [TopologicalSpace G] [MulAction G X] [CompactlyGeneratedSpace (X × X)] [T2Space X] [ContinuousSMul G X] : ProperSMul G X ↔ ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact {g : G | (g • U ∩ V).Nonempty}

The G-action on X is proper iff, for each pair of compacts U, V in X, the set of g such that U intersects g • V is compact.

See ProperSMul.isCompact_setOf_inter_nonempty for a one-way implication with fewer conditions.

Note: We assume CompactlyCoherentSpace (X × X) as this is the minimal assumption needed to make the proof work; but this follows from various more familiar conditions, such as FirstCountableTopology X. Importing Mathlib.Topology.Sequences makes this implication available.

theorem AddAction.properVAdd_iff_isCompact_setOf_inter_nonempty {G : Type u_1} {X : Type u_2} [TopologicalSpace X] [AddGroup G] [TopologicalSpace G] [AddAction G X] [CompactlyGeneratedSpace (X × X)] [T2Space X] [ContinuousVAdd G X] : ProperVAdd G X ↔ ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact {g : G | ((g +ᵥ U) ∩ V).Nonempty}

The G-action on X is proper iff, for each pair of compacts U, V in X, the set of g such that U intersects g +ᵥ V is compact.

See ProperVAdd.isCompact_setOf_inter_nonempty for a one-way implication with fewer conditions.

Note: We assume CompactlyCoherentSpace (X × X) as this is the minimal assumption needed to make the proof work; but this follows from various more familiar conditions, such as FirstCountableTopology X. Importing Mathlib.Topology.Sequences makes this implication available.

theorem properlyDiscontinuousSMul_iff_properSMul {G : Type u_1} {X : Type u_2} [TopologicalSpace X] [Group G] [TopologicalSpace G] [MulAction G X] [CompactlyGeneratedSpace (X × X)] [T2Space X] [DiscreteTopology G] [ContinuousConstSMul G 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.

theorem properlyDiscontinuousVAdd_iff_properVAdd {G : Type u_1} {X : Type u_2} [TopologicalSpace X] [AddGroup G] [TopologicalSpace G] [AddAction G X] [CompactlyGeneratedSpace (X × X)] [T2Space X] [DiscreteTopology G] [ContinuousConstVAdd G X] : ProperlyDiscontinuousVAdd G X ↔ ProperVAdd G X