nilpotency questions

Stream: maths

[Joachim Breitner]

I am digging my teeth into various stuff about nilpotent groups, as suggested by @Kevin Buzzard, and before I bark up the wrong tree, maybe someone can quickly confirm whether this is actually true or not:

If $H_n$ is the lower central series of $G$, then $H_{n+1}/Z(G)$ is the lower central series of $G/Z(G)$.

Note that $H_0 = \bot$ and $H_1 = Z(G)$.
(From this I can then prove that the nilpotency class of $G/Z(G)$ is one less than that of $G$, for non-trivial $G$, and that gives me a useful induction principle.)

[Joachim Breitner]

Relatedly, and maybe helpful here: Where do I find $(G_1/G_3)/(G_2/G_3) \simeq(G_1/G_2)$? (because then I could apply https://math.stackexchange.com/questions/4111176/show-that-these-two-definitions-of-a-nilpotent-group-are-equivalent#comment8500626_4111320 maybe)

[Floris van Doorn]

docs#quotient_group.quotient_quotient_equiv_quotient I think

[Joachim Breitner]

Oh, looks like the header at the top of the file is wrong, it says

Noether's third isomorphism theorem, the canonical isomorphism between (G / M) / (M / N) and G / N, where N ≤ M.

so I didn’t look further (note the (M/N)):
:face_palm: Thanks!

[Floris van Doorn]

That looks like a couple of typos, yes

[Joachim Breitner]

I’ll prepare a PR to fix them.
https://github.com/leanprover-community/mathlib/pull/11581

[Moritz Doll]

(sorry, no github account right now): it should be (G / N) / (M / N) and (G / M) (the last N should become an M), see docs#quotient_group.quotient_quotient_equiv_quotient

[Yaël Dillies]

Reviewed for you!

[Joachim Breitner]

And I screwed up. Must be cursed. Second try :-)