normal sylow groups

Stream: maths

[Joachim Breitner]

A math questions (but with a hint of “which proof might be easiest to do”).
I’m in the process of proving various definitions for nilpotent equivalent (for finite groups).
I already have nilpotent → normalizer condition → all max subgroups are normal.
Now I want to prove that all sylow subgroups are normal.
Wikipedia goes from “normalizer condition” to that directly, but I found the proofs on that page to be too vague to be very helpful, and had more luck on the groupprops wiki. There, the list of equivalente conditions puts “all max groups normal” before “all sylow groups normal”, and I wonder if that hints at a simple proof of that implication. But it’s not clear to me if that implication really holds (or rather, it certainly holds, they are all equivalent, but whether there is a small proof). Sylow subgroups need not be maximal, right? But maybe there is a simple argument?

[Daniel Roca González]

You're correct that Sylow groups definitely don't need to be maximal: think about the direct sum of three cyclic groups of different prime orders.

[Joachim Breitner]

Ok, guess I should then go from “normalizer condition” to “sylow groups normal”. The argument seems to go via characteristic subgroups, so I might need some extra lemmas about characteristic

[Daniel Roca González]

What do you think about the proof of 24.18 Theorem here?

[Thomas Browning]

Mathlib knows that characteristic subgroups of normal subgroups are characteristic, so you just need to know that normal sylow subgroups are characteristic.
You could also prove (normalizer condition) -> (sylow subgroups normal) from the useful fact N_G(N_G(P))=N_G(P), which can be proved from Frattini's argument (which is already in mathlib).

[Thomas Browning]

To spell the latter proof out a bit more:
Lemma 1: If P is a Sylow p-subgroup of G, and if N_G(P) is a normal subgroup of G, then N_G(P) = G.
Proof: Frattini's argument (#sylow.normalizer_sup_eq_top) gives N_G(P) ⊔ N_G(P) = G. It follows that N_G(P) = G.

Lemma 2: If P is a Sylow p-subgroup of G, then N_G(N_G(P))=N_G(P)
Proof: Let H = N_G(N_G(P)). Then P is a Sylow p-subgroup of H, and N_H(P)=N_G(P) is a normal subgroup of H, so Lemma 1 gives N_H(P)=H, so N_G(P)=N_G(N_G(P)).
(This proof might be a bit fiddly to formalize in Lean, due to the passing back and forth between G and H)

From here it's easy to go from "normalizers grow" to "sylow subgroups normal"

[Joachim Breitner]

Thanks for the hints! Should be enough to get me going :-)

[Joachim Breitner]

I am trying to find a function given P : sylow p G and P.1 < N, it’s unclear to me how to consider P a sylow subgroup of `N. Are the definitions for that missing?

If so, would this be a good start?

def subtype {p : ℕ} (P : sylow p G) (N : subgroup G) (h : P.1 ≤ N) :
  sylow p N :=
   ⟨ comap N.subtype P.1,
    begin sorry end ,
    begin sorry end⟩

[Daniel Roca González]

I am not very deep in this, but as I see it, it should be easy to prove if you know that N.subtype is injective (which doesn't seem to be in the library?). Then $p$-groupness should be in the library and maximality should be pretty easy.

[Joachim Breitner]

Right, I’m not worried about the proofs (yet :-)), merely checking back that this is the right way to define this conversion.

[Daniel Roca González]

The statement itself looks fine to me: maybe you would also need the iso, but the iso should really be defined for N.subtype as I said.

[Joachim Breitner]

Indeed easy to get lost passing back and forth between G and H. I do that by applying comap H.subtype to go from the subgroups of G to the subgroups of H. In particular your N_H(P)=N_H(P) in Lemma 2, which seems to elaborate to N_H(comap H.subtype P) = comap H.subtype(N_G(P)) is not a trivial result, it seems to me.
I could prove H ≤ P.normalizer → comap H.subtype P.normalizer = (comap H.subtype P).normalizer for any subgroup P, but the inequality in the assumption goes the wrong way.

[Thomas Browning]

Look like some Sylow API is needed for passing back and forth between G and H, but I agree that it will be messy either way. The relevant lemmas are the is_p_group.map and is_p_group.comap lemmas in p_group.lean.

[Kevin Buzzard]

I think that this kind of problem is fascinating. I used to think it was really annoying -- you're in a situation here where in set theory the $P\subseteq G$ and the $P\subseteq N$ are actually the same object, because $N\subseteq G$. In type theory they're not, and I used to think that this was a serious problem; however now I think that in fact it's just a case of keeping your head and making sure the API is there. Once you've got over the fact that the two $P$ s aren't the same, but you know that they're isomorphic, this should be enough to make a messy proof. And then the art is to turn the messy proof into a more beautiful proof by writing the API which is required to make it clean.

[Adam Topaz]

Another approach is to replace the subgroups with an injective homomorphism. This way you have only one P, but get some other annoyances (which are perhaps not as bad?). I was talking with one of my students about free product with amalgamation in lean the other day, and this is the approach we took. (PS. We don't yet have free products with amalgamation in mathlib, except for the categorical formulation using colimits.)

[Joachim Breitner]

And I wonder how many manual proofs out there might accidentially go from N_G(P) to N_H(P) (both “the normalizer of P”) without justifying that step.