Working with Sylow subgroups in a simple case

Stream: new members

[Ryan Smith]

I noticed that mathlib doesn't have the basic fact that for primes p and q all groups of order pq are solvable. This seemed like an easy place to get more familiar with how lean handles group theory.

I'm finding it surprisingly hard to do the equivalent of "let P be a sylow p subgroup of G of order p". The library has results that there exist a subgroup of order p^1 but not that it is a sylow p subgroup since that needs an extra property of maximality.

We also have a result which says that if I already have a sylow subgroup I could get its cardinality from the multiplicity of p in the order of G, which would be great if I could just say "let P \in Sylow p G" but how do I express that?

Sylow.exists_subgroup_card_pow_prime.{u} {G : Type u} [Group G] [Finite G] (p : ℕ) {n : ℕ} [Fact (Nat.Prime p)]
  (hdvd : p ^ n ∣ Nat.card G) : ∃ K, Nat.card ↥K = p ^ n

Sylow.card_eq_multiplicity.{u} {G : Type u} [Group G] [Finite G] {p : ℕ} [hp : Fact (Nat.Prime p)] (P : Sylow p G) :
  Nat.card ↥↑P = p ^ (Nat.card G).factorization p

Also, I'm confused over both of these theorems type coercing the cardinality of objects? Why wouldn't the second one for instance just say Nat.card P = p ^ (Nat.card G).factorization p?

[Aaron Liu]

docs#Sylow

[Kenny Lau]

@Ryan Smith Nat.card takes a type, which P is not

[Aaron Liu]

Ryan Smith said:

I'm finding it surprisingly hard to do the equivalent of "let P be a sylow p subgroup of G of order p". The library has results that there exist a subgroup of order p^1 but not that it is a sylow p subgroup since that needs an extra property of maximality.

If you want an arbitrary Sylow p-subgroup you can use docs#Sylow.nonempty

[Thomas Browning]

Ryan Smith said:

I noticed that mathlib doesn't have the basic fact that for primes p and q all groups of order pq are solvable.

Actually, we have better than that: Every group of squarefree order is solvable. See docs#IsZGroup.of_squarefree and docs#IsZGroup.instIsSolvableOfFinite (the strongest statement we have is docs#isZGroup_iff_exists_mulEquiv)

[Ryan Smith]

Nice, we have Z-Groups. That proves the literal question at hand but the point was more "how do I introduce a named sylow p group for G" from the standpoint of a lean beginner.

Or put another way, how do I explicitly go about using Sylow.nonempty for example? Maybe I'm just approaching it the wrong way and being too literal about translating English to lean by writing things like

have hP : ∃ P, P ∈ Sylow p G := Sylow.nonempty p G

Which is not at all well formed according to lean?

[Aaron Liu]

Sylow is a type, which means you have objects of type Sylow p G

[Aaron Liu]

In other words, you don't talk about subgroups being Sylow, instead you talk about Sylow subgroups

[Aaron Liu]

You can still state "the subgroup P is Sylow" as "there exists a Sylow subgroup which is equal (as a subgroup) toP"

[Aaron Liu]

you can obtain an arbitrary p-Sylow subgroup of G and name it v with

obtain ⟨v⟩ : Nonempty (Sylow p G) := inferInstance

[Ryan Smith]

Thanks for having the patience to answer simple stuff