mathlib
mathlib copied to clipboard
leanprover-community
feat(group_theory/iwasawa.lean): add a proof of the Iwasawa criterion for simplicity
Add the Iwasawa criterion for simplicity. This criterion can be used in the proof of simplicity of some classical groups such as the alternating group or the projective special linear group (these applications are TODO).
I have one question about lines 202, 203, 214, where I want to use exists_ne.
Lean was not able of getting the hypothesis hX : nontrivial X by itself, so I resorted to use the full form, typing @exists_ne _ hX x form. Is there a better way to do this?
Some checks fail, I don't understand why, nor whether it's important.
As I wrote to Patrick this morning, I am self-disappointed. The plan I had to write this proof broke down 5 minutes before its conclusion. The Iwasawa criterion is formalized, it should be used to prove simplicity of PSL(n) (as Iwasawa did), but for the alternating group, what it nicely proves, and this is now formalized, is that the normal subgroups of the symmetric groups are \bot, \top, and the alternating group. I am not sure how to derive the simplicity of the alternating group from that.
Can you elaborate a bit @AntoineChambert-Loir ? The things you say are now formalized are they in this PR or somewhere else? I guess I see why knowing the normal subgroups of S_n doesn't automatically give you simplicity of A_n, but what application of Iwaswa's criterion are you using to get the normal subgroups of S_n (i.e. what set and action?).
@alexjbest It is planned to belong to this PR, but I have worked on separate files, I will push them tomorrow or next week, after some polishing, because it is quite a mess.
I applied the Iwasawa criterion (which already belongs to this PR) to the action of the symmetric_group X on pairs of elements of X, and the structure maps a pair {a,b} to the subgroup generated by the transposition equiv.swap a b. An intermediate result is that the stabilizer of such a pair is a maximal subgroup of symmetric_group X (this uses card X \geq 5!). With a proof (that I have formalized) that commutator(symmetric_group X)=alternating_group X, this proves that the normal subgroups of symmetric_group X are \top, \bot and alternating_group X, but this falls short of proving the simplicity of alternating_group X.
Presumably, one can apply the criterion to the action of alternating_group X on 3-element sets of X, mapping such a triple to the subgroup generated by the 3-cycles on this triple s (it is the subgroup of alternating_group X which fixes every element out of s). But for this I need to prove (is it only true ?) that the stabilizers are maximal subgroups of alternating_group X. Wait and see.
The files of the formalization are certainly worth of drastic refactoring. I did a lot of stuff by bare hands, probably because I don't know some idioms, or some parts of the library.
I have explained a bit of the math on the blog post : https://freedommathdance.blogspot.com/2021/12/not-simple-proofs-of-simplicity.html