Zulip Chat Archive

Stream: general

Topic: from iso between sets to iso between groups


Jiatong Yang (Jul 27 2022 at 08:08):

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 (Jul 27 2022 at 08:13):

there's docs#equiv.group

Andrew Yang (Jul 27 2022 at 08:14):

And docs#fintype.equiv_fin should also be helpful.

Eric Wieser (Jul 27 2022 at 08:48):

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 (Jul 27 2022 at 08:49):

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

Jiatong Yang (Jul 27 2022 at 08:55):

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 (Jul 27 2022 at 09:02):

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

Eric Wieser (Jul 27 2022 at 09:04):

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

Jiatong Yang (Jul 27 2022 at 09:08):

I haven't solved the equiv part :sob:

Eric Wieser (Jul 27 2022 at 09:23):

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 (Jul 27 2022 at 09:31):

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 (Jul 27 2022 at 09:31):

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 (Jul 27 2022 at 10:50):

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

Kevin Buzzard (Jul 27 2022 at 10:51):

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

Yaël Dillies (Jul 27 2022 at 10:51):

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

Kevin Buzzard (Jul 27 2022 at 10:52):

Yes!

Eric Wieser (Jul 27 2022 at 11:08):

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 (Jul 27 2022 at 11:22):

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


Last updated: Dec 20 2023 at 11:08 UTC