Sylow subgroups

Stream: Is there code for X?

[Ines Wright]

I've been working on a proof of Sylow two with Kevin Buzzard which I want to PR eventually. What do you think about this as a definition of sylow subgroups?

import data.zmod.basic
import data.fintype.card

open fintype subgroup
universe u
variables {G : Type u} [group G]

open_locale classical

/-- define a sylow subgroup given a prime p, and subgroup L -/
def is_sylow_subgroup [fintype G] (L : subgroup G) {p : ℕ} [fact p.prime]:=
  ∃ m n : ℕ, card G = p ^ n * m ∧ ¬ p ∣ m ∧ card L = p ^ n

[Kevin Buzzard]

Does the linter complain that you never assumed p was prime? :-)

[Ines Wright]

no but it complains that it's unused so perhaps it does need removing

[Eric Wieser]

Do you want to say "L is a sylow subgroup for a given p" or "there exists a p for which L is a sylow subgroup"?

[Eric Wieser]

Because what you've written is closer to the former, but can't work unless you make p explicit

[Adam Topaz]

Yes, I think p should be made explicit, so you can write is_sylow_subgroup L p saying that L is a p-Sylow subgroup

[Adam Topaz]

Maybe p should come before L so that set_of (is_sylow_subgroup p) is the set of all p-Sylow subgroups?

[Thomas Browning]

There's also the option of defining p-subgroups, putting an ordering on them (which has nice properties), and defining Sylow p-subgroups to be the maximal elements (and later proving things about the order of a Sylow p-subgroups)