Transfer instances for restricted and properly discontinuous actions

This file records generic instances for actions on a topological space that typeclass search cannot otherwise reach. A submonoid, and hence a subgroup, inherits ContinuousConstSMul from an ambient scalar action; and a properly discontinuous action has Finite point stabilisers. It also records that a properly discontinuous scalar family on a nonempty σ-compact space is countable, and that the translates of a compact set under it form a locally finite family. Conversely, for a jointly continuous action of a T₁ group with separately continuous multiplication, local finiteness of the translates of any nonempty set forces the group topology to be discrete. Likewise, a nonempty open set disjoint from all of its nontrivial translates forces the acting topological group to be discrete, and on such a set the orbit projection is an open embedding.

Main results

• Submonoid.continuousConstSMul and TauCeti.Subgroup.continuousConstSMul: continuity in the point is inherited by a submonoid, hence by a subgroup.
• SubMulAction.properlyDiscontinuousSMul: proper discontinuity is inherited by every invariant subspace.
• TauCeti.properlyDiscontinuousSMul_of_conjAct_smul_eq: a conjugate g H g⁻¹ of a properly discontinuous subgroup H acts properly discontinuously.
• TauCeti.finite_stabilizer_of_properlyDiscontinuousSMul: a properly discontinuous action has finite point stabilisers, as an instance rather than as Set.Finite of the carrier.
• TauCeti.countable_of_properlyDiscontinuousSMul: a properly discontinuous scalar family on a nonempty σ-compact space is countable.
• TauCeti.locallyFinite_smul_of_isCompact: under a properly discontinuous action on a weakly locally compact space, the translates of a compact set form a locally finite family.
• TauCeti.discreteTopology_of_locallyFinite_smul: if the translates of a nonempty set under a continuous action are locally finite, then the acting group is discrete.
• TauCeti.isClosed_iUnion_smul_of_isCompact: the union of the translates of a closed compact set under such an action of a group is closed.
• TauCeti.isOpenEmbedding_quotientMk_domRestrict_of_disjoint_smul: the orbit projection is an open embedding on an open set disjoint from its nontrivial translates.
• TauCeti.discreteTopology_of_disjoint_smul: the existence of a nonempty such open set makes the acting topological group discrete.

theorem TauCeti.injOn_quotientMk_of_disjoint_smul {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {U : Set X} (hU : ∀ (g : G), g ≠ 1 → Disjoint (g • U) U) : Set.InjOn Quotient.mk'' U

The orbit projection is injective on a set disjoint from each of its nontrivial translates.

theorem TauCeti.isOpenEmbedding_quotientMk_domRestrict_of_disjoint_smul {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {U : Set X} [TopologicalSpace X] [ContinuousConstSMul G X] (hU_open : IsOpen U) (hU : ∀ (g : G), g ≠ 1 → Disjoint (g • U) U) : Topology.IsOpenEmbedding (U.domRestrict Quotient.mk'')

On an open set disjoint from each of its nontrivial translates, the orbit projection is an open embedding. Thus this set is an honest open chart in the orbit space, not merely a set of orbit representatives.

theorem TauCeti.injOn_quotientMk_of_disjoint_vadd {A : Type u_1} {X : Type u_2} [AddGroup A] [AddAction A X] {U : Set X} (hU : ∀ (a : A), a ≠ 0 → Disjoint (a +ᵥ U) U) : Set.InjOn Quotient.mk'' U

The additive orbit projection is injective on a set disjoint from each of its nontrivial translates.

theorem TauCeti.isOpenEmbedding_quotientMk_domRestrict_of_disjoint_vadd {A : Type u_1} {X : Type u_2} [AddGroup A] [AddAction A X] {U : Set X} [TopologicalSpace X] [ContinuousConstVAdd A X] (hU_open : IsOpen U) (hU : ∀ (a : A), a ≠ 0 → Disjoint (a +ᵥ U) U) : Topology.IsOpenEmbedding (U.domRestrict Quotient.mk'')

On an open set disjoint from each of its nontrivial additive translates, the additive orbit projection is an open embedding.

theorem TauCeti.discreteTopology_of_disjoint_smul {G : Type u_1} {X : Type u_2} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] [TopologicalSpace X] [MulAction G X] {U : Set X} (hcont : ∀ (x : X), Continuous fun (g : G) => g • x) (hU_open : IsOpen U) (hU_nonempty : U.Nonempty) (hU : ∀ (g : G), g ≠ 1 → Disjoint (g • U) U) : DiscreteTopology G

Discreteness from a disjoint open translate. If a topological group acts with continuous orbit maps and some nonempty open set is disjoint from all of its translates by nonidentity elements, then the group is discrete.

theorem TauCeti.discreteTopology_of_disjoint_vadd {G : Type u_1} {X : Type u_2} [AddGroup G] [TopologicalSpace G] [SeparatelyContinuousAdd G] [TopologicalSpace X] [AddAction G X] {U : Set X} (hcont : ∀ (x : X), Continuous fun (g : G) => g +ᵥ x) (hU_open : IsOpen U) (hU_nonempty : U.Nonempty) (hU : ∀ (g : G), g ≠ 0 → Disjoint (g +ᵥ U) U) : DiscreteTopology G

Discreteness from a disjoint open translate. If a topological additive group acts with continuous orbit maps and some nonempty open set is disjoint from all of its translates by nonzero elements, then the group is discrete.

theorem TauCeti.discreteTopology_of_locallyFinite_smul {G : Type u_1} {X : Type u_2} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] [TopologicalSpace X] [MulAction G X] [ContinuousSMul G X] [T1Space G] {S : Set X} (hS : S.Nonempty) (hlocal : LocallyFinite fun (g : G) => g • S) : DiscreteTopology G

Local finiteness of the translates of a nonempty set forces the acting group to be discrete.

The set need not be open, closed, or compact, and the action need not be faithful. This is the discreteness criterion for a group whose translates of a fundamental polygon form a locally finite tessellation.

theorem TauCeti.discreteTopology_of_locallyFinite_vadd {G : Type u_1} {X : Type u_2} [AddGroup G] [TopologicalSpace G] [SeparatelyContinuousAdd G] [TopologicalSpace X] [AddAction G X] [ContinuousVAdd G X] [T1Space G] {S : Set X} (hS : S.Nonempty) (hlocal : LocallyFinite fun (g : G) => g +ᵥ S) : DiscreteTopology G

Local finiteness of the translates of a nonempty set forces the acting additive group to be discrete.

instance Submonoid.continuousConstSMul {M : Type u_1} {X : Type u_2} [MulOneClass M] [TopologicalSpace X] [SMul M X] [ContinuousConstSMul M X] (S : Submonoid M) : ContinuousConstSMul (↥S) X

A submonoid inherits continuity in the point from an ambient continuous action.

instance AddSubmonoid.continuousConstVAdd {M : Type u_1} {X : Type u_2} [AddZeroClass M] [TopologicalSpace X] [VAdd M X] [ContinuousConstVAdd M X] (S : AddSubmonoid M) : ContinuousConstVAdd (↥S) X

An additive submonoid inherits continuity in the point from an ambient continuous additive action.

instance TauCeti.Subgroup.continuousConstSMul {G : Type u_1} {X : Type u_2} [Group G] [TopologicalSpace X] [SMul G X] [ContinuousConstSMul G X] (S : Subgroup G) : ContinuousConstSMul (↥S) X

A subgroup inherits continuity in the point from an ambient continuous action.

theorem TauCeti.properlyDiscontinuousSMul_of_conjAct_smul_eq {G : Type u_1} {X : Type u_2} [Group G] [TopologicalSpace X] [MulAction G X] [ContinuousConstSMul G X] {H H' : Subgroup G} {g : G} [ProperlyDiscontinuousSMul (↥H) X] (h : ConjAct.toConjAct g • H = H') : ProperlyDiscontinuousSMul (↥H') X

Conjugation preserves proper discontinuity: if H' is the conjugate g H g⁻¹ of a subgroup H acting properly discontinuously, then H' acts properly discontinuously, since g k g⁻¹ moves K to meet L exactly when k moves g⁻¹ • K to meet g⁻¹ • L.

theorem SubMulAction.properlyDiscontinuousSMul {G : Type u_1} {X : Type u_2} [TopologicalSpace X] [SMul G X] [ProperlyDiscontinuousSMul G X] (S : SubMulAction G X) : ProperlyDiscontinuousSMul G ↥S

A properly discontinuous action remains properly discontinuous on every invariant subspace.

instance TauCeti.finite_stabilizer_of_properlyDiscontinuousSMul {G : Type u_1} {T : Type u_2} [Group G] [TopologicalSpace T] [MulAction G T] [ProperlyDiscontinuousSMul G T] (x : T) : Finite ↥(MulAction.stabilizer G x)

A properly discontinuous action has finite point stabilisers, as a Finite instance.

Mathlib's ProperlyDiscontinuousSMul.finite_stabilizer (Alex Kontorovich and Heather Macbeth, Mathlib/Topology/Algebra/ConstMulAction.lean) states this as Set.Finite of the stabiliser's carrier. That form does not drive typeclass search, so a count through Nat.card — which is the junk value 0 on an infinite type — has to bridge to Finite by hand at each use. This does it once, for every properly discontinuous action.

For an action of a subgroup of GL(2, ℝ) no further instance is needed: Mathlib's Subgroup.IsArithmetic.properlyDiscontinuous supplies proper discontinuity for an arithmetic 𝒢 ≤ GL(2, ℝ), and the image of a finite-index Γ ≤ SL(2, ℤ) is arithmetic, so both shapes reach Finite through this instance alone. The stabiliser of a point under SL(2, ℤ) itself is not one of those shapes — SL(2, ℤ) is a type, not a Subgroup (GL (Fin 2) ℝ), so there is no ProperlyDiscontinuousSMul SL(2, ℤ) ℍ to apply — and stays with the hand-proved TauCeti.ModularGroup.finite_stabilizer.

instance TauCeti.finite_stabilizer_of_properlyDiscontinuousVAdd {G : Type u_1} {T : Type u_2} [AddGroup G] [TopologicalSpace T] [AddAction G T] [ProperlyDiscontinuousVAdd G T] (x : T) : Finite ↥(AddAction.stabilizer G x)

A properly discontinuous additive action has finite point stabilisers, as a Finite instance. Mathlib's ProperlyDiscontinuousVAdd.finite_stabilizer states it as Set.Finite of the stabiliser's carrier, which does not drive typeclass search; this bridges it once.

theorem TauCeti.countable_of_properlyDiscontinuousSMul (G : Type u_1) {T : Type u_2} [TopologicalSpace T] [SMul G T] [ProperlyDiscontinuousSMul G T] [SigmaCompactSpace T] [Nonempty T] : Countable G

A properly discontinuous scalar family on a nonempty σ-compact space is countable. Each element carries a chosen point x₀ into one of countably many compact sets Kₙ ∋ x₀, and only finitely many elements move a given Kₙ to meet itself.

theorem TauCeti.countable_of_properlyDiscontinuousVAdd (G : Type u_1) {T : Type u_2} [TopologicalSpace T] [VAdd G T] [ProperlyDiscontinuousVAdd G T] [SigmaCompactSpace T] [Nonempty T] : Countable G

A properly discontinuous additive scalar family on a nonempty σ-compact space is countable.

theorem TauCeti.locallyFinite_smul_of_isCompact {Γ : Type u_1} {T : Type u_2} [TopologicalSpace T] [SMul Γ T] [ProperlyDiscontinuousSMul Γ T] {S : Set T} [WeaklyLocallyCompactSpace T] (hS : IsCompact S) : LocallyFinite fun (γ : Γ) => γ • S

The translates of a compact set under a properly discontinuous action are locally finite, in the sense of Katok (Fuchsian groups, geodesic flows on surfaces of constant negative curvature and symbolic coding of geodesics, Clay Math. Proc. 10 (2010), Definition 8.2, p. 27): every point has a neighbourhood meeting only finitely many of them.

theorem TauCeti.locallyFinite_vadd_of_isCompact {Γ : Type u_1} {T : Type u_2} [TopologicalSpace T] [VAdd Γ T] [ProperlyDiscontinuousVAdd Γ T] {S : Set T} [WeaklyLocallyCompactSpace T] (hS : IsCompact S) : LocallyFinite fun (γ : Γ) => γ +ᵥ S

The translates of a compact set under a properly discontinuous additive action are locally finite.

theorem TauCeti.isClosed_iUnion_smul_of_isCompact {G : Type u_1} {T : Type u_2} [TopologicalSpace T] [Group G] [MulAction G T] [ContinuousConstSMul G T] [ProperlyDiscontinuousSMul G T] [WeaklyLocallyCompactSpace T] {S : Set T} (hS : IsCompact S) (hS' : IsClosed S) : IsClosed (⋃ (g : G), g • S)

The union of the translates of a closed compact set under a properly discontinuous action is closed.

theorem TauCeti.isClosed_iUnion_vadd_of_isCompact {G : Type u_1} {T : Type u_2} [TopologicalSpace T] [AddGroup G] [AddAction G T] [ContinuousConstVAdd G T] [ProperlyDiscontinuousVAdd G T] [WeaklyLocallyCompactSpace T] {S : Set T} (hS : IsCompact S) (hS' : IsClosed S) : IsClosed (⋃ (g : G), g +ᵥ S)

The union of the translates of a closed compact set under a properly discontinuous additive action is closed.