## Stream: new members

### Topic: a concrete group

#### Jalex Stark (Dec 18 2019 at 04:08):

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 (Dec 18 2019 at 04:15):

what's the group?

#### Kenny Lau (Dec 18 2019 at 04:15):

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

#### Kenny Lau (Dec 18 2019 at 04:15):

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

#### Johan Commelin (Dec 18 2019 at 05:08):

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

#### Johan Commelin (Dec 18 2019 at 05:09):

@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 (Dec 18 2019 at 05:09):

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

#### Johan Commelin (Dec 18 2019 at 05:09):

It might be in mathlib already

#### Kenny Lau (Dec 18 2019 at 05:10):

do we have normal closure?

Yep

#### Johan Commelin (Dec 18 2019 at 05:10):

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

#### Johan Commelin (Dec 18 2019 at 05:11):

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

#### Kenny Lau (Dec 18 2019 at 05:12):

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

#### Kenny Lau (Dec 18 2019 at 05:12):

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

#### Johan Commelin (Dec 18 2019 at 05:17):

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

#### Jalex Stark (Dec 18 2019 at 07:52):

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 (Dec 18 2019 at 07:53):

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 (Dec 18 2019 at 07:56):

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 (Dec 18 2019 at 08:08):

@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 (Dec 18 2019 at 08:10):

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 (Dec 18 2019 at 08:12):

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 (Dec 18 2019 at 08:12):

Once you have those, you should be able to write

def pauli_two := presented_group pauli_two_rels


#### Jalex Stark (Dec 18 2019 at 08:13):

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

#### Johan Commelin (Dec 18 2019 at 08:15):

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

#### Alex J. Best (Dec 18 2019 at 08:24):

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 (Dec 18 2019 at 08:24):

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 (Dec 18 2019 at 08:25):

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 (Dec 18 2019 at 08:29):

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 (Dec 18 2019 at 08:30):

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

#### Johan Commelin (Dec 18 2019 at 08:30):

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

#### Kevin Buzzard (Dec 18 2019 at 08:34):

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

#### Kevin Buzzard (Dec 18 2019 at 08:38):

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

#### Kevin Buzzard (Dec 18 2019 at 08:39):

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 (Dec 18 2019 at 08:40):

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

#### Jalex Stark (Dec 21 2019 at 13:06):

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 (Dec 21 2019 at 13:12):

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 (Dec 21 2019 at 13:12):

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 (Dec 21 2019 at 13:13):

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 (Dec 21 2019 at 13:14):

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

#### Kevin Buzzard (Dec 21 2019 at 13:15):

 lean  at the top

#### Kevin Buzzard (Dec 21 2019 at 13:15):

And    at the end

#### Jalex Stark (Dec 21 2019 at 13:20):

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 (Dec 21 2019 at 13:21):

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

#### Jalex Stark (Dec 21 2019 at 13:22):

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

#### Jalex Stark (Dec 21 2019 at 13:22):

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

#### Kevin Buzzard (Dec 21 2019 at 13:22):

instance : group pauli_two := by unfold pauli_two; apply_instance

#### Kevin Buzzard (Dec 21 2019 at 13:22):

is what you're missing.

#### Kevin Buzzard (Dec 21 2019 at 13:23):

or alternatively

@[derive group]
def pauli_two := presented_group my_rels2


#### Kevin Buzzard (Dec 21 2019 at 13:25):

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 (Dec 21 2019 at 13:25):

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

#### Kevin Buzzard (Dec 21 2019 at 13:25):

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

#### Jalex Stark (Dec 21 2019 at 13:26):

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

#### Kevin Buzzard (Dec 21 2019 at 13:26):

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 (Dec 21 2019 at 13:27):

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

#### Jalex Stark (Dec 21 2019 at 13:27):

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

#### Kevin Buzzard (Dec 21 2019 at 13:27):

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 (Dec 21 2019 at 13:28):

In short, this is a design decision

#### Kevin Buzzard (Dec 21 2019 at 13:28):

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 (Dec 21 2019 at 13:29):

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 (Dec 21 2019 at 13:31):

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

#### Jalex Stark (Dec 21 2019 at 13:34):

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 (Dec 21 2019 at 14:32):

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 (Dec 21 2019 at 15:02):

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 (Dec 21 2019 at 15:16):

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 (Dec 21 2019 at 15:44):

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 (Dec 21 2019 at 17:21):

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


Last updated: May 12 2021 at 23:13 UTC