Praeger's theorem on bounded movement #
Let a group act on a set Ω without fixed points, and let every finite subset that some element
moves off itself have at most m ≥ 1 points. Then Ω is finite, there are at most 2m − 1 orbits,
each orbit has at most 3m points, and |Ω| ≤ 3m + t − 1 (Theorem of the Day; Praeger 1991).
Proof: every element has support of size at most 3m (it lies in A ∪ gA ∪ g⁻¹A for a maximal set
A moved off itself), and the orbit-counting identity Σ_g |supp g| = |G| (|Ω| − t) gives the
bounds.
Main results #
Praeger.card_support_le: every element has at most 3m moved pointsPraeger.bounded_movement: Praeger's bounds: Ω finite, t ≤ 2m − 1, orbits ≤ 3m, |Ω| ≤ 3m + t − 1
References #
- R. Whitty, Theorem of the Day, «Praeger's Theorem on Bounded Movement» (GroupTheory/Movement).
- C. E. Praeger, On permutation groups with bounded movement, J. Algebra 144 (1991) 436–442.
theorem
Praeger.card_eq_sum_orbits
(H : Type u_1)
(X : Type u_2)
[Group H]
[MulAction H X]
[Finite X]
[Fintype (MulAction.orbitRel.Quotient H X)]
:
def
Praeger.inducedSubgroup
(G : Type u_3)
[Group G]
{Ω : Type u_4}
[MulAction G Ω]
(U : Set Ω)
:
Subgroup (Equiv.Perm ↑U)
The elements of Perm U induced by elements of G.
Equations
Instances For
theorem
Praeger.card_union_le
{G : Type u_1}
{Ω : Type u_2}
[Group G]
[MulAction G Ω]
(m : ℕ)
(hm : 1 ≤ m)
(hmove : ∀ (Γ : Finset Ω) (g : G), (∀ x ∈ Γ, g • x ∉ Γ) → Γ.card ≤ m)
(U : Set Ω)
(hU : U.Finite)
(hcov : ∀ x ∈ U, ∃ (g : G), g • x ≠ x ∧ {y : Ω | g • y ≠ y} ⊆ U)
:
A finite set covered by supports contained in itself has at most 6m points.
theorem
Praeger.finite_of_hmove
{G : Type u_1}
{Ω : Type u_2}
[Group G]
[MulAction G Ω]
(m : ℕ)
(hm : 1 ≤ m)
(hfix : ∀ (x : Ω), ∃ (g : G), g • x ≠ x)
(hmove : ∀ (Γ : Finset Ω) (g : G), (∀ x ∈ Γ, g • x ∉ Γ) → Γ.card ≤ m)
:
Finite Ω
Finiteness of Ω (B.4): a maximal finite union of supports contains all supports.