a concrete group

Stream: new members

[Jalex Stark]

I'd like to define a group via its presentation, prove that it's finite, and then compute its character table. I read some of the files in mathlib/algebra/group but still don't really know where to start. Could anyone point me to an example that might be instructive?

[Kenny Lau]

what's the group?

[Kenny Lau]

I don't really think it's best to define a group via its presentation

[Kenny Lau]

rather than going from large to small, we go from small to large

[Johan Commelin]

@Kenny Lau But we'll need to be able to deal with this, right? Presentations are pervasive in maths

[Johan Commelin]

@Jalex Stark In mathlib, you can find free groups. And subgroups. And quotients. That should allow you to build your group. And didn't a student of Scott even do finitely presented groups?

[Kenny Lau]

I guess groupprops would be a good source for proofs using presentations

[Johan Commelin]

It might be in mathlib already

[Kenny Lau]

do we have normal closure?

[Johan Commelin]

Yep

[Johan Commelin]

@Jalex Stark You probably want to look at https://github.com/leanprover-community/mathlib/blob/0eea0d9fc53bd037da13abdf5d95a711cbd0c288/src/group_theory/presented_group.lean

[Johan Commelin]

However, be warned that proving that this thing is finite is probably going to be quite awkard

[Kenny Lau]

https://groupprops.subwiki.org/wiki/Equivalence_of_presentations_of_dicyclic_group

[Kenny Lau]

maybe we would want to be able to do something like this

[Johan Commelin]

@Kenny Lau Certainly. It would be great to have all sorts of stuff like that.

[Jalex Stark]

Jalex Stark You probably want to look at https://github.com/leanprover-community/mathlib/blob/0eea0d9fc53bd037da13abdf5d95a711cbd0c288/src/group_theory/presented_group.lean

I'll work on understanding this file (on my first pass, I have a mathematical understanding but I don't yet have a good guess of how to translate a group presentation like < a , b | a^2 = 1, abab\inv = 1> into code)

[Jalex Stark]

what's the group?

The groups I'm interested are described here https://en.wikipedia.org/wiki/Extra_special_group
quantum information people call them the pauli group on n qudits

[Jalex Stark]

However, be warned that proving that this thing is finite is probably going to be quite awkard

The proof I have in mind is to define a canonical form, that is a list of words in the group together with a proof that any word in the group is equal to one of the canonical ones
Do you mean awkward like, I will have to understand details about how lean represents finite lists?

[Johan Commelin]

@Jalex Stark Cool, I think it's really good if people work on examples. But usually it's not something that Lean excels at. Let's break down a bit what you have to do. We've got the following definition:

/-- Given a set of relations, rels, over a type α, presented_group constructs the group with
generators α and relations rels as a quotient of free_group α.-/
def presented_group (rels : set (free_group α)) : Type :=
quotient_group.quotient $ group.normal_closure rels

[Johan Commelin]

You gave as example, a group generated by two elements a and b. So you need a type with two elements. You could choose bool or fin 2, or roll your own type:

inductive pauli_two_gens | a | b

[Johan Commelin]

After that, you need the relations. So you do something like

open pauli_two_gens

def pauli_two_rels : set (free_group pauli_two_gens) :=
{ x | x = a^2 \or x = a * b * a * b \-1 }

[Johan Commelin]

Once you have those, you should be able to write

def pauli_two := presented_group pauli_two_rels

[Jalex Stark]

Wow, thanks! I will play with your definitions when I get home from work.

[Johan Commelin]

Note that I didn't test any of these in Lean. So they might be full of hidden mistakes

[Alex J. Best]

I did a little testing earlier and the following works

open presented_group

#check free_group (fin 2)

def r : free_group (fin 2) := free_group.of 0
def s : free_group (fin 2) := free_group.of 1

--check everything makes sense so far
#eval to_bool (r * (s⁻¹) = 1) -- if you use pauli_two_gens like Johan you need to tell lean that this is decidable
#eval to_bool (r * (r⁻¹) = 1)

-- either one of the following ways works, but lean does not automatically work out what 0 or 1 are inside the free group so we use r and s
def my_rels : set (free_group (fin 2)) :=
{ x | x = r^2 ∨ x = r * s * r * s⁻¹ }

def my_rels2 : set (free_group (fin 2)) :=
{r^2, r*s*r*s⁻¹}

def pauli_two := presented_group my_rels2 -- or my_rels

[Mario Carneiro]

I would try defining your "canonical forms" as a type in its own right, then construct the group operation and prove that it is generated the way you expect

[Mario Carneiro]

You will have to do essentially all this work anyway in order to prove that the free group modulo relations is in fact finite

[Johan Commelin]

Whut? How does this work:

def my_rels2 : set (free_group (fin 2)) :=
{r^2, r*s*r*s⁻¹}

Has this syntax always been available in lean?

[Johan Commelin]

I guess it is, but I just never really realized...

[Johan Commelin]

Always used the {x | x = _ \or _ \or _} stuff

[Kevin Buzzard]

I believe it unfolds to something worse than your option ;-)

[Kevin Buzzard]

example (x : ℕ) : x ∈ ({4,6} : set ℕ) ↔ x = 6 ∨ x = 4 ∨ false := iff.rfl

[Kevin Buzzard]

I would try defining your "canonical forms" as a type in its own right, then construct the group operation and prove that it is generated the way you expect

Proving associativity will be a nightmare like this.

[Mario Carneiro]

I don't see why, provided you set up the operation right

[Jalex Stark]

Using the definitions that Alex J Best gave, it seems like the type system has less of an understanding of the claim "pauli_two is a group" than the claim "free_group (fin 2)" is a group.

Lean knows how to deal with
theorem order_not_two : ∀ x : (free_group (fin 3)), x≠ 1 → x * x ≠ 1

but not
theorem order_two : ∀ x : pauli_two, x * x = 1
in which case it says it can't find has_mul or has_one for pauli_two

[Jalex Stark]

the presented_group file has this line
instance (rels : set (free_group α)) : group (presented_group (rels)) :=
quotient_group.group _

and I guess I expected it to have something like
instance group : (presented_group rels)

[Kevin Buzzard]

Can you post the current working version of your code? The errors just mean that there is no term of tyoe group G for your group G

[Jalex Stark]

import tactic
import group_theory.presented_group

import algebra.group

-- open presented_group

#check free_group (fin 3)

def J : free_group (fin 3) := free_group.of 0
def x : free_group (fin 3) := free_group.of 1
def z : free_group (fin 3) := free_group.of 2

--check everything makes sense so far
#eval to_bool (z * (x⁻¹) = 1) -- if you use pauli_two_gens like Johan you need to tell lean that this is decidable
#eval to_bool (J * (J⁻¹) = 1)

def my_rels2 : set (free_group (fin 3)) :=
{J^2, x^2, z^2, J*x*z*x⁻¹*z⁻¹}

def pauli_two := presented_group my_rels2

#check my_rels2
#check pauli_two
#check group pauli_two

#check has_pow (free_group (fin 3)) ℕ
#check has_pow (pauli_two) ℕ

open free_group

theorem order_not_two : ∀ x : (free_group (fin 3)), x≠ 1 → x * x ≠ 1 :=
begin
rintros  ⟨ L⟩ ,
induction L with hd tl h,
simp,
end

theorem order_two : ∀ x : pauli_two, x * x = 1 := by sorry

[Kevin Buzzard]

Can you put it all in quotes so it displays properly?

[Kevin Buzzard]

```lean at the top

[Kevin Buzzard]

And ``` at the end

[Jalex Stark]

there is no term of type group G for your group G

If I construct such a term manually, how do I get the compiler to notice it when I'm writing statements about G?

[Kevin Buzzard]

which version of lean/mathlib are you using? Your proof of order_not_two doesn't compile for me

[Jalex Stark]

oh, sorry, it doesn't compile for me either

[Jalex Stark]

it had been a sorry and I had been trying to prove it and forgot to revert it before posting

[Kevin Buzzard]

instance : group pauli_two := by unfold pauli_two; apply_instance

[Kevin Buzzard]

is what you're missing.

[Kevin Buzzard]

or alternatively

@[derive group]
def pauli_two := presented_group my_rels2

[Kevin Buzzard]

The type class inference system handles the job of coming up with e.g. what notation means for a given type. Your definition of pauli_two is just a definition of a new type -- if you hover over presented_group then you'll see that it just returns something of type Type.

[Jalex Stark]

that @derive clause makes a lot of sense to me coming from programming in ocaml

[Kevin Buzzard]

OK great, it's brand spanking new in Lean.

[Jalex Stark]

would it make sense for presented_group to return a type decorated with a group instance?

[Kevin Buzzard]

I am not a computer scientist, all I can say is that because groups are "partially bundled" this is what we have to do.

[Kevin Buzzard]

Another alternative is that presented_group returns a term of type Group where Group is the category of groups.

[Jalex Stark]

ok, I think I can accept this as a fact of life.

[Kevin Buzzard]

If you do it that way then all your maps between groups will be morphisms in the category and you'll lose some of the cool advantages of functional programming because they won't be functions any more. Or something.

[Kevin Buzzard]

In short, this is a design decision

[Kevin Buzzard]

and the less I say about it the better ;-) because I know nothing about the pros and cons. There is a section about this in the mathlib paper.

[Kevin Buzzard]

Note that theorem order_two : ∀ x : presented_group my_rels2, x * x = 1 := by sorry works fine, because the typeclass system knows that presented_group R is a group.

[Kevin Buzzard]

section 4.1.1 of the mathlib paper talks about the design decisions.

[Jalex Stark]

i guess the term lean ∀ x : presented_group my_rels2, x * x = 1 can be turned into the termlean ∀ x:pauli_two, x * x = 1 by one application of definitional equality, but you can't make that substitution before the compiler has made up its mind about whether the second term makes sense

[Jalex Stark]

I don't know how to access a statment like "if w \in rels, then w = 1 in presented_group rels". I also don't know how to access the quotient map from my free group to my presented group. There is a lemma in the presented_groups file that looks awfully relevant but I can't figure out how to make any interesting terms with it.

lemma to_group_eq_one_of_mem_closure : ∀ x ∈ group.normal_closure rels, F x = 1 :=
λ x w, (is_group_hom.mem_ker F).1  ((closure_rels_subset_ker h) w)

(I would love if the answer to my question was "read X tutorial or Y book chapter more closely to understand Z fundamental concept that you clearly lack understanding of")

-- goal: define the two qubit pauli group
import tactic
import group_theory.presented_group

import algebra.group

open presented_group

def gen_J : free_group (fin 3) := free_group.of 0
def gen_x : free_group (fin 3) := free_group.of 1
def gen_z : free_group (fin 3) := free_group.of 2

def my_rels : set (free_group (fin 3)) :=
{gen_J^2, gen_x^2, gen_z^2, gen_J*gen_x*gen_z*gen_x⁻¹*gen_z⁻¹}

@[derive group]
def pauli_two := presented_group my_rels

def J := ((presented_group.of 0) : pauli_two)
def x := ((presented_group.of 1) : pauli_two)
def z := ((presented_group.of 2) : pauli_two)

theorem rel1 : J^2 = 1 :=
begin
sorry
end

[Alex J. Best]

Its possible a lot of the lemmas you are interested in are actually just lemmas about group quotients, and so in group_theory/quotient_group.lean rather than this file. In particular the one you mentioned to_group_eq_one_of_mem_closure is a bit more complex, it has the additional assumptions defined above in that file

variables {β : Type} [group β] {f : α → β} {rels : set (free_group α)}

local notation `F` := free_group.to_group f

variable (h : ∀ r ∈ rels, F r = 1)

so its to do with when you have a map from your generating letters into some other group such that rels end up in the kernel then the universal property of a presented group gives you a map to the other group etcetc..

[Jalex Stark]

Thanks, Alex! I'm currently convinced that if I read the quotient_group file closely enough, I will learn how to access the quotient map

[Alex J. Best]

Yeah I think this area (presented_group) needs many more helper lemmas and things, I did it one way, there may be an easier one but I couldn't find it yet:

theorem rel1 : J^2 = 1 :=
begin
    rw J,
    rw presented_group.of,
    rw ← gen_J,
    change ((quotient_group.mk (gen_J ^2)) : quotient_group.quotient (group.normal_closure my_rels)) = 1,
    rw ← is_group_hom.mem_ker (quotient_group.mk),
    rw quotient_group.ker_mk,
    apply set.mem_of_subset_of_mem (group.subset_normal_closure),
    rw my_rels,
    simp,
end

[Alex J. Best]

Probably a nicer refactor is

def mk {α : Type} {rels : set (free_group α)} (x : free_group α) : presented_group rels :=
quotient_group.mk x

lemma mk_eq_one_of_mem_rels {α : Type} {rels : set (free_group α)} {x : free_group α} (h : x ∈ rels) : (mk x : presented_group rels) = 1 :=
begin
    refine (is_group_hom.mem_ker (quotient_group.mk)).mp _,
    rw quotient_group.ker_mk,
    exact set.mem_of_subset_of_mem (group.subset_normal_closure) h,
end

theorem rel1 : J^2 = 1 :=
begin
    change mk (gen_J ^2) = 1,
    apply mk_eq_one_of_mem_rels,
    simp [my_rels],
end