Discrete subgroups act properly discontinuously and have infinite index

A discrete subgroup S of a T₁ topological group G is closed, so it meets every compact set of G in a finite set. Hence S acts properly discontinuously on G by left multiplication. Mathlib proves this from the hypothesis that the inclusion S → G tends to the cocompact filter along the cofinite filter (Subgroup.properlyDiscontinuousSMul_of_tendsto_cofinite); this file records it as an instance for subgroups carrying the discrete topology, and for discrete submodules of a topological module acting by translation, such as a lattice in a real or complex vector space.

A discrete subgroup of finite index in a Hausdorff topological group makes the whole group discrete (Subgroup.discreteTopology_iff_of_finiteIndex). So when the group has no isolated points, for instance a nonzero real or complex vector space, every discrete subgroup has infinite index. In particular the orbit space of translation by a discrete submodule, such as a complex torus E / L with E ≠ 0, is infinite.

Main results

• Subgroup.properlyDiscontinuousSMul_of_discreteTopology, AddSubgroup.properlyDiscontinuousVAdd_of_discreteTopology: a discrete subgroup acts properly discontinuously on the ambient group.
• Submodule.properlyDiscontinuousVAdd_of_discreteTopology: a discrete submodule acts properly discontinuously on the ambient module by translation.
• Subgroup.infinite_quotient_of_discreteTopology, AddSubgroup.infinite_quotient_of_discreteTopology: a discrete subgroup of a Hausdorff group without isolated points has infinite index.
• Submodule.instInfiniteOrbitRelQuotient: the orbit space of translation by a discrete submodule of a Hausdorff topological module without isolated points is infinite.

instance Subgroup.properlyDiscontinuousSMul_of_discreteTopology {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [T1Space G] (S : Subgroup G) [DiscreteTopology ↥S] : ProperlyDiscontinuousSMul (↥S) G

A discrete subgroup of a T₁ topological group acts properly discontinuously on the group by left multiplication.

instance AddSubgroup.properlyDiscontinuousVAdd_of_discreteTopology {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [T1Space G] (S : AddSubgroup G) [DiscreteTopology ↥S] : ProperlyDiscontinuousVAdd (↥S) G

A discrete additive subgroup of a T₁ additive topological group acts properly discontinuously on the group by translation.

instance Submodule.properlyDiscontinuousVAdd_of_discreteTopology {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [T1Space M] (p : Submodule R M) [DiscreteTopology ↥p] : ProperlyDiscontinuousVAdd (↥p) M

A discrete submodule of a T₁ topological module acts properly discontinuously on the module by translation.

theorem Subgroup.infinite_quotient_of_discreteTopology {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] [(nhdsWithin 1 {1}ᶜ).NeBot] (H : Subgroup G) [DiscreteTopology ↥H] : Infinite (G ⧸ H)

A discrete subgroup of a group without isolated points has infinite index. A discrete subgroup of finite index in a Hausdorff topological group makes the group itself discrete (Subgroup.discreteTopology_iff_of_finiteIndex).

theorem AddSubgroup.infinite_quotient_of_discreteTopology {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [T2Space G] [(nhdsWithin 0 {0}ᶜ).NeBot] (H : AddSubgroup G) [DiscreteTopology ↥H] : Infinite (G ⧸ H)

A discrete subgroup of an additive group without isolated points has infinite index. A discrete subgroup of finite index in a Hausdorff additive topological group makes the group itself discrete (AddSubgroup.discreteTopology_iff_of_finiteIndex).

instance Submodule.instInfiniteOrbitRelQuotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace M] [IsTopologicalAddGroup M] [T2Space M] [(nhdsWithin 0 {0}ᶜ).NeBot] (p : Submodule R M) [DiscreteTopology ↥p] : Infinite (AddAction.orbitRel.Quotient (↥p) M)

The orbit space of translation by a discrete submodule of a Hausdorff topological module without isolated points is infinite, since the submodule has infinite index (AddSubgroup.infinite_quotient_of_discreteTopology). For instance, a complex torus E / L with E ≠ 0 is infinite.