Sequence of Sylow subgroups

Stream: Is there code for X?

[Artie Khovanov]

We have Sylow.exists_subgroup_card_pow_succ, which says that a subgroup of order $p^k$ is contained in a subgroup of order $p^{k+1}$ if $p^{k+1}$ divides the order of the group. Do we have the sequence of such subgroups from $1$ up to the Sylow $p$-subgroup?

[Scott Carnahan]

Your use of “the” is slightly problematic since this sequence is not uniquely defined.

[Scott Carnahan]

Do you want to iteratively use choice to make a sequence?

[Yaël Dillies]

It looks Artie might mean the sequence for a given Sylow subgroup?

[Kevin Buzzard]

That's not unique either (it could be a vector space over Z/pZ for example). Every "the" in the last sentence of Artie's post is confusing.

[Artie Khovanov]

Yeah it's not unique in any way
I just mean, do we have some sequence of those groups packaged together

[Artie Khovanov]

But it's moot because I realised in my application I only need to go two steps so I can just apply the lemma twice

[Scott Carnahan]

I just remembered that this amounts to a composition series for a Sylow p-group, but I don’t know if we have existence of composition series.

[Artie Khovanov]

Found 0 declarations mentioning CompositionSeries and Group.
looks like no

[Junyan Xu]

See
#Is there code for X? > Composition Series for Groups wrt Normal subgroup @ 💬
#maths > JordanHolderLattice for Subgroup @ 💬

[Artie Khovanov]

I am pretty sure this is about uniqueness and I am asking about existence.
And moreover I'm not just asking for any series; I want a series where all the indexes are $p$. There's some content here (that follows from the theorem I linked).

[Kevin Buzzard]

A series where all the indexes are $p$ is precisely a composition series.

[Junyan Xu]

Yeah, and composition series are not unique, though the multiset of successive quotients is unique up to isomorphisms.

[Artie Khovanov]

I don't disagree @Kevin Buzzard
But the statement that was linked only talks about maximality
When what I want is precisely that the maximal subgroup has index $p$!

[Artie Khovanov]

And yeah by uniqueness I meant the quotient thing

[Junyan Xu]

H being a maximal normal subgroup in K means that K/H is simple, and a $p$-group is simple iff it is cyclic.

There is LTSeries.exists_relSeries_covBy but CovBy is maximality without normality, so you'll need to prove something harder, see https://math.stackexchange.com/questions/1763518/every-proper-maximal-subgroup-of-a-p-group-p-is-normal-and-has-index-p

It's probably easier to build a LTSeries from Sylow.exists_subgroup_card_pow_succ by recursion.

[Artie Khovanov]

Well, quite