Sylow game - group of order 20 not simple

Stream: general

[Edinburgh]

Hi, I am trying to show that a group of order 20 cannot be simple using Sylow's theorems.
I am very much struggling and I would like to learn how to use the Sylow theorems to show that there is a unique Sylow 5-subgroup, so it must be a proper normal subgroup of G, thus G is not simple.
I am currently now trying to show that the number of Sylow 5 subgroups must divide 4 as |G|/|G_5|=20/5=4 and the only number number that divides 4 and is conrguent 1 mod 5 is 1.

I would very much appreaciate your help as I am quite lost with lean.
Thanks in advance.

import Mathlib.GroupTheory.Sylow
import Mathlib.Data.Finset.Card
import Mathlib.Data.ZMod.Basic -- Contains definition of modular equality
import Mathlib.GroupTheory.Index -- Contains definition of group index
import Mathlib.GroupTheory.Subgroup.Basic -- Contains definition of a normal subgroup
import Mathlib.Data.Nat.Prime -- Contains definition of a prime


variable (p : ℕ) [Fact p.Prime] (G : Type*) [Group G] [Fintype G]

-- The example states that a group of order 20 cannot be simple
example (hG : Fintype.card G = 20) : ¬ IsSimpleGroup G := by
  -- Establish that 5 is a prime number
  have h₀ : Fact (Nat.Prime 5) := fact_iff.mpr (by norm_num)

  -- Prove that 5 divides the order of the group G
  have h₂ : 5 ∣ Fintype.card G := by use 4 -- 5 divides 20 (20 = 4 * 5)

  -- Apply Sylow's theorem to conclude the existence of a Sylow 5-subgroup
  -- The theorem guarantees a subgroup of order 5^1, as 5 is a prime dividing the group's order
  have h₃ := Sylow.exists_subgroup_card_pow_prime 5 <| (pow_one 5).symm ▸ h₂

  -- We extract the actual subgroup Q which satisfies the Sylow p-subgroup conditions for p=5
  obtain ⟨Q, hQ⟩ := h₃

  have : Fintype Q := Fintype.ofFinite Q

  have : (Nat.factorization 20) 5 = 1 := sorry
  have card_eq : Fintype.card Q = 5 ^ (Nat.factorization (Fintype.card G)) 5 := by
    rw [hG]
    convert hQ

  have S := Sylow.ofCard Q card_eq

  -- Now we use Sylow's theorems to analyse the number of such subgroups

   -- Use Sylow's theorems to deduce the number of Sylow p-subgroups is congruent to 1 mod p
  have h₄ : Fintype.card (Sylow 5 G) ≡ 1 [MOD 5] := card_sylow_modEq_one 5 G

  -- Show that the number of Sylow 5-subgroups divides the order of the group divided by the order of a Sylow 5-subgroup
  have h₅ : (Fintype.card (Sylow 5 G)) ∣ (Fintype.card G)/(Fintype.card Q) := by sorry
  have h₆ : Fintype.card (Sylow 5 G) = 1 ∨ Fintype.card (Sylow 5 G) = 4 := by sorry
  have h₇ : ¬ (4 ≡ 1 [MOD 5]) := by exact of_decide_eq_false rfl

  -- Establish that there is exactly one Sylow 5-subgroup in G

  have h₈ : Fintype.card (Sylow 5 G) = 1 := by sorry

  -- Conclude the existence and uniqueness of the Sylow 5-subgroup, implying it is normal
  -- The uniqueness of the Sylow subgroup follows from h₈ and the properties of Sylow subgroups
  obtain ⟨P, hP⟩ := Fintype.card_eq_one_iff.mp h₈

  -- Prove that the unique Sylow subgroup P is a normal subgroup of G
  -- This will use the fact that a unique Sylow subgroup is always normal
  have h₁₀ : Subgroup.Normal Q := by sorry

  -- Conclude that G is not simple because it has a normal subgroup of order 5
  -- This final step uses the definition of a simple group, which cannot have non-trivial normal subgroups
  exact h₁₀```

[Johan Commelin]

@Edinburgh Please edit your message to add #backticks so that you get syntax highlighting, like so

```
code here
```

[Johan Commelin]

 have : Fintype ↥Q := Fintype.ofFinite ↥Q -- HERE I GET ERROR (unexpected token '↥'; expected command)

Just drop the ↥, should work

[Johan Commelin]

have h₅ : Fintype.card (Sylow 5 G) = 5 ∨ Fintype.card (Sylow 5 G) = 1 := by sorry

Why the first clause? 5 isn't congruent to 1 mod 5.

[Johan Commelin]

In general you seem to be on the right track.

[Johan Commelin]

Note the computations about explicit numeral numbers can often be done using norm_num or decide.

[Edinburgh]

Johan Commelin said:

have h₅ : Fintype.card (Sylow 5 G) = 5 ∨ Fintype.card (Sylow 5 G) = 1 := by sorry

Why the first clause? 5 isn't congruent to 1 mod 5.

thanks for spotting that.. my mistake

[Johan Commelin]

Ooh, and omega can also help with calculations with natural numbers.

[Notification Bot]

Edinburgh has marked this topic as resolved.

[Notification Bot]

Edinburgh has marked this topic as unresolved.

[Edinburgh]

I am currently now trying to show that the number of Sylow 5 subgroups must divide 4 as |G|/|G_5|=20/5=4 and the only number number that divides 4 and is conrguent 1 mod 5 is 1. Do you have any idea how to approach it? (using probably:

have h₇ : ¬ (4 ≡ 1 [MOD 5]) := by exact of_decide_eq_false rfl

[Julian Berman]

decide handles that one:

example : ¬ (4 ≡ 1 [MOD 5]) := by decide