nilpotency in finite groups

Stream: Is there code for X?

[Joachim Breitner]

@Kevin Buzzard , your order is ready:

/-- A finite group is nilpotent iff the normalizer condition holds, and iff all sylow groups are
normal and iff its the direct product of its sylow groups.  -/
theorem is_nilpotent_of_finite_tfae : tfae
  [ is_nilpotent G,
    normalizer_condition G,
    ∀ (p : ℕ) (hp : fact p.prime) (P : sylow p G), (↑P : subgroup G).normal,
    nonempty ((Π p : (card G).factorization.support, Π P : sylow p G, (↑P : subgroup G)) ≃* G) ] :=
begin
  tfae_have : 1 → 2, { exact @normalizer_condition_of_is_nilpotent _ _ },
  tfae_have : 2 → 3, { introsI h p _ P, exact sylow.normal_of_normalizer_condition h _ },
  tfae_have : 3 → 4, { exact λ h, nonempty.intro (sylow.direct_product_of_normal h) },
  tfae_have : 4 → 1, { rintros ⟨e⟩, exact is_nilpotent_of_product_of_sylow_group e },
  tfae_finish,
end

[Joachim Breitner]

It’s still missing the connection to “all maximal groups are normal”, for which I have not looked yet at how to prove the implication back (probably using Frattini's argument as done here). And of course there is a DAG of outstanding 10 PRs that I have to clean up, get through review, in addition to the 19 PRs created over the last three weeks and already merged; PR overview.

[Thomas Browning]

Yes, the Frattini's argument proof doesn't seem too bad.

[Kevin Buzzard]

@Joachim Breitner that is awesome! Thank you for the valuable addition to mathlib!

It turns out that the community here (led on this occasion by Patrick Massot) have written down an "official" definition of "an undergraduate degree", and now we have the challenge to teach it to Lean. However I have my own unofficial definition of an undergraduate degree, which is "everything I learnt in my undergraduate classes" and this is one of the few theorems in my group theory class which was not already in mathlib. Thanks very much!

[Joachim Breitner]

Do we already have the statement that a non-top subgroup of a finite group is contained in a maximal (is_coatom) subgroup? It seems that the statement should look like is_coatomic (subgroup G), but grep doesn’t find a lemma of that form.

[Yaël Dillies]

I think we don't

[Yaël Dillies]

However I'm wondering what's the correct generality for this. I think it has little to do with subgroups.

[Yaël Dillies]

Shouldn't it hold in any finite top order?

[Joachim Breitner]

Yes, I think that instance should do.

[Yaël Dillies]

Eh, we don't have fintype -> is_coatomic either :upside_down:

[Joachim Breitner]

Isn’t that the instance you were suggesting?

[Yaël Dillies]

Yeah! I just thought it was there already. Wanna do it or should I?

[Joachim Breitner]

I just sorried’d it in my proof, at https://github.com/leanprover-community/mathlib/pull/11841/files#diff-ab70e1f803f9921c903cc935dd827a15a25f8323fad19b349c8f756bb396c059R555 and will call it a day for now. If I find the instance on master or some PR when I come back to it tomorrow I wouldn’t mind :-)

[Joachim Breitner]

Hmm, on Feb 4 I claimed that the theorem about the various different definitions of nilpotency for finite groups is ready, after three weeks of leaning. Turns out it wasn’t quite ready, and it took another 6 weeks to actually get “the” PR in. (Quotation marks because it actually took 45 PRs with at least 424 commits – thanks to all the patient reviewers, especially @Eric Wieser ).

But here it is:
https://leanprover-community.github.io/mathlib_docs/group_theory/nilpotent.html#is_nilpotent_of_finite_tfae
or maybe prettier
https://github.com/leanprover-community/mathlib/blob/7f1ba1a333d66eed531ecb4092493cd1b6715450/src/group_theory/nilpotent.lean#L898-L903

The biggest chunk during PR review was probably noncomm_pi_coprod; the construction of {ϕ : Π (i : ι), (N i →* M) // pairwise commutes mumble mumble} ≃ ((Π (i : ι), N i) →* M), and expanding the API of the underlying finset.noncomm_prod function.