Proving group elements are commutative

Stream: general

[Roshan Kohli]

I have finished almost everything in my proof that groups of order pq (given p doesn't divide q-1) are cyclic. The only thing left to prove is that when I have my generators for the Sylow p-subgroup and Sylow q-subgroup, these generators commute. Usually in maths I would show these Sylow subgroups are unique hence they are normal. So by definition of a normal subgroup the elements must commute. I am having a difficult time trying to show this. I haven't found anything particularly useful in the Sylow.lean file. I have also tried to use the assumption that my Sylow subgroups are normal to see if I could prove that the elements commute, but also this has led to nothing. I think the way normal groups are defined in Mathlib could be the issue but I am unsure. If you can think of another way to prove commutativity then please let me know. Any advice or guidance would be appreciated. I will show my code up to the point where I need commutativity.

import Mathlib.Data.ZMod.Basic
import Mathlib.GroupTheory.Index
import Mathlib.Data.Finset.Card
import Mathlib.GroupTheory.OrderOfElement
import Mathlib.Data.Nat.Choose.Dvd
import Mathlib.Data.Nat.Choose.Basic
import Mathlib.Algebra.Group.Defs
import Mathlib.GroupTheory.Subgroup.Basic
import Mathlib.GroupTheory.SpecificGroups.Cyclic
import Mathlib.Data.Nat.Prime
import Mathlib.GroupTheory.Sylow
import Mathlib.GroupTheory.Coset
import Mathlib.GroupTheory.GroupAction.Defs

open scoped Classical

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

-- A group of order pq for primes p and q and such that p doesn't divide q-1, is the cyclic group of pq elements
theorem C_pq (q : ℕ) [hp : Fact p.Prime] [hq : Fact q.Prime] (hpq: p<q) (hpqq: Fintype.card G = p*q) (h:¬(p ∣ q - 1)): IsCyclic G := by
-- Define the Sylow p-subgroup
  have p0 : p ∣ Fintype.card G := by
    rw [hpqq]
    exact Nat.dvd_mul_right p q
  have p1 := Sylow.exists_subgroup_card_pow_prime p ((pow_one p).symm ▸ p0)
  rw [pow_one] at p1
  obtain ⟨P, hP⟩ := by exact p1
  have p2 : Fintype.card P = p := by
    exact hP
-- Show P is cyclic and generated by an element g of order p
  have p3 : IsCyclic P := by
    exact isCyclic_of_prime_card hP
  obtain ⟨g, gP⟩ := IsCyclic.exists_generator (α := P)
  have p4 : orderOf g = Fintype.card P := by exact orderOf_eq_card_of_forall_mem_zpowers gP

-- Define the Sylow q-subgroup
  have q0 : q ∣ Fintype.card G := by
    rw [hpqq]
    exact Nat.dvd_mul_left q p
  have q1 := Sylow.exists_subgroup_card_pow_prime q ((pow_one q).symm ▸ q0)
  rw [pow_one] at q1
  obtain ⟨Q, hQ⟩ := by exact q1
  have q2 : Fintype.card Q = q := by
    exact hQ
-- Show Q is cyclic and generated by an element k of order q
  have q3 : IsCyclic Q := by
    exact isCyclic_of_prime_card hQ
  obtain ⟨k, kQ⟩ := IsCyclic.exists_generator (α := Q)
  have q4 : orderOf k = Fintype.card Q := by exact orderOf_eq_card_of_forall_mem_zpowers kQ

-- Show p and q are coprime
  have pq_coprime : Nat.gcd p q = 1 := by
   refine (Nat.coprime_primes ?pp ?pq).mpr ?_
   apply hp.1
   apply hq.1
   exact Nat.ne_of_lt hpq

-- Show g and k commute
  have g_k_commute : Commute (g : G) (k : G) := by sorry

[Filippo A. E. Nuccio]

It would be a nice idea to split your proof in several short sublemmas, because it would be easier to check and to modify it. That being said, there is this result docs#Sylow.directProductOfNormal telling that as soon as you prove that the Sylows are normal, you are basically done because the group will be a direct product of cyclic groups.

[Matt Diamond]

I have also tried to use the assumption that my Sylow subgroups are normal to see if I could prove that the elements commute, but also this has led to nothing.

would docs#Subgroup.commute_of_normal_of_disjoint help?

[Junyan Xu]

I feel that OP's questions have been solved in this thread and on Discord ...