Mathieu group M₂₃

DefinitionThe standard 23-cycle in \(M_{23}\)#✓fully proved

The permutation of \(\{0, 1, \dots, 22\}\) that sends \(i\) to \(i + 1\) for \(i < 22\) and sends \(22\) to \(0\), that is, the 23-cycle \((0\ 1\ 2\ \cdots\ 22)\). It is the first of the two standard generators of the Mathieu group \(M_{23}\).

def m23Cycle : Equiv.Perm (Fin 23) :=
  (List.finRange 23).formPerm

Used by 2

Used byThe Mathieu group \(M_{23}\) · Subgroups containing \(M_{23}\)

DefinitionThe standard product of four 5-cycles in \(M_{23}\)#✓fully proved

The permutation of the points \(\{0, 1, \dots, 22\}\) given by the product of the four disjoint 5-cycles \((2\ 16\ 9\ 6\ 8)(3\ 12\ 13\ 18\ 4)(7\ 17\ 10\ 11\ 22)(14\ 19\ 21\ 20\ 15)\), where a cycle \((a_1\ a_2\ \cdots\ a_5)\) sends \(a_k\) to \(a_{k+1}\) for \(k < 5\) and sends \(a_5\) to \(a_1\). It fixes the three remaining points \(0\), \(1\) and \(5\), and it is the second of the two standard generators of the Mathieu group \(M_{23}\).

def m23FiveCycles : Equiv.Perm (Fin 23) :=
  ([2, 16, 9, 6, 8] : List (Fin 23)).formPerm *
    ([3, 12, 13, 18, 4] : List (Fin 23)).formPerm *
    ([7, 17, 10, 11, 22] : List (Fin 23)).formPerm *
    ([14, 19, 21, 20, 15] : List (Fin 23)).formPerm

Used by 2

Used byThe Mathieu group \(M_{23}\) · Subgroups containing \(M_{23}\)

DefinitionThe Mathieu group \(M_{23}\)#✓fully proved

The subgroup of the symmetric group on \(\{0, 1, \dots, 22\}\) generated by the standard 23-cycle \((0\ 1\ 2\ \cdots\ 22)\) and the standard product of four disjoint 5-cycles \((2\ 16\ 9\ 6\ 8)(3\ 12\ 13\ 18\ 4)(7\ 17\ 10\ 11\ 22)(14\ 19\ 21\ 20\ 15)\).

def M23 : Subgroup (Equiv.Perm (Fin 23)) :=
  Subgroup.closure {m23Cycle, m23FiveCycles}

Uses 2 · Used by 1

Statement usesThe standard 23-cycle in \(M_{23}\) · The standard product of four 5-cycles in \(M_{23}\)

Used bySubgroups containing \(M_{23}\)

TheoremSubgroups containing \(M_{23}\)#✓fully proved

A subgroup \(H\) of the symmetric group on \(\{0, 1, \dots, 22\}\) contains the Mathieu group \(M_{23}\) if and only if \(H\) contains both the standard 23-cycle and the standard product of four 5-cycles that generate \(M_{23}\).

theorem m23_le_iff (H : Subgroup (Equiv.Perm (Fin 23))) :
    M23 ≤ H ↔ m23Cycle ∈ H ∧ m23FiveCycles ∈ H

Uses 3

Statement usesThe Mathieu group \(M_{23}\) · The standard 23-cycle in \(M_{23}\) · The standard product of four 5-cycles in \(M_{23}\)

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.