The last few weeks, I started my self-education in proof formalization (in Lean) by a test case, the simplicity of the alternating group. In this blog post, I want to discuss some aspects of the underlying mathematics which I think I learnt during the formalization process.
Simple groups. Some examples
This is about groups, eventually finite groups. Let us recall that a subgroup $N$ of a group $G$ is normal if for every $g \in G$ and $n\in N$, one has $gng^{-1}\in N$. Concretely, this means that the two equivalence relations modulo $N$ (left or right) coincide, and that the quotient set $G/N$ inherits a group structure that makes the natural projection $G \to G/N$ a morphism of groups.
In this setting, the group $G$ can be viewed as an extension of the two groups $G/N$ and $N$, which are possibly simpler, and this extension may help at understanding properties of the group $G$. At the opposite, one says that $G$ is simple if it has no normal subgroup besides $\{e\}$ and $G$ itself (and if $G\neq\{e\}$).
Trivial examples of normal subgroups of a group $G$ are $\{e\}$ and $G$ itself. Less trivial examples are the center $Z(G)$ of $G$ (those elements $g$ such that $gh=hg $ for all $h\in G$), and the derived subgroup $D(G)$, the subgroup generated by all commutators $ghg^{-1}h^{-1}$. This commutator subgroup is interesting: any subgroup $N$ of $G$ containing the commutator subgroup $D(G)$ is normal, and the quotient is abelian; and conversely.
The kernel of a group morphism is a normal subgroup, and the construction of a quotient shows that all normal subgroups appear in this way. In particular, the alternating group $A_n$ is a normal subgroup of the symmetric group $S_n$.
A simple group has either $Z(G)=\{e\}$ or $Z(G)=G$; in the latter case, this means that $G$ is commutative, and it quickly appears that $G$ has to be finite of prime order. Consequently, our discussion will now concern groups with trivial center.
The concept of simplicity of groups is classically presented in connection with Galois theory, and the question of solvability of equations by radicals. Namely, a “general” polynomial equation of degre $n$ has $S_n$, the full symmetric group on $n$ elements, for its Galois group, and, if $n\geq 5$, the only possible dévissage of this group consists in introducing the alternating group $A_n$ of even permutations, the subgroup $A_n$ being normal and simple. On the other hand, the solvability of polynomial equation by radicals is equivalent to such a dévissage where all successive quotients are cyclic groups (equivalently abelian groups). Since $A_n$ is not abelian, this implies that a “general” polynomial equation of degree $n$ is not solvable by radicals. However, using simplicity of the alternating group is much stronger than what we need: what would be needed is solvability of the symmetric group, and that this does not hold if $n\geq 5$ is much simpler. Consequently, for the problem of resolution by radicals, it suffices to prove that the derived subgroup $D(A_n)$ of the alternating group is equal to $A_n$.
Theorem. — For $n\geq 5$, one has $D(A_n)=A_n$. In particular, the alternating group and the symmetric group on $n$ letters are not solvable.
I give two (equivalent) proofs, the second one being a computational interpretation of the first one. Both use that the 3-cycles generate $A_n$ and are conjugate in $A_n$. The computational proof is shorter, arguingly simpler. As a matter of fact, I never understood it, nor could remember it, until I translated the conceptual proof into the proof assistant.
Consider the morphism $p\colon A_n\to A_n/D(A_n)$. Since $A_n/D(A_n)$ is commutative, all 3-cycles have the same image. Since the square of a 3-cycle is again a 3-cycle, both have the same image. This implies that for every 3-cycle $g\in A_n$, one has $p(g)=p(g^2)$, hence $p(g)=e$. Since the 3_cycles generate $A_n$, the morphism $p$ is trivial; since it is surjective, one has $A_n/D(A_n)=\{e\}$ and $D(A_n)=A_n$.
Computationally, consider a 3-cycle $g$ and its square $g^2$. Since they are conjugate, there exists $h\in A_n$ such that $g^2=hgh^{-1}$. Then $g=hgh^{-1}g^{-1}$, so that $g$ is a commutator; in particular, $D(A_n)$ contains all commutators and $D(A_n)=A_n$.
The remaining cases, for $n\leq 4, are interesting, but classically left as exercises in text books:
- One has $A_1=S_1=\{e\}$;
- The group $S_2$ is the cyclic group of order 2, hence is simple and solvable, and $A_2$ is trivial;
- The group $S_3$ is a noncommutative group of order 6, and $A_3$ is a cyclic group of order 2.
- The groups $S_4$ and $A_4$ are noncommutative and solvable, of orders 24 and 12. The derived subgroups $D(S_4)$ and $D(A_4)$ are both equal to the Klein subgroup $V_4$ of $S_4$, consisting of the permutations of the form $(ab)(cd)$ for $a,b,c,d$ any enumeration of $1,2,3,4$ — “double transpositions” – and of the identity. The group $V_4$ is commutative, isomorphic to $(\mathbf Z/2\mathbf Z)^2$, and the quotient $D(A_4)/V_4$ is cyclic of order $3$.
Another classical series of simple groups appears in linear algebra. Let $F$ be a field and let $n$ be an integer such that $n\geq 2$. The group $\mathrm{GL}(n,F)$ of $n\times n$ invertible matrices is not simple, for it is noncommutative but its center consists of homotheties; we can try to mod out by the center, getting the group $\mathrm{PGL}(n,F)=\mathrm{GL}(n,F)/F^\times$ but that one may not be simple. Indeed, another reason for $\mathrm{GL}(n,F)$ not to be simple is that it admits the special linear group $\mathrm{SL}(n,F)$, kernel of determinant, as a normal subgroup. The group $\mathrm{SL}(n,F)$ has a nontrivial center in general, it consists of homotheties of ratio $a\in F^\times$ such that $a^n=1$ — let us denote it by $\mu_n$. But the quotient $\mathrm{PSL}(n,F)=\mathrm{SL}(n,F)/\mu_n$ is simple in general — in general meaning that is is always the case but for two exceptions:
- $n=2$ and $F=\mathbf F_2$. Then $\mathrm{PSL}(2,\mathbf F_2)\simeq S_3$ (by the action on $\mathbf P_1(\mathbf F_2)$, see below), hence is not simple.
- $n=2$ and $F=\mathbf F_3$. Then $\mathrm{PSL}(2,\mathbf F_3)\simeq S_4$ (again by the action on $\mathbf P_1(\mathbf F_3)$), and is not simple.
Bilinear algebra gives rise to new groups, orthogonal, unitary and symplectic, which also furnish simple groups up to elementary transformations. By the famous “classification of finite simple groups”, these constructions furnish all finite simple groups, up to 26 (or 27) examples called sporadic groups. This remarkable theorem has a fantastic proof, encompassing thousands of pages across the years 1960-2010.
But the question here is: How can one prove that a given group is simple?
Alternating groups
There is a large supply of proofs that the alternating group $A_n$ is simple for $n\geq 5$. Here is a sketch of one.
Let $N$ be a normal subgoup of $A_n$ ($n\geq 5$) and assume that $N\neq\{e\}$. An element of $A_n$ can be written as a product of an even number of transpositions. If two successive permutations in the product are equal, we can cancel them; if the share exactly one a common member, as in $(a\,b)(a\,c)$, their product is a 3-cycle $(a\,c\,b)$; if they have no common member, their product is a double transposition. On the other hand, if $n\geq 5$, we can either insert $(b\,c)(b\,c)$ in the product $(a\,b)(c\,d)$, writing a double transposition as a product of two 3-cycles, or insert $(d\,e)(d\,e)$ in the product $(a\,b)(a\,c)$, writing a 3-cycle as a product of two double transpositions. Consequently, $A_n$ is generated by, either the 3-cycles, or the double transpositions. Moreover, since $n\geq 5$, we can check that 3-cycles are pairwise conjugate, and similarly for double transpositions; consequently, if the normal subgroup $N$ of $A_n$ contains either a 3-cycle, or a double transposition, it will contain all of them, hence be equal to $A_n$.
When $n=5$, the only case that remains to consider is when $N$ contains a 5-cycle, say $g=(1\,2\,3\,4\,5)$. Conjugating $g$ by the 3-cycle $h=(4\,5\,1)$, we get $hgh^{-1}=(h1\,h2\,h3\,h4\,h5)=(4\,2\,3\,5\,1)\in N$. By construction, this element behaves as $g$ on $5$, but differs. Consequently, the commutator $hgh^{-1}g^{-1}$ is a nontrivial element of $N$ that fixes $5$. By the first two cases, one has $N=A_5$.
A similar argument works in general, arguing by descending induction on the cardinality on the fixed point set of an element $g\neq e$ of $N$. One considers an element $h$ of $A_n$ and the conjugate $hgh^{-1}$; if $g=(a_1\,a_2\,\dots)(b_1\,b_2\,\dots)\dots$, then $hgh^{-1}=(ha_1\,ha_2\,\dots)(hb_1\,hb_2\,\dots)\dots$ is an element of $N$ that behaves as $g$ on many elements, but not all. Consquently, $hgh^{-1}g^{-1}$ is a non trivial element of $N$ that fixes more elements than $g$, and we conclude by induction. (Details can be found in James Milne's lectures, 4.34.)
The Iwasawa criterion
In 1941, Kenkiti Iwasawa published a proof of the simplicity of the projective special linear group. From this proof, a general criterion for simplicity has been abstracted:
Theorem (Iwasawa). — Let $G$ be a group with a primitive action on a set $X$. Assume that one is given, for every $x\in X$, a subgroup $T(x)$ of $G$ satisfying the following properties:
Then any normal subgroup $N$ of $G$ that acts nontrivially on $X$ contains the commutator subgroup of $G$. In particular, if $G=D(G)$, then $G$ is simple.
There are two classical ways to state that the action is primitive. The simplest states that it is transitive and that the stabilizers of points are maximal subgroups of $G$. Another is that there is no imprimitivity block, a nontrivial partition $(X_i)$ of $X$ such that for every $g\in G$ and every $i$, there exist $j$ such that $g\cdot X_i=$X_j$. One can prove that a 2-transitive action (= transitive on ordered pairs of distinct elements) is primitive.
Iwasawa applies his criterion to $G=\mathrm{SL}(n,F)$ acting on the projective space $\mathbf P_{n-1}(F)$ of lines in $F^n$. Except when $n=2$ and $F$ has 2 or 3 elements, this action is 2-transitive, hence primitive. For a nonzero $x\in F^n$, one considers the group $T(x)$ of linear transformations of the form $y\mapsto y + \phi(y) x$ (transvections), for all linear forms $\phi$ on $F^n$ such that $\phi(x)=0$. They constitute a commutative subgroup of $\mathrm{SL}(n,F)$ (isomorphic, as a group, to $F^{n-1}$). The map $T$ gives rise to the data as in Iwasawa's theorem. Consequently, every normal subgroup $N$ of $\mathrm{SL}(n,F)$ that acts nontrivially on $\mathbf P_{n-1}(F)$ contains the commutator subgroup of $\mathrm{SL}(n,F)$, which is $\mathrm{SL}(n,F)$. Explicitly, either $N$ consists of homotheties, or $N$ contains $\mathrm{SL}(n,F)$. This implies that $\mathrm{PSL}(n,F)$ is simple.
Applying the Iwasawa criterion for symmetric groups
One may wish to apply the Iwasawa criterion to the symmetric group. However, the conclusion is not as nice as what I had hoped initially.
Let $S_n$ act on the set of 2-element subsets of $X=\{1,\dots,n\}$. If $n\geq 5$, the action is primitive. This is not completely obvious, because it this action is not 2-transitive (you cannot map $\{1,2\}$ and $\{1,3\}$ to $\{1,2\}$ and $\{3,4\}$)! Its primitivity means that stabilizers are maximal subgroups, and one can prove that the stabilizer of a 2-element subset is indeed maximal unless $n=4$. It is also faithful (no nontrivial acts trivially). To a pair $\{a,b\}$, associate the subgroup of order 2 generated by the transposition $(a\,b)$. It satisfies the criterion, and this shows that the nontrivial normal subgroups of $S_n$ contain $D(S_n)=A_n$. Since $A_n$ has index 2, this shows $N=A_n$ or $N=S_n$.
It is interesting to guess how the criterion breaks for $n=4$. In fact, the action of $S_4$ on pairs is transitive, but not primitive: the stabilizer of $\{1,2\}$ is a subgroup of $S_4$ of order $4$, consisting of the identiy, two transpositions $(1\,2)$ and $(3\,4)$, and their product. Since $\mathrm{Card}(S_4)=24!=2^3\cdot 3$, this subgroup is contained in a 2-sylow subgroup, of order 8, so is not maximal.
However, and I find it unfortunate, this proof does not imply that the alternating group $A_n$ is simple for $n\geq 5$. To prove the simplicity of $A_n$ along these lines, we need to consider the following actions.
- Let $A_n$ act on the set $X_3$ of 3-element subsets of $X$. For $x=\{a,b,c\}\in X_3$, consider the subgroup $T(x)$ of order 3 of $A_n$ consisting of the identity and the 3-cycles $(a\,b\,c)$ and $(a\,c\,b)$. (It is the alternating group on $x$, viewed as a subgroup of $A_n$.) The Iwasawa criterion applies provided the action is primitive, which presumably holds for $n>6$. Consequently, $A_n$ is simple for $n\geq 7$. However, if $n=6$, the stabilizer of $\{1,2\,3\}$ in $A_6$ is not maximal, for a reason analogous to the one explained for $S_4$.
- Let $A_n$ act on the set $X_4$ of 4-element subsets of $X$. For $x\in X_4$, we can consider the Klein subgroup $T(x)$ of $A_4$, acting on $x$, viewed as a subgroup of $A_n$. I hope that the action is primitive, except for $n=8$, and this would prove that $A_n$ is simple for $n\geq 8$. This uses that double transpositions generate $A_n$.
- One can improve the two preceding arguments a little bit. If $n=5$, we can have $A_n$ act on $X_2$, associating with $x$ the alternating group on the three remaining letters. Therefore, $A_5$ is simple (the action is primitive because the stabilizer of a point is the Klein subgroup of $A_4$, as a subgroup of $A_5$, its cardinality is 12, that of $A_5$ is 60, and since 60/12=5 is prime, the Klein subgroup of $A_4$ is maximal in $A_5$). Similarly, if $n=6$, we have $A_6$ act on $X_2$, associating with $x\in X_2$ the Klein subgroup corresponding to the four remaining letters. Provided one can prove that the stabilizer of a pair in $A_6$ is a maximal subgroup, this gives a proof that $A_6$ is simple!
The primitivity assertions seem to hold. In fact, maximal subgroups of $A_n$ and $S_n$ are classified by the O'Nan–Scott theorem. Those we're concerned with have type (a) in the notation of (Liebeck, Praeger, Saxl, 1987. “A Classification of the Maximal Subgroups of the Finite Alternating and Symmetric Groups.” Journal of Algebra 111 (2): 365–83. DOI:10.1016/0021-8693(87)90223-7), and according to Theorem 1 of that paper, the relevant subgroups are indeed maximal.
Formalization: where am I now?
I have already formalized the Iwasawa criterion in Lean (there's an ongoing pull request for this), as well as the result that the normal subgroups of $S_n$ are $\{e\}$, $A_n$ and $S_n$ for $n\geq 5$.
It remains to formalize the rest of the proof, and the main difficulty will be in proving primitivity, plus some nice way of defining the maps $T$ so that their properties are visible.
I also wish to formalize the simplicity of the special linear group along these lines, and it should be ready for an application to orthogonal, unitary or symplectic groups as well.
Great Stuff i wish i could learn this
ReplyDelete