Properly discontinuous actions of subgroups #
theorem
Subgroup.properlyDiscontinuousSMul_of_le
{Γ : Type u_1}
{α : Type u_2}
[Group Γ]
[TopologicalSpace α]
[SMul Γ α]
{G H : Subgroup Γ}
(hG : ProperlyDiscontinuousSMul (↥G) α)
(hGH : H ≤ G)
:
ProperlyDiscontinuousSMul (↥H) α
theorem
AddSubgroup.properlyDiscontinuousVAdd_of_le
{Γ : Type u_1}
{α : Type u_2}
[AddGroup Γ]
[TopologicalSpace α]
[VAdd Γ α]
{G H : AddSubgroup Γ}
(hG : ProperlyDiscontinuousVAdd (↥G) α)
(hGH : H ≤ G)
:
ProperlyDiscontinuousVAdd (↥H) α
instance
instProperlyDiscontinuousSMulSubtypeMemSubgroup
{Γ : Type u_1}
{α : Type u_2}
[Group Γ]
[TopologicalSpace α]
[SMul Γ α]
[ProperlyDiscontinuousSMul Γ α]
(G : Subgroup Γ)
:
ProperlyDiscontinuousSMul (↥G) α
If Γ acts properly discontinuously, so does every subgroup of Γ.
instance
instProperlyDiscontinuousVAddSubtypeMemAddSubgroup
{Γ : Type u_1}
{α : Type u_2}
[AddGroup Γ]
[TopologicalSpace α]
[VAdd Γ α]
[ProperlyDiscontinuousVAdd Γ α]
(G : AddSubgroup Γ)
:
ProperlyDiscontinuousVAdd (↥G) α
theorem
ProperlyDiscontinuousSMul.ofFiniteRelIndex
{Γ : Type u_1}
{α : Type u_2}
[Group Γ]
[TopologicalSpace α]
[MulAction Γ α]
[ContinuousConstSMul Γ α]
(G H : Subgroup Γ)
[hH : ProperlyDiscontinuousSMul (↥H) α]
[H.IsFiniteRelIndex G]
:
ProperlyDiscontinuousSMul (↥G) α
If G, H are subgroups of Γ which acts on α, and G ∩ H has finite index in G,
then G acts properly discontinuously if H does.
theorem
ProperlyDiscontinuousVAdd.ofFiniteRelIndex
{Γ : Type u_1}
{α : Type u_2}
[AddGroup Γ]
[TopologicalSpace α]
[AddAction Γ α]
[ContinuousConstVAdd Γ α]
(G H : AddSubgroup Γ)
[hH : ProperlyDiscontinuousVAdd (↥H) α]
[H.IsFiniteRelIndex G]
:
ProperlyDiscontinuousVAdd (↥G) α
theorem
Subgroup.properlyDiscontinuousSMul_iff_of_isFiniteRelIndex
{Γ : Type u_1}
{α : Type u_2}
[Group Γ]
[TopologicalSpace α]
[MulAction Γ α]
[ContinuousConstSMul Γ α]
{G H : Subgroup Γ}
(hGH : G ≤ H)
[G.IsFiniteRelIndex H]
:
theorem
AddSubgroup.properlyDiscontinuousVAdd_iff_of_isFiniteRelIndex
{Γ : Type u_1}
{α : Type u_2}
[AddGroup Γ]
[TopologicalSpace α]
[AddAction Γ α]
[ContinuousConstVAdd Γ α]
{G H : AddSubgroup Γ}
(hGH : G ≤ H)
[G.IsFiniteRelIndex H]
:
theorem
Subgroup.Commensurable.properlyDiscontinuousSMul_iff
{Γ : Type u_1}
{α : Type u_2}
[Group Γ]
[TopologicalSpace α]
[MulAction Γ α]
[ContinuousConstSMul Γ α]
{G H : Subgroup Γ}
(h : G.Commensurable H)
:
theorem
AddSubgroup.Commensurable.properlyDiscontinuousVAdd_iff
{Γ : Type u_1}
{α : Type u_2}
[AddGroup Γ]
[TopologicalSpace α]
[AddAction Γ α]
[ContinuousConstVAdd Γ α]
{G H : AddSubgroup Γ}
(h : G.Commensurable H)
: