The very simple proof that the alternating group on 5 letters (or more) is simple

$\def\supp {\operatorname{supp}}$

As explained in the previous post, I wanted to formalize the proof that the alternating group on 5 letters or more is simple, using the Iwasawa criterion. This formalization is in the middle of nowhere, because it requires a proof that the natural action of the alternating group $A_n$ on $k$-elements subsets of $\{1,\dots,n\}$ is primitive, provided $n\neq 2k$, $k\neq 0,n$ and $n\geq 5$.

A simple proof

There is a simple, slightly computational proof that the alternating group of 5 letters (or more) is simple, it is explained in many textbooks, for example in James Milne's Group theory notes. However, its formalization is not so easy, because even Milne has a lot of implicit stuff.

The situation, as in Lemma 4.36 of Milne's booklet, is the following.

One is given a nontrivial normal subgroup $N$ of $A_n$ and one wishes to prove that $N=A_n$. We know that the 3-cycles generate $A_n$. We also know that 3-cycles are pairwise conjugate in the symmetric group, and also, using $n\geq 5$, in the alternating group $A_n$. Consequently, it suffices to prove that $N$ contains a 3-cycle. To that aim, one argues by induction on the cardinality of the support $\supp(g)$ of a nontrivial element $g$ of $N$. 

Here is an attempt at presenting the induction argument in a way which is as straightforward as possible.

Since $g\neq 1$, $\supp(g)$ has cardinality $\geq 2$.

If $\supp(g)$ has cardinality $2$, then $g$ is a transposition, contradicting the hypothesis that $g$ belongs to the alternating group. So the support of $g$ has cardinality $\geq 3$.

If $\supp(g)$ has cardinality $3$, then $g$ is a 3-cycle, and we are done. So we may assume that the support of $g$ has cardinality $\geq 4$.

Let us choose an element $a\in\{1,\dots,n\}$ which belongs to the largest cycle of $g$ and set $b=g(a)$; by assumption, one has $b\neq a$. The proof consists in considering an element $c\in\{1,\dots,n\}$ such that $c\neq a$ and $c\neq b$, the 3-cycle $h=(a\,b\,c)$ and the conjugate $g'=h g h^{-1}$. 

Since $h$ is a 3-cycle, it belongs to the alternating group; since $N$ is normal, one has $g'\in N$.

We wish to apply the induction hypothesis to the element $g' g^{-1}$ of $N$. So we need to prove

1. $g'\neq g$, and
2. The support of $g' g^{-1}$ has cardinality strictly smaller than the one of $g$.

To guarantee (1), that $g'\neq g$, it suffices to choose $c$ such that $g'(b)\neq g(b)$. But $$g'(b) = hgh^{-1}(b) = hg(a) = h(b) = x,$$ so the new assumption we make is that $c\neq g(b)$.

The rest of the argument is devoted to finding appropriate conditions on $c$ that guarantee (2). First, observe the inclusion $\supp(g'g^{-1})\subset g(\supp(h))\cup \supp(h)$, which is proved by contraposition. Indeed, if $x$ does not belong to the right hand side, then $g^{-1}(x) \notin \supp(h)$, hence $h^{-1}g^{-1}(x)=g^{-1}(x)$ (for example, using that $\supp(h)=\supp(h^{-1})$), and then $g' g^{-1}(x)=hgh^{-1}(g^{-1}(x))=hg(g^{-1}(x))=h(x)=x$, since $x\not\in h(x)$. This proves that the cardinality of the support of $g'g^{-1}$ is at most 6.

However, since $g(a)=b$ belongs both to $g(\supp(h))$ and to $\supp(h)$, the cardinality is at most 5. Explicitly, $\supp(g'g^{-1})\subset \{a,b,c,g(b), g(c)\}$. In particular, a clever choice for $c$ is only needed when $\supp(g)$ has cardinality 4 or 5!

To conclude in the remaining cases, we remark that there are only two possibilities for the cycle-type of $g$: it can only be $(5)$ or $(2,2)$, since it is an alternating permutation, and we split the discussion according to these two cases:

• If the cycle-type of $g$ is $(5)$, then we choose for $c$ the “last” element of the cycle of $a$, namely $c=g^{-1}(a)$. Then, $g(c)=a$, so that $\supp(g'g^{-1})\subset\{a,b,c,g(b)\}$ which has at most 4 elements.
• If the cycle-type of $g$ is $(2,2)$, then we have $g(b)=a$ and we choose for $c$ any fixed point of $g$. Then $\supp(g'g^{-1})\subset\{a,b,c\}$ has at most 3 elements.

About the formalization

One annoying part for formalizing this argument is the elimination of cycle-types. One would like that a computer assistant is able to list all possible cycle-types of a given size. Presumably it can, by I cannot (yet), so I need to do the argument by hand, for that specific value.

In principle, that argument needs to be spelt out in class too. We use two formulas:

1. The sum of the length of the cycles is the cardinality of the support, hence $4$ or $5$ in this case.
2. The signature of a permutation is even if and only if the number of cycles and the cardinality of the support have the same parity.

One way to write it down consists in taking the length $m$ of the smallest cycle of $g$. One has $m\geq 2$ by assumption.

1. If there are no other cycles, then the cycle-type of $g$ is $(m)$. Then $m=4$ or $5$, and only $(5)$ respects the parity constraint.
2. Otherwise, there is only one other cycles, otherwise the sum of their lengths would be at least $3\cdot 2\geq 6$. If $m'$ is the length of that other cycle, one has $2\leq m\leq m'$. Then $2m\leq m+m'\leq 5$, hence $m\leq 2$, so that $m=2$. This gives $m'\leq 3$, giving two cycle-types $(2,3)$ and $(2,2)$, of which the second one only satisfies the parity constraint.