Hall's universal group

Stream: new members

[Matt Diamond]

I was reading about Hall's universal group and thought it might be fun to try to define it in Lean. I read that it was a direct limit of a sequence of embeddings, so I tried to assemble it using docs#DirectLimit. However, this is way outside of my comfort zone and I have no idea if any of this is correct:

import Mathlib

open Function

variable {α : Type}

def permute (G : Type) : Type := Equiv.Perm G

instance {G : Type} [Group G] : Group (permute G) := Equiv.Perm.permGroup

def permute_embed (G : Type) [Group G] : G ↪ permute G :=
⟨MulAction.toPerm, MulAction.toPerm_injective⟩

def S3 := Equiv.Perm (Fin 3)

@[reducible]
def Γ (n : ℕ) : Type := permute^[n] S3

instance : (n : ℕ) → Group (Γ n)
| 0     => by
  unfold Γ
  rw [iterate_zero_apply]
  exact Equiv.Perm.permGroup
| n + 1 => by
  unfold Γ
  rw [iterate_succ_apply']
  exact Equiv.Perm.permGroup

def Γ_embed_succ {k} : Γ k ↪ Γ (k + 1) :=
by
  unfold Γ
  rw [iterate_succ_apply' permute k S3]
  exact permute_embed (permute^[k] S3)

def Γ_embed (i j : ℕ) (hle : i ≤ j) : Γ i ↪ Γ j :=
Nat.leRec (Embedding.refl _) (fun _ _ emb => emb.trans Γ_embed_succ) hle

instance : DirectedSystem Γ fun x1 x2 x3 => Γ_embed x1 x2 x3 :=
by
  constructor
  · intro i Γ_i
    simp [Γ_embed]
  · intro k j i i_le_j j_le_k Γ_i
    unfold Γ_embed
    induction j_le_k using Nat.leRec with
    | refl => simp
    | le_succ_of_le j_le ih =>
      rw [Nat.leRec_succ _ _ j_le, Embedding.trans_apply, ih]
      rw [Nat.leRec_succ _ _ (i_le_j.trans j_le), Embedding.trans_apply]

-- Hall's universal group... maybe?
def U := DirectLimit Γ Γ_embed

instance : Group U := sorry

Is U Hall's universal group? If not, how would one go about defining it?

[Matt Diamond]

Actually I think this might work better with MonoidHoms instead of embeddings, but I'm having trouble defining Γ k →* Γ (k + 1). I want to be able to use MulAction.toPermHom (Γ k) (Γ k) but the types don't quite line up.

[Matt Diamond]

MulAction.toPermHom (Γ k) (Γ k) gives me Γ k →* Equiv.Perm (Γ k), and I have a lemma that says Equiv.Perm (Γ k) = Γ (k + 1), but I'm not sure how to stitch those facts together to get Γ k →* Γ (k + 1). Maybe I'll need to build it from the ground up.

Edit: Ah, the problem was that I defined Γ using Function.iterate. Works a lot better as a simple recursive definition. No more issues.

[Damiano Testa]

I never worked with it, but there is docs#FirstOrder.Language.IsFraisse and I wonder if you can leverage the API there to get Hall's universal group from it.

[Edward van de Meent]

it seems lean doesn't like permute^[n], as it isn't reducible... the following seems to work a bit better:

import Mathlib

open Function

variable {α : Type}


def permute_embed (G : Type) [Group G] : G ↪ Equiv.Perm G :=
⟨MulAction.toPerm, MulAction.toPerm_injective⟩

def S3 := Equiv.Perm (Fin 3)

def Γ : ℕ → Type
| 0 => S3
| n + 1 => Equiv.Perm (Γ n)

instance {α : Type*} : α ≃ α := Equiv.refl α

instance : (n : ℕ) → Group (Γ n)
| 0     => inferInstanceAs (Group (Equiv.Perm (Fin 3)))
| n + 1 => inferInstanceAs (Group (Equiv.Perm (Γ n)))

def Γ_mulHom_succ {k} : Γ k →* Γ (k + 1) := by
  exact MulAction.toPermHom (Γ k) (Γ k)


def Γ_embed_succ {k} : Γ k ↪ Γ (k + 1) := by
  exact permute_embed _

[Matt Diamond]

Okay, I actually think I've got Hall's Universal Group defined:

import Mathlib

def S3 := Equiv.Perm (Fin 3)

def Γ : ℕ → Type
| 0     => S3
| n + 1 => Equiv.Perm (Γ n)

lemma Γ_zero : Γ 0 = Equiv.Perm (Fin 3) := rfl
lemma Γ_succ {k} : Γ k.succ = Equiv.Perm (Γ k) := rfl

instance : (n : ℕ) → Group (Γ n)
| 0     => Equiv.Perm.permGroup
| _ + 1 => Equiv.Perm.permGroup

def Γ_hom_succ {k} : Γ k →* Γ (k + 1) :=
MulAction.toPermHom (Γ k) (Γ k)

def Γ_hom (i j : ℕ) (hle : i ≤ j) : Γ i →* Γ j :=
Nat.leRec (MonoidHom.id _) (fun _ _ hom => Γ_hom_succ.comp hom) hle

instance : DirectedSystem Γ fun x1 x2 x3 => Γ_hom x1 x2 x3 :=
by
  constructor
  · intro i Γ_i
    simp [Γ_hom]
  · intro k j i i_le_j j_le_k Γ_i
    unfold Γ_hom
    induction j_le_k using Nat.leRec with
    | refl => simp
    | le_succ_of_le j_le ih =>
      rw [Nat.leRec_succ _ _ j_le, MonoidHom.comp_apply, ih]
      rw [Nat.leRec_succ _ _ (i_le_j.trans j_le), MonoidHom.comp_apply]

-- Hall's universal group
abbrev U := DirectLimit Γ Γ_hom

noncomputable instance : Group U := inferInstance

(I originally defined the Group instance myself before finding docs#DirectLimit.instGroup. Very convenient!)

[Matt Diamond]

Now I just need to figure out how to prove that all countable locally finite groups embed into it