The Nielsen class of $(2,23A,23B)$ in $M_{23}$

Definition

MathieuM23_Nielsen

by Lucas · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

group-theoryinverse-galois-problemmathieu-groupnielsen-class

Let $C_1, C_2, C_3$ be the $M_{23}$ -conjugacy classes of $g_1, g_2, g_3$ respectively. In the source's labelling these are the classes $2$ , $23A$ , $23B$ . Define

\Sigma_c=\{(h_1,h_2,h_3)\in C_1\times C_2\times C_3:\ h_1h_2h_3=1,\ \langle h_1,h_2,h_3\rangle=M_{23}\},

and let the Nielsen class $\mathrm{Ni}_c$ be the set of orbits of $\Sigma_c$ under simultaneous conjugation $(h_1,h_2,h_3)\mapsto(kh_1k^{-1},kh_2k^{-1},kh_3k^{-1})$ , $k\in M_{23}$ .

By the Riemann existence theorem, $\mathrm{Ni}_c$ is in bijection with the $M_{23}$ -covers of $\mathbb{P}^1_{\mathbb{C}}$ branched over three points with local monodromy $(2,23A,23B)$ .

Formalization Note The classes are defined through the representatives $g_1,g_2,g_3$ , and orbits are represented as subsets of the set of triples.

Definition code

import Definitions.Def_MathieuM23_Group

/-!
# The Nielsen class of the class triple `(2, 23A, 23B)` of `M₂₃` (§2.3 and §3)

The classes `C₁ = 2`, `C₂ = 23A`, `C₃ = 23B` are the `M₂₃`-conjugacy classes of
`g₁`, `g₂`, `g₃` respectively.
-/

namespace MathieuM23

/-- Simultaneous conjugation of a triple of permutations by `k`. -/
def conjTriple (k : Equiv.Perm (Fin 23))
    (x : Equiv.Perm (Fin 23) × Equiv.Perm (Fin 23) × Equiv.Perm (Fin 23)) :
    Equiv.Perm (Fin 23) × Equiv.Perm (Fin 23) × Equiv.Perm (Fin 23) :=
  (k * x.1 * k⁻¹, k * x.2.1 * k⁻¹, k * x.2.2 * k⁻¹)

/-- `Σ_c`: triples `(h₁, h₂, h₃) ∈ C₁ × C₂ × C₃` with `h₁ h₂ h₃ = 1` that generate `M₂₃`. -/
def sigmaC : Set (Equiv.Perm (Fin 23) × Equiv.Perm (Fin 23) × Equiv.Perm (Fin 23)) :=
  {x | x.1 ∈ classIn g₁ ∧ x.2.1 ∈ classIn g₂ ∧ x.2.2 ∈ classIn g₃ ∧
    x.1 * x.2.1 * x.2.2 = 1 ∧ Subgroup.closure {x.1, x.2.1, x.2.2} = M23}

/-- The Nielsen class `Ni_c = Inn(M₂₃) \ Σ_c`, as the set of orbits of `Σ_c` under simultaneous
conjugation by elements of `M₂₃`. -/
def nielsenClass :
    Set (Set (Equiv.Perm (Fin 23) × Equiv.Perm (Fin 23) × Equiv.Perm (Fin 23))) :=
  (fun x => {y | ∃ k ∈ M23, y = conjTriple k x}) '' sigmaC

end MathieuM23

Source

X. Huang, B. Jackson, K.-H. Lee, B. Poonen, R. Pries, S. Zhang, *The Mathieu group M23 is a Galois group over Q*, arXiv:2608.08538v1 (2026), https://arxiv.org/abs/2608.08538, p. 4, §2.3 (definitions of

\bar\Sigma_c

\Sigma_c

\mathrm{Ni}_c

) and §3 (the classes

2, 23A, 23B

and the triple

(g_1,g_2,g_3)\in\Sigma_c

)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; non-blind

Disclosure — NON-BLIND read-back. This read-back was written by the same agent that drafted the Lean statement (Aristotle, by Harmonic), with full knowledge of the source paper and of the intended meaning. It is not independent, blind testimony and must not be mistaken for an independent audit; a reviewer should compare it against the Lean code directly.

Everything takes place in the group $S$ of permutations of $\{0,\dots,22\}$ , with $M_{23}=\langle g_1,g_2\rangle$ and $\mathrm{cl}(g)=\{kgk^{-1}:k\in M_{23}\}$ as in the group definition file.

Simultaneous conjugation. For $k\in S$ (any permutation, not only in $M_{23}$ ) and a triple $x=(x_1,x_2,x_3)\in S^3$ , $\kappa_k(x)=(kx_1k^{-1},\,kx_2k^{-1},\,kx_3k^{-1})$ .
The set $\Sigma_c$ is the set of triples $(h_1,h_2,h_3)\in S^3$ $(h_{1}, h_{2}, h_{3}) \in S^{3}$ such that all of the following hold:
- $h_1\in\mathrm{cl}(g_1)$ , $h_2\in\mathrm{cl}(g_2)$ , $h_3\in\mathrm{cl}(g_3)$ ;
- $h_1h_2h_3=1$ (composition, $h_3$ applied first);
- the subgroup of $S$ generated by $\{h_1,h_2,h_3\}$ is exactly $M_{23}$ .
The Nielsen class is a set of subsets of $S^3$ . It is the image of $\Sigma_c$ under the map $x\mapsto\{y\in S^3:\exists k\in M_{23},\ y=\kappa_k(x)\}$ . In other words it is the collection of $M_{23}$ -conjugation orbits of elements of $\Sigma_c$ , where each orbit is the full orbit in $S^3$ , which automatically stays inside $\Sigma_c$ .

No claim is made about the size of either set.

Human review

Endorsed by Shuze Chen · Oct 5, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

The Nielsen class of (2,23A,23B)(2,23A,23B)(2,23A,23B) in M23M_{23}M23​

The Nielsen class of $(2,23A,23B)$ in $M_{23}$