Proving groups of order pq are cyclic

Stream: general

[Roshan Kohli]

I am proving that groups of order pq (with p not dividing q-1) are isomorphic to the cyclic group of order pq. I have defined the Sylow p-subgroup and Sylow q-subgroup. I have then taken their generators (say g and k) then I am trying to show that gk has order pq. However I am unsure on how to make lean understand that g and k are also elements of G. I have tried coercion but I am not sure how to correctly implement it. At the moment lean does not like that I want to multiply g and k together as they are from different subgroups. The code is below, thank you.

-- 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 gh generates G ie gh has order pq
  have pq : orderOf (g*k) = p*q := by
    sorry

[Yaël Dillies]

(could someone move this to #general?)

[Bolton Bailey]

I am currently getting failed to synthesize instance Fintype G. Care to make this a #mwe @Roshan Kohli ?

[Roshan Kohli]

my imports are

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]

The open scoped Classical should fix that error. Sorry for not providing earlier @Bolton Bailey

[Bolton Bailey]

Thanks. Does ((g : G) * k) work?

[Roshan Kohli]

Yes thanks a lot. Surprised it was that simple. @Bolton Bailey

[Notification Bot]

Roshan Kohli has marked this topic as resolved.

[Bolton Bailey]

Well, don't thank me yet, you will now have to deal with the casting to the G, but this should at least be the first step.

[Notification Bot]

Roshan Kohli has marked this topic as unresolved.