Another theorem of Jordan

Stream: maths

[Antoine Chambert-Loir]

I have finally :sweat_smile: finished the formalization of the following theorem of Jordan (1871) :

A primitive subgroup of a permutation group $\mathfrak S_n$ that contains a transposition is equal to $\mathfrak S_n$; a primitive subgroup that contains a 3-cycle contains the alternating group.

(A permutation group is primitive if there are no nontrivial equivalence relations which are compatible with the action.)
The proof follows the book of Wielandt, Finite permutation groups (this is Thm 13-3). I have basically coded sections 6-10 and the beginning of section 13 of that book. The whole stuff is distributed along a bunch of files in branch#acl-Wielandt which I will now need to clean up.

I may go further and prove the stronger result (Thm 13-9).

If a primitive group contains a cycle of prime order, then it contains the alternating group.

My motivation for this was a putative proof of the simplicity of the alternating group using the Iwasawa lemma. To that aim, one needs to know that some subgroups of the alternating group are maximal, and this theorem of Jordan provides the result. Probably, this will be put together quickly.

By the way, this maximal subgroup business is (the trivial part) of a now classic result of O'Nan-Scott, with converse by Liebeck, Praeger and Saxl, that describes all maximal subgroups of an alternating/symmetric group. This may be an interesting project to formalize.