Iwasawa Criterion for simplicity

Stream: maths

[Antoine Chambert-Loir]

I just finished the Lean proof of the Iwasawa criterion for simplicity.
Ultimately, I will add the applications to the simplicity of the alternating group and of PSL(n,K).
(I do not know whether the latter will require a lot of stuff or not, I am not sure it is already proved that SL(n,K)
is generated by transvections.)

The file is a bit long (500 lines), but it incorporates some definitions and ad hoc lemmas which may have simpler proofs,
organized in a few sections.
How should I do a pull request ? Try to guess in which files each lemma could go ?
Or send a big file and wait for reviews ?
Also, the names of the lemmas might need to be adjusted.

[Anne Baanen]

Antoine Chambert-Loir said:

The file is a bit long (500 lines), but it incorporates some definitions and ad hoc lemmas which may have simpler proofs,
organized in a few sections.
How should I do a pull request ? Try to guess in which files each lemma could go ?
Or send a big file and wait for reviews ?
Also, the names of the lemmas might need to be adjusted.

In general, the advice is to make lemmas available as soon as possible, i.e. in the file with the fewest transitive imports. However if you can't find an obvious candidate, I'd like to encourage you to make a new file - I like working with short files. And if you are unsure, it's fine to leave the lemmas in the original file, especially if you note such cases with a comment.

[Anne Baanen]

More important than making the code look nice is making the code available at all! So in case of doubt, please don't hesitate to create the PR as it is now, and the experienced users can help you with any issues that come up.

[Antoine Chambert-Loir]

Done! see #10253

[Johan Commelin]

Congratulations! I left two first comments. We'll try to give a detailed review later this week.

[Sebastien Gouezel]

Antoine Chambert-Loir said:

(I do not know whether the latter will require a lot of stuff or not, I am not sure it is already proved that SL(n,K)
is generated by transvections.)

We already have that GL (n, K) is generated by transvections and diagonal matrices, see docs#matrix.diagonal_transvection_induction_of_det_ne_zero. From this the SL (n, K) case should not be too painful (essentially do 2 x 2 matrices to replace iteratively the diagonal terms by 1).

[Antoine Chambert-Loir]

Thanks for your comments @Sebastien Gouezel and @Johan Commelin .
To implement the second remark of Johan, it seems that I need, if Xis a type and n:ℕ, to define a type representing the subtype of X^n representing n-tuples with distinct entries in the type X — and to endow it with its natural action of G if Xhas an action of G(mul_action G X) . What is the standard way to code this ? (s :fin n → X) (inj: injective s) ?

[Johan Commelin]

@Antoine Chambert-Loir Ooh, I was thinking of formalizing the definition you wrote in the module docstring:

-- The action is *primitive* if it is transitive, and if all stabilizers G_x are maximal subgroups.

[Johan Commelin]

Is that not the kind of thing that you are using in the lemmas that of primitive in their name?

[Yakov Pechersky]

You can us function.embedding (fin n) X to bundle the injectivity

[Antoine Chambert-Loir]

Johan Commelin said:

Antoine Chambert-Loir Ooh, I was thinking of formalizing the definition you wrote in the module docstring:

-- The action is *primitive* if it is transitive, and if all stabilizers G_x are maximal subgroups.

The file already includes

variables (G X)
structure is_primitive
extends is_transitive G X : Prop :=
(has_maximal_stabilizers: ∀ x:X, (stabilizer G x).is_maximal)

Isn't it sufficient then ?

[Johan Commelin]

@Antoine Chambert-Loir ooh, sorry I hadn't seen that. So why are you not using that definition in those lemmas? Maybe I haven't thought enough about the maths. But the names of the lemmas suggest you want to talk about a primitive action. But the statement doesn't use is_primitive.

[Antoine Chambert-Loir]

Don't I use it ? I'm completely puzzled…

[Johan Commelin]

Sorry, maybe I'm just blind. Let me look at your code again.

[Johan Commelin]

@Antoine Chambert-Loir My apologies for all the noise. I was probably still asleep when I wrote that comment.

[Johan Commelin]

Please ignore my second remark.

[Johan Commelin]

To make up for the bad review. Let me try to do a better one now.

[Antoine Chambert-Loir]

No worry… You cannot guess how pleasant I find to realize that people thousand miles away are looking, commenting at one's work, providing help, making suggestions of improvements…

[Johan Commelin]

Ok, I left several more comments. Hopefully less stupid this time.

[Antoine Chambert-Loir]

Just to let you know that 2 weeks ago, I (almost) completed the formal proof that the alternating group is simple using the Iwasawa criterion for simplicity. This is really a long proof, because it requires to prove that some subgroups of the alternating group are maximal subgroups, and in turn that result follows from a 1871 theorem of Jordan (that a primitive subgroup of $S_n$ that contains a 3-cycle contains the alternating group). All of this is in branch#acl_Wielandt.

Actually, there is one case missing, when $n=6$, because in that case, the relevant subgroup of $A_6$, $A_6 \cap (S_3\times S_3)$, is not maximal. To use that method, I wish to consider double transpositions, but first I need to prove that the double transpositions (and identity) form a commutative subgroup of $A_4$ —This is the “Kleiner Vierergruppe”.

By hand, this is clear, but it looked annoying to try to formalize these arguments, so I imagined another way.
You can observe that these elements (identity and double transpositions) are the only elements of $A_4$ whose order is a power of $2$;
so once you know there are of them, they will fill any Sylow subgroup of $A_4$ hence they would constitute the unique 2-Sylow subgroup of $A_4$.

Lean easily tells you that there are 3 elements with cycle type [2,2], via #eval, but it is a bit slow and I don't know how to use such a computation in a formal proof.
So I embarked in computing the number of permutations in a given conjugacy class in the general symmetric/alternating group.
(This is almost done but will take a few weeks.)

[Antoine Chambert-Loir]

A few more weeks meant 3 months,
but I finally accomplished what I started to 14 months ago!

/-- If α has at least 5 elements,
then the only nontrivial normal sugroup of (perm α) is the alternating_group. -/
theorem alternating_group.normal_subgroups {α : Type*} [decidable_eq α] [fintype α]
  (hα : 5 ≤ fintype.card α)
  {N : subgroup (alternating_group α)} (hnN : N.normal) (ntN : nontrivial N) : N = ⊤ :=
begin
  by_cases hα' : fintype.card α = 6,
  { apply alternating_group.normal_subgroups_8 hα _ hnN ntN,
    rw hα', norm_num, },
  exact alternating_group.normal_subgroups_6 hα hα' hnN ntN,
end

[Kevin Buzzard]

The docstring seems to be about the symmetric group but the lemma says that the alternating group is simple?

[Antoine Chambert-Loir]

“Just to check that some people are actually reading…”