Finite permutation groups

Actions of finite groups on finite sets: Burnside-type counting, stabilizers, multiply and doubly transitive finite groups, Frobenius groups, bases and independent sets, 2-closures, regular orbits of linear actions, coverings and products in finite symmetric groups.

TheoremA subgroup stabilizing a subset has order dividing its size#✓fully proved

Let \(G\) be a finite group, let \(H\) be a subgroup of \(G\) and let \(U\) be a subset of \(G\) such that \(hu \in U\) for all \(h \in H\) and \(u \in U\). Then \(|H|\) divides \(|U|\).

The \(H\)-orbits partition \(U\) and each orbit has exactly \(|H|\) elements, since left multiplication is injective.

theorem card_stabilizer_dvd_card (H : Subgroup G) (U : Finset G)
    (hU : ∀ (h : G), h ∈ H → ∀ u ∈ U, h * u ∈ U) :
    Nat.card H ∣ U.card

TheoremBurnside's lemma with a uniform fixed-point count#✓fully proved

Let a finite group \(G\) act on a finite set \(X\), and let \(c\) be a natural number such that every element \(g \ne 1\) of \(G\) fixes exactly \(c\) points of \(X\). Writing \(N\) for the number of orbits of \(G\) on \(X\), we have \(|X| + c\,(|G| - 1) = N \cdot |G|\).

theorem _root_.MulAction.card_add_mul_card_sub_one_eq_card_orbits_mul_card
    (G X : Type*) [Group G] [MulAction G X] [Finite G] [Finite X]
    (c : ℕ) (hfixed : ∀ g : G, g ≠ 1 → Nat.card (MulAction.fixedBy X g) = c) :
    Nat.card X + c * (Nat.card G - 1) =
      Nat.card (MulAction.orbitRel.Quotient G X) * Nat.card G

Used by 1

Used byDickson's classification, tame case

TheoremFrobenius's theorem on the Frobenius kernel#●ready to prove

Let a finite group \(G\) act faithfully and transitively on a finite set \(X\) with at least two elements, such that every point stabiliser is nontrivial and no nonidentity element of \(G\) fixes two distinct points of \(X\). Then the set consisting of the identity together with the elements of \(G\) that fix no point of \(X\) is a normal subgroup of \(G\).

public theorem_wanted frobenius_kernel_isNormal
    (G X : Type) [Group G] [Fintype G] [Fintype X]
    [MulAction G X] [FaithfulSMul G X]
    (hcard : 2 ≤ Fintype.card X)
    (htrans : ∀ x y : X, ∃ g : G, g • x = y)
    (hstab : ∀ x : X, MulAction.stabilizer G x ≠ ⊥)
    (hfrob : ∀ g : G, g ≠ 1 → ∀ x y : X, g • x = x → g • y = y → x = y) :
    ∃ N : Subgroup G, N.Normal ∧
      (N : Set G) = {1} ∪ {g : G | ∀ x : X, g • x ≠ x}

Sources

G. Frobenius, Über auflösbare Gruppen IV, Sitzungsber. Akad. Wiss. Berlin (1901). Problem frobenius_kernel_isNormal of the lean-eval benchmark.

TheoremOrders of finite \(5\)-transitive permutation groups#●ready to prove

Let a finite group \(G\) act faithfully on a finite set \(X\) with \(n = |X| \ge 5\), and suppose that the action is \(5\)-transitive: for any two injective maps \(a, b \colon \{0, 1, 2, 3, 4\} \to X\) there is \(g \in G\) with \(g \cdot a(i) = b(i)\) for all \(i\). Then \(|G| = n!\), or \(n \ge 7\) and \(|G| = n!/2\), or \(n = 12\) and \(|G| = 95040\), or \(n = 24\) and \(|G| = 244823040\).

public theorem_wanted five_transitive_card_classification
    (G X : Type) [Group G] [Fintype G] [Fintype X]
    [MulAction G X] [FaithfulSMul G X]
    (hcard : 5 ≤ Fintype.card X)
    (h5 : ∀ a b : Fin 5 → X, Function.Injective a → Function.Injective b →
      ∃ g : G, ∀ i, g • a i = b i) :
    let n := Fintype.card X
    Fintype.card G = n.factorial ∨
    (7 ≤ n ∧ Fintype.card G = n.factorial / 2) ∨
    (n = 12 ∧ Fintype.card G = 95040) ∨
    (n = 24 ∧ Fintype.card G = 244823040)

Sources

Folklore via CFSG; classical work of Mathieu, Jordan; modern accounts in P. Cameron, Permutation Groups (1999). Problem five_transitive_card_classification of the lean-eval benchmark.

2 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.