Constructing a group generated by a shift permutation

Stream: new members

[Daniel Eriksson]

One proof of Cauchy theorem for groups is to let a shift operator act on tuples of group elements and count orbits. Towards that end, I would like to construct a group generated a single shift. For simplicity, take the set L = {1,2,3} and the group generated by the permutation that takes 1 to 2, 2 to 3 and 3 to 1 which is a subgroup of the group of permutations of {1,2,3}. My idea is to try to prove an instance of a subgroup of permGroup which provides a group structure on permutations in MIL p.89: 

import MIL.Common
import Mathlib.GroupTheory.Perm.Subgroup

def permGroup {α : Type*} : Group₁ (Equiv.Perm α) where

  mul f g := Equiv.trans g f

  one := Equiv.refl α

  inv := Equiv.symm

  mul_assoc f g h := (Equiv.trans_assoc _ _ _).symm one_mul := Equiv.trans_refl

  mul_one := Equiv.refl_trans

  inv_mul_cancel := Equiv.self_trans_symm

I can explicitly define the elements:

def L := {l:List ℕ // l.length = 3}

def pm: L → L := fun ⟨x,h⟩ ↦ ⟨x.drop 1++[x.get! 0],by simp; rw[h]⟩

#eval pm ⟨[1,2,3],rfl⟩ -- [2,3,1]

def pm2: L → L := fun ⟨x,h⟩ ↦ pm (pm ⟨x,h⟩)

def pm3: L → L := fun ⟨x,h⟩ ↦ pm (pm (pm ⟨x,h⟩))

I used functions from list because I know how to work with them.
On page 121 in MIL they show Z is an additive subgroup of Q:

example : AddSubgroup ℚ where
  carrier := Set.range ((↑) : ℤ → ℚ)
  add_mem' := by
    rintro _ _ ⟨n, rfl⟩ ⟨m, rfl⟩
    use n + m
    simp
  zero_mem' := by
    use 0
    simp
  neg_mem' := by
    rintro _ ⟨n, rfl⟩
    use -n
    simp

I am trying to replace Q by permGroup L and Z by {pm, pm2, pm3} and do something like this.

instance genbyshiftperm: Subgroup permGroup L where
  carrier := Set.range ((↑) : {pm, pm2,pm3} → permGroup L)
  mul_mem' := by
    sorry
  one_mem' := by
    use f
    simp
  inv_mem' := by sorry -- use pm2 for pm etc

Is this how you do things?

[Matt Diamond]

There's syntax for specifying cyclic permutations (e.g. c[0, 1, 2]), which might be helpful:

https://leanprover-community.github.io/mathlib4_docs/Mathlib/GroupTheory/Perm/Cycle/Concrete.html

(I think the cyclic group of order 3 would be { c[], c[0, 1, 2], c[0, 2, 1] } ?)

See also: https://leanprover-community.github.io/mathlib4_docs/Mathlib/GroupTheory/Perm/Cycle/Basic.html

[Kevin Buzzard]

neg_mem' is only a thing for AddSubgroup, it gets replaced by inv_mem' for Subgroup

[Kevin Buzzard]

Subgroup means "subgroup of a group with group law *" and AddSubgroup means "subgroup of a group with group law +"

[Daniel Eriksson]

Yes sorry, edited to inv_mem'.

[Kevin Buzzard]

Two key problems with your code: permGroup L is not a group. It is an instance, which is a huge n-tuple of data consisting of a multiplication on Equiv.Perm L, an identity, an inverse, and proofs of lots of axioms. The group is Equiv.Perm L, which needs to go in brackets because functions in functional programming are greedy, they eat the next thing, so Subgroup permGroup L will eat permGroup and then get confused because (a) permGroup isn't a group (it's a function from types to big n-tuples) and (b) there's a random L which it won't know what to do with.

The second key problem is that your permutations pm are not terms of type Equiv.perm L, they are functions from L to L which happen to be bijective but no proof is supplied.

[Kevin Buzzard]

Here's some working code:

import Mathlib.GroupTheory.Perm.Subgroup

-- mathlib's group, not MIL's
instance permGroup {α : Type*} : Group (Equiv.Perm α) where
  mul f g := Equiv.trans g f
  one := Equiv.refl α
  inv := Equiv.symm
  mul_assoc f g h := (Equiv.trans_assoc _ _ _).symm
  one_mul := Equiv.trans_refl
  mul_one := Equiv.refl_trans
  inv_mul_cancel := Equiv.self_trans_symm

def L := {l:List ℕ // l.length = 3}

def pm : L ≃ L where
  toFun lh := ⟨[lh.1[1]!,lh.1[2]!,lh.1[0]!],by aesop⟩
  invFun lh := ⟨[lh.1[2]!,lh.1[0]!,lh.1[1]!], by aesop⟩
  left_inv lh := by
    obtain ⟨l, h⟩ := lh
    apply Subtype.ext
    simp
    -- now need some kind of induction on l
    sorry
  right_inv := sorry

#eval! pm ⟨[1,2,3],rfl⟩ -- [2,3,1]


def pm2: L ≃ L := pm * pm

def pm3: L ≃ L := pm * pm * pm

instance genbyshiftperm: Subgroup (Equiv.Perm L) where
  carrier := {pm, pm2, pm3}
  mul_mem' := by
    sorry
  one_mem' := by
    sorry
  inv_mem' := by sorry -- use pm2 for pm etc

But I am pretty sure that my definition of toFun in pm is bad (I can tell because I'm struggling to prove theorems about it). Probably it should be defined recursively. Maybe someone who is more competent at the CS side of things can suggest a better definition of pm which will make things less painful. It's still going to be painful though because to prove associativity you are going to have to do 27 calculations.

[Matt Diamond]

I suppose a quick way of defining it would be Subgroup.closure { finRotate 3 } but that would be a subgroup of permutations on Fin 3 rather than lists

[Kevin Buzzard]

Right, this is something different. Equiv.Perm L is an infinite group and the element is an infinite product of 3-cycles so I don't think the c notation can help.

[Matt Diamond]

Ah ha, I didn't catch that the lists were ℕ instead of Fin 3. Got it.

[Kevin Buzzard]

I think this is one way to do it:

import Mathlib.GroupTheory.Perm.Subgroup

-- mathlib's group, not MIL's
instance permGroup {α : Type*} : Group (Equiv.Perm α) where
  mul f g := Equiv.trans g f
  one := Equiv.refl α
  inv := Equiv.symm
  mul_assoc f g h := (Equiv.trans_assoc _ _ _).symm
  one_mul := Equiv.trans_refl
  mul_one := Equiv.refl_trans
  inv_mul_cancel := Equiv.self_trans_symm

def L := {l:List ℕ // l.length = 3}

def pm.toFun : L → L
| ⟨[a, b, c], rfl⟩ => ⟨[b, c, a], by aesop⟩

def pm.invFun : L → L
| ⟨[a, b, c], rfl⟩ => ⟨[c, a, b], by aesop⟩

def pm : L ≃ L where
  toFun := pm.toFun
  invFun := pm.invFun
  left_inv lh :=
    match lh with
    | ⟨[a, b, c], rfl⟩ => rfl
  right_inv lh :=
    match lh with
    | ⟨[a, b, c], rfl⟩ => rfl

#eval! pm ⟨[1,2,3],rfl⟩ -- [2,3,1]

def pm2: L ≃ L := pm * pm

def pm3: L ≃ L := pm * pm * pm

instance genbyshiftperm: Subgroup (Equiv.Perm L) where
  carrier := {pm, pm2, pm3}
  mul_mem' := by
    sorry
  one_mem' := by
    sorry
  inv_mem' := by sorry -- use pm2 for pm etc

Now I've got as far as the original posted code anyway.

[Matt Diamond]

From re-reading the post I still wonder if perhaps the intention was the cyclic group of order 3.

Towards that end, I would like to construct a group generated a single shift. For simplicity, take the set L = {1,2,3} and the group generated by the permutation that takes 1 to 2, 2 to 3 and 3 to 1 which is a subgroup of the group of permutations of {1,2,3}.

It seems like he's talking about just permuting the numbers 1, 2, and 3...

[Matt Diamond]

could be wrong though... @Daniel Eriksson can clarify

if he's talking about the cyclic group of order 3 and wants to define it explicitly, he could write out the carrier set as { (finRotate 3) ^ 0, (finRotate 3) ^ 1, (finRotate 3) ^ 2 }

or define it as { perm | ∃ k, perm = finRotate 3 ^ k }

[Daniel Eriksson]

Great input guys! Yes, sorry, I was trying to do to the cyclic group of order 3, brute force by using functions from list to lists. The end goal was to do a cyclic group of order p generated by a shift permutation on group elements sending (g1, g2, g3, …, gp) to (gp, g1, g2, …, g_{p-1}). I thought to do it first explicitly using the set {1,2,3}, a shift permutation generate a subgroup of S3.

Maybe I can work more abstractly and then show isomorphisms. I saw the elements in permGroup are bijections and my functions should be to, but yes I need a proof and the sets on which the bijection is defined to agree. Nice suggestion with finRotate p, sounds much cleaner. There was a similar idea in MIL where they defined a group generated by a single element whose cube is one but I didn't really understand so I tried to do it explicitly. They did (sorry should have posted this also):

def myGroup := PresentedGroup {.of () ^ 3} deriving Group

[Matt Diamond]

Let us know if you have any other questions. Like I said, if you just want a Subgroup generated by a single shift operation, def myGroup (p : ℕ) := Subgroup.closure { finRotate p } would accomplish that.

[Matt Diamond]

also, if you're curious how Mathlib proves the Cauchy theorem, you can find it at docs#exists_prime_orderOf_dvd_card

[Kevin Buzzard]

Yeah it's the same proof; I think this might be because this is the proof I was taught by John Thompson in the 80s and maybe me or one of my undergrads formalized it in the early days? I was very surprised to see someone giving it a name recently ("X's proof of Cauchy") -- I thought it was folklore (Thompson didn't name it)

[Daniel Eriksson]

I realized I can just let Z_p act on lists of group elements by rotating. I can't write just something like instance : MulAction (Multiplicative (ZMod p)) (@X G _ p)? Is there an easy way to provide a group structure on Zp? Found a field and commutative ring instance and some lift ZMod.lift for additive groups on Mathlib but don't get it working.

[Matt Diamond]

What is @X G _ p?

[Matt Diamond]

ZMod p already has an AddGroup instance

[Matt Diamond]

docs#Subgroup.zpowers / docs#AddSubgroup.zmultiples provide the (Add)Subgroup generated by a single element

[Matt Diamond]

if you still need help, I would advise providing an #mwe showing what you're trying to construct (even if it doesn't completely work)

I have a feeling what you're trying to do is much easier / simpler than you think