from iso between sets to iso between groups

Stream: general

[Jiatong Yang]

import data.fintype.basic

universes u

def G4 := fin 4
lemma mul_comm_of_G4 [group G4] (x y : G4) : x * y = y * x := sorry

/-- Every group of order 4 is commutative -/
lemma mul_comm_of_card_eq_four (G : Type u) [fintype G] [group G] (hG4 : fintype.card G = 4) :
  ∀ g h : G, g * h = h * g := sorry

How to prove mul_comm_of_card_eq_four using mul_comm_of_G4?

[Junyan Xu]

there's docs#equiv.group

[Andrew Yang]

And docs#fintype.equiv_fin should also be helpful.

[Eric Wieser]

What's the maths proof? It's not enough to say "these types have the same number of elements", you need to show that you can match the group identity with the identity etc

[Eric Wieser]

Oh, I guess here because you stated G4 without a specific group structure you don't have that problem

[Jiatong Yang]

import data.fintype.basic
import logic.equiv.transfer_instance

universes u

def G4 := fin 4
lemma mul_comm_of_G4 [H : group G4] (x y : G4) : x * y = y * x := sorry

/-- Every group of order 4 is commutative -/
lemma mul_comm_of_card_eq_four (G : Type u) [fintype G] [group G] (hG4 : fintype.card G = 4) :
  ∀ g h : G, g * h = h * g := begin
  have e : G ≃ G4 := begin
    change G4 with fin 4,
    rw ← hG4,
    apply fintype.equiv_fin,
  end,
  let grp := equiv.group e.symm,
  intros g h,
  have : (e.to_fun g) * (e.to_fun h)= (e.to_fun h) * (e.to_fun g),
  exact mul_comm_of_G4 (e.to_fun g) (e.to_fun h),
end

I'm sorry that I still cannot finish this proof...

[Eric Wieser]

Looks like you've solved the annoying equiv part of the proof at least

[Eric Wieser]

Oh right, there's a missing sorry in that proof

[Jiatong Yang]

I haven't solved the equiv part :sob:

[Eric Wieser]

A bit sloppy, but this works:

import data.fintype.basic
import logic.equiv.transfer_instance

universes u

def G4 := fin 4
lemma mul_comm_of_G4 [H : group G4] (x y : G4) : x * y = y * x := sorry

/-- Every group of order 4 is commutative -/
lemma mul_comm_of_card_eq_four (G : Type u) [fintype G] [group G] (hG4 : fintype.card G = 4) :
  ∀ g h : G, g * h = h * g :=
begin
  have e : G ≃ G4 := fintype.equiv_fin_of_card_eq hG4,
  rw e.symm.surjective.forall₂,
  intros g h,
  apply e.injective,
  letI grp := equiv.group e.symm,
  convert mul_comm_of_G4 _ _,
  rw equiv.symm_symm,
  rw equiv.symm_symm,
end

[Eric Wieser]

Ah, this is a bit slicker:

/-- Every group of order 4 is commutative -/
lemma mul_comm_of_card_eq_four (G : Type u) [fintype G] [group G] (hG4 : fintype.card G = 4)
  (g h : G) : g * h = h * g :=
begin
  have e : G ≃ G4 := fintype.equiv_fin_of_card_eq hG4,
  letI grp := equiv.group e.symm,
  let e' := e.symm.mul_equiv,
  have := fun_like.congr_arg e' (mul_comm_of_G4 (e'.symm g) (e'.symm h)),
  simpa only [map_mul, mul_equiv.apply_symm_apply],
end

Where docs#equiv.mul_equiv is responsible for most of the cleanup

[Eric Wieser]

I'm a little suspicious that your mul_comm_of_G4 doesn't state what you think it states, but I guess you'll find out when you start trying to prove it!

[Kevin Buzzard]

What are you worried about? It's still true, right?

[Kevin Buzzard]

I think there are two open PRs now proving that all groups of order p^2 are commutative by the way

[Yaël Dillies]

Yes, but it's just as hard as the next lemma, right?

[Kevin Buzzard]

Yes!

[Eric Wieser]

Possibly harder than the next lemma, because either you don't unfold G4 in which case it's basically identical, or do you unfold it and now you have 1 : fin 4 and 1 : G4 for which equality is undecidable

[Jiatong Yang]

Thank you a lot. I've unlocked the answer to the problem since I couldn't solve the first lemma either. :sob: