Group theory

Stream: new members

[Sai Gopal]

If I want to use pre defined definitions and theorems in groip theory, how shld I import them?
For instance, to import topology it is import topology.basic

[Johan Commelin]

import topology.basic means: grab everything that's in src/topology/basic.lean and import it into the environment.

[Johan Commelin]

So now import group_theory.<some_nice_file> that you find by browsing mathlib

[Sai Gopal]

instead of .<>
Can you tell me which file has all basics of GT ?

[Johan Commelin]

You should rather be precise about what you want to do.

[Johan Commelin]

What is the exact maths statement that you want to formalize in Lean?

[Johan Commelin]

There is also the directory src/algebra/group/ which contains a lot of low-level stuff: https://github.com/leanprover-community/mathlib/tree/master/src/algebra/group

[Sai Gopal]

So How do I include this ?

[Kevin Buzzard]

Import the name of the file

[Holly Liu]

if i were to construct a specific kind of free group, would i do something like this:

structure some_specific_free_group (G : Type) [free_group G] :=
--proofs of its properties here

which came from modifying this code slightly:

structure subgroup (G : Type) [group G] :=
(carrier : set G)
(one_mem' : (1 : G) ∈ carrier)
(mul_mem' {x y} : x ∈ carrier → y ∈ carrier → x * y ∈ carrier)
(inv_mem' {x} : x ∈ carrier → x⁻¹ ∈ carrier)

or should i use something like this:

class group (G : Type) extends has_mul G, has_one G, has_inv G :=
(mul_assoc : ∀ (a b c : G), a * b * c = a * (b * c))
(one_mul : ∀ (a : G), 1 * a = a)
(mul_left_inv : ∀ (a : G), a⁻¹ * a = 1)

(i found these in the tutorial project linked in previous messages)

[Adam Topaz]

What would you like to do specifically? Would you like to declare that a specific group $G$ is a free group, or, given a type $\alpha$, consider "the" free group on $\alpha$?

[Holly Liu]

I would like to create a new structure/class (i'm not sure what the difference is yet) that is a free group plus some other properties. I think this is like declaring a free group, or declaring that it has free group properties.

[Eric Wieser]

It's maybe not what you want, but we have docs#is_free_group

[Eric Wieser]

As well as docs#free_group

[Holly Liu]

could someone briefly walk me through what these are doing:

noncomputable theory
universes u w

/-- `is_free_group G` means that `G` has the universal property of a free group,
That is, it has a family `generators G` of elements, such that a group homomorphism
`G →* X` is uniquely determined by a function `generators G → X`. -/
class is_free_group (G : Type u) [group G] : Type (u+1) :=
(generators : Type u)
(of : generators → G)
(unique_lift' : ∀ {X : Type u} [group X] (f : generators → X),
                ∃! F : G →* X, ∀ a, F (of a) = f a)

instance free_group_is_free_group {A} : is_free_group (free_group A) :=
{ generators := A,
  of := free_group.of,
  unique_lift' := begin
    introsI X _ f,
    have := free_group.lift.symm.bijective.exists_unique f,
    simp_rw function.funext_iff at this,
    exact this,
  end }

and

instance : group (free_group α) :=
{ mul := (*),
  one := 1,
  inv := has_inv.inv,
  mul_assoc := by rintros ⟨L₁⟩ ⟨L₂⟩ ⟨L₃⟩; simp,
  one_mul := by rintros ⟨L⟩; refl,
  mul_one := by rintros ⟨L⟩; simp [one_eq_mk],
  mul_left_inv := by rintros ⟨L⟩; exact (list.rec_on L rfl $
    λ ⟨x, b⟩ tl ih, eq.trans (quot.sound $ by simp [one_eq_mk]) ih) }

to me, these look like they are both declaring free groups?

[Kevin Buzzard]

To give a term of the first type is_free_group G is to give a proof that G is abstractly isomorphic to a free group (more precisely, it is to give an isomorphism between G and a free group).

The instance is a term of type is_free_group (free_group A) so it's a proof that the free group on a type A is a free group.

The final instance is the proof that the free group on a type alpha is a group.

[Adam Topaz]

For example, you could fill in the following sorry:

import group_theory.is_free_group

example : is_free_group (multiplicative ℤ) :=
{ generators := punit,
  of := λ x, multiplicative.of_add 1,
  unique_lift' := sorry }

[Adam Topaz]

Which says that the group of integers is a free group on a single element.

[Eric Wieser]

And then you could PR it to mathlib :)

[Holly Liu]

hi! i was wondering if you could explain what the following code is doing? i understand that 1 is the identity here. how is it being declared in order to be used in the axioms one_mul and mul_one later on?

/-- The canonical map from `list (α × bool)` to the free group on `α`. -/
def mk (L) : free_group α := quot.mk red.step L

...

instance : has_one (free_group α) := ⟨mk []⟩
lemma one_eq_mk : (1 : free_group α) = mk [] := rfl

instance : inhabited (free_group α) := ⟨1⟩

from https://github.com/leanprover-community/mathlib/blob/4ace3b73b4a3cdafe51f3c1a01fe2b583ae0c499/src/group_theory/free_group.lean#L76

[Eric Wieser]

instance : has_one _ is specifying what 1 means in that example. Is that your question?

[Holly Liu]

sorry for the late reply. yes, i'm confused on what the notation mk [] means? i think this also leads to my question of what quot.mk red.step L is?

[Holly Liu]

thanks again.

[Kyle Miller]

@Holly Liu Recall that a free group can be presented as words of generators and inverses of generators, modulo the relation $u x^{\pm 1} x^{\mp 1}v=uv$ where $x$ is a generator and $u$ and $v$ are words. A nice fact about this relation is that you can apply this relation repeatedly until it doesn't apply anymore (in the left-to-right direction), and it will always eventually reduce the word to its normal form.

In mathlib, words are represented by the type list (α × bool), lists of pairs of a generator and a boolean. The boolean is true or false depending on whether it is the generator or its inverse. For example [(x, tt), (y, tt), (x, ff)] represents $xyx^{-1}$.

A single application of the reduction relation is represented by the following inductive type:

/-- Reduction step: `w * x * x⁻¹ * v ~> w * v` -/
inductive red.step : list (α × bool) → list (α × bool) → Prop
| bnot {L₁ L₂ x b} : red.step (L₁ ++ (x, b) :: (x, bnot b) :: L₂) (L₁ ++ L₂)

If you squint hard enough, you might see the resemblance.

Then, the free group with generators from the type α is given by the type quot red.step α (this is the definition of free_group). This creates a quotient type, where terms of quot red.step α correspond to equivalence classes under the equivalence relation generated by red.step.

The way you take a word w and put it into the quotient type is quot.mk red.step w. In math speak, this is like writing brackets around an element that represents an element of a quotient (it's like $[w]$).

In Lean, [] is the empty list, so quot.mk red.step [] is "the empty word as an element of the free group."

[Holly Liu]

@Kyle Miller thanks for the very thorough explanation.

[Holly Liu]

in this snippet, what are the notations $ and @ doing?

/-- The free group over a type, i.e. the words formed by the elements of the type and their formal
inverses, quotient by one step reduction. -/
def free_group (α : Type u) : Type u :=
quot $ @free_group.red.step α

[Kyle Miller]

I like to think of $ as a pair of parentheses stacked on top of each other, nailed together. It's a notation that basically means "open parenthesis, then insert the close parenthesis at the end of the expression." So, it's the same as

/-- The free group over a type, i.e. the words formed by the elements of the type and their formal
inverses, quotient by one step reduction. -/
def free_group (α : Type u) : Type u :=
quot (@free_group.red.step α)

What @ does is make all implicit arguments explicit. https://leanprover.github.io/reference/expressions.html#implicit-arguments

[Holly Liu]

ah i see.

[Malvin Gattinger]

Ah, so $ does the same as in Haskell, nice to know.

[Kyle Miller]

This is the type:

free_group.red.step : free_group.red.step : Π {α : Type u_1}, list (α × bool) → list (α × bool) → Prop

So if you want to pass the α in, you can use @. The issue is that there's nothing else in the expression that can help Lean infer what α should be.

[Kyle Miller]

Malvin Gattinger said:

Ah, so $ does the same as in Haskell, nice to know.

Yep, though it's implemented a bit differently. Rather than being an operator in its own right, it's defined as notation in init/core.lean:

notation f ` $ `:1 a:0 := f a

You can still do ($) as a Haskeller would expect.

[Malvin Gattinger]

Ah, thanks. The ( ) notation to turn infix into prefix works just for $ or in general with all infix notations?

[Eric Wieser]

It works on all infix notation

[Eric Wieser]

We also have (+ 1) which expands to λ x, x + 1 for all infix operators

[Eric Wieser]

So I guess ($ x) is docs#function.eval x

[Holly Liu]

Kyle Miller said:

This is the type:

free_group.red.step : free_group.red.step : Π {α : Type u_1}, list (α × bool) → list (α × bool) → Prop

So if you want to pass the α in, you can use @. The issue is that there's nothing else in the expression that can help Lean infer what α should be.

so if we were to leave out the @, say we have quot free_group.red.step α, then what is α? is it still Type u? i think i'm confused about when we would want Lean to infer the type, and why we want it to infer it here when we're already giving it the type by writing (α : Type u). read the doc and i think i understand.

[Eric Rodriguez]

Eric Wieser said:

It works on all infix notation

if by infix you mean infix, then $ isn't defined in that way:

notation f ` $ `:1 a:0 := f a

[Eric Rodriguez]

oh I see this was mentioned above

[Eric Wieser]

I think by infix I mean "anything that unfolds to the same type of notation command as infix"

[Eric Wieser]

#print notation doesn't show anything but notation; the other keywords seem to just be shorthands

[Kyle Miller]

@Holly Liu quot free_group.red.step α would be an error, because quot only takes a single explicit argument. This is the type for quot:

quot : Π {α : Sort u}, (α → α → Prop) → Sort u

It takes (implicitly) a type and (explicitly) a relation on that type, producing a new type.

The following are equivalent:

def free_group_1 (α : Type*) : Type* := quot (@free_group.red.step α)
def free_group_2 (α : Type*) : Type* := @quot (list (α × bool)) free_group.red.step
def free_group_3 (α : Type*) : Type* := @quot (list (α × bool)) (@free_group.red.step α)

In this last one, we explicitly give all the implicit arguments.

The issue I was talking about is this:

def free_group_4 (α : Type*) : Type* := quot free_group.red.step

Notice that it doesn't ever use α. Lean will figure out it's a quotient on list (_ x bool), but it can't figure out what to put for the underscore. This is the "don't know how to synthesize placeholder" error message.

[Holly Liu]

ok i think that makes sense. thanks a lot! that was really clear and easy to understand.

[Holly Liu]

i was wondering if there is an expression equivalent to fin n for {n : nat} that uses an abstract variable instead of n but still defines a group with a certain number of elements?

[Eric Wieser]

{G : Type*} [group G] [fintype G]?

[Eric Wieser]

fintype.card G is then the number of elements

[Kyle Miller]

and if you want the cardinality to be a variable, it could be

(n : ℕ) (G : Type*) [group G] [fintype G] (hcard : fintype.card G = n)

If you have an application in mind, it would be helpful if you explained what you were trying to do -- I'm not sure exactly what you're asking for.

[Holly Liu]

sure:

def braid (n : ℕ) := Π n, list((fin n) × bool)
def braid3 := braid 3
#eval braid3.length

i'm trying to define a braid on a finite number of strands, though I wonder if list((fin n) x bool) is appending the bool to the set rather than its elements? also, braid is of type Type which i think is keeping me from using list operations like length on it? i'm not sure how to go about this.

[Kevin Buzzard]

Can you post a link to the maths definition you're trying to formalise?

[Holly Liu]

i'm not sure if braid groups are formalized yet? i think i'm mostly using free groups: https://github.com/leanprover-community/mathlib/blob/49bf1fdecf56ce9ae3e6d15953896996af596c07/src/group_theory/free_group.lean#L385

[Holly Liu]

oh wait was this what you meant? https://en.wikipedia.org/wiki/Braid_group

[Kevin Buzzard]

Oh we're talking about braid groups? Why not just formalise them as the presentation on that Wikipedia page?

[Holly Liu]

do you mean like when its saying 'the group whose elements are equivalence classes of n-braids (e.g. under ambient isotopy), and whose group operation is composition of braids'? or is there code somewhere i'm not seeing?

[Kevin Buzzard]

Oh, I just mean that there's an explicit description of the braid group $B_n$ as the quotient of the free group on $\sigma_1,\sigma_2,\ldots,\sigma_{n-1}$ by (the normal subgroup generated by) the relations $\sigma_i\sigma_{i+1}\sigma_i=\sigma_{i+1}\sigma_i\sigma_{i+1}$ for $1\leq i\leq n-2$ and $\sigma_i\sigma_j=\sigma_j\sigma_i$ for $1\leq i\leq j-2\leq n-3$. That wouldn't be too hard to put into Lean.

[David Wärn]

There is docs#presented_group

[Holly Liu]

ah ok, i'll try that. i don't fully understand what all those words mean together yet...

[Holly Liu]

oh so would we just construct a specific quotient of the free group that contains only those two equivalence classes?

[Kevin Buzzard]

Do you understand what a presentation of a group is (in maths, nothing to do with Lean)? If not then you should maybe read up on that first. I'm suggesting that using group presentations is a painless way to define braid groups in Lean.

[Holly Liu]

hm alright, i'll read up on that.

[Kevin Buzzard]

The Wikipedia page you linked to contains a presentation of the braid group which can be turned into a lean definition once you know something about presentations.

[Holly Liu]

i'm still a bit confused on how to define braids using presentation groups. i'm trying to understand the presentation groups file and have a bunch of miscellaneous questions:

1. why do set and equivalence relations map to a Prop in their definitions: def set (α : Type u) := α → Prop and constant quot : Π {α : Sort u}, (α → α → Prop) → Sort u where r : (α → α → Prop)?

2. for universe u, #check Sort u evaluates Sort u as having type Type u, however the documentation says types are really just Sorts, i.e. Prop abbreviates Sort 0, Type abbreviates Sort 1, and Type u abbreviates Sort (u+1). is the point of Sort just to have an umbrella set that includes both Prop and Type?

3. i see this of term often and i'm having trouble understanding it. for example:

/-- `of` is the canonical map from `α` to a presented group with generators `x : α`. The term `x` is
mapped to the equivalence class of the image of `x` in `free_group α`. -/
def of {rels : set (free_group α)} (x : α) : presented_group rels :=
quotient_group.mk (free_group.of x)

why do we want to map the terms x : α to the equivalence classes? i feel like there's some math here i'm not understanding. also, what is the 'image of x in free_group α'? is this referring to another function?

[Adam Topaz]

You seem to have at least three unrelated questions here... The following is an explanation about item 3

Suppose $S$ is a set, and $R$ is a set of elements in $F(S)$ where $F(T)$ denotes the free group on a set $T$. Write $N(R)$ for the smallest normal subgroup of $F(S)$ which contains $R$. A presentation of a group $G$ is, mathematically speaking, an isomorphism $F(S)/N(R) \cong G$ for some $S$ and $R$.

In mathlib, free_group α is simply $F(\alpha)$, and the map free_group.of is the canonical function $\alpha \to F(\alpha)$. The set $R$ above corresponds to rels in your code, and quotient_group.mk in this case is the quotient map $F(\alpha) \to F(\alpha)/N(rels)$. So if you start with a in $\alpha$, you first map to $F(\alpha)$ using free_group.of, then to the quotient by $N(rels)$ using quotient_group.mk.

[Holly Liu]

Adam Topaz said:

have at least three unrelated questions here...

yeah i keep going down these rabbit holes...

[Eric Wieser]

I think Adam's point is that you might do better to ask each question as a separate thread if you suspect they are unrelated

[Holly Liu]

oh, i will do that

[Adam Topaz]

Before going on to working with braid groups via their presentation, it might be worthwhile to try to fill in some of the following sorry's (or at least try to understand mathematically why they should be true):

import data.zmod.basic
import group_theory.presented_group

example : free_group punit ≃* multiplicative ℤ := sorry

def Z2_rels : set (free_group bool) :=
  { free_group.of tt * free_group.of ff * (free_group.of tt)⁻¹ * (free_group.of ff)⁻¹ }

example : presented_group Z2_rels ≃* multiplicative ( ℤ × ℤ ) := sorry

def Zn_rels (n : ℕ) : set (free_group punit) :=
  { (free_group.of punit.star)^n }

example {n} : presented_group (Zn_rels n) ≃* multiplicative ( zmod n ) := sorry

[Holly Liu]

thanks, that makes more sense

[Heather Macbeth]

Adam Topaz said:

example : free_group punit ≃* ℤ := sorry

example : free_group punit ≃* multiplicative ℤ := sorry

?

[Adam Topaz]

Oops!

[Adam Topaz]

Yes

[Adam Topaz]

Same for the other sorry's as well

[Adam Topaz]

Fixed! Thanks @Heather Macbeth !

[Holly Liu]

Adam Topaz said:

it might be worthwhile to try to fill in some of the following sorry's

example : free_group punit ≃* multiplicative ℤ := sorry

what is the ≃* notation and what is multiplicative ℤ ?

[Eric Wieser]

vscode will tell you what notation means if you hover over it

[Holly Liu]

is it \approx * ? nvm let me copy paste first

[Mario Carneiro]

it will also tell you how to write it

[Holly Liu]

import data.zmod.basic
import group_theory.presented_group

example : free_group punit ≃* multiplicative ℤ := sorry

if we are proving this isomorphism between the free group and the multiplicative ℤ, wouldn't the second set need an inverse property? i don't think it has one as we aren't able to use reciprocals in ℤ.

[Yakov Pechersky]

"multiplicative int" means consider the additive group on int, but labeling the unit as 1, the group operation as *, and the inverse as ^-1

[Holly Liu]

ohh ok

[Holly Liu]

where is punit defined btw? i found punit.lean but it calls punit from somewhere else.

[Adam Topaz]

src#punit

[Holly Liu]

inductive punit : Sort u
| star : punit

/-- An abbreviation for `punit.{0}`, its most common instantiation.
    This type should be preferred over `punit` where possible to avoid
    unnecessary universe parameters. -/
abbreviation unit : Type := punit

@[pattern] abbreviation unit.star : unit := punit.star

i'm not really understanding what this type is for or why it only has the element star. does this have something to do with category theory

[Adam Topaz]

punit is a type with a single term called punit.star

[Adam Topaz]

So the mathematical meaning of the isomorphism you're trying to construct is that the integers (as an additive group) is isomorphic to the free group generated by a set with a single element.

[Kevin Buzzard]

If you don't understand yhe definition of punit then before you go much further you should probably read the chapters on inductive types in #tpil , it provides a good introduction to basic dependent type theory notions such as inductive types.

[Holly Liu]

could i get a hint on how to unpack the mul_equiv (≃*)? i don't think i encountered this in the natural numbers game though i got through about 70% of it.

[Thomas Browning]

A mul_equiv consists of a function that satisfies some properties. If you want to construct it manually, then you can write something like

def my_def : free_group punit ≃* multiplicative ℤ :=
{ to_fun := sorry }

and then vscode should tell you what axioms you need to prove.

[Thomas Browning]

In practice, you're probably better off using some lemma about how a bijective monoid_hom is a mul_equiv

[Thomas Browning]

docs#mul_equiv.of_bijective

[Holly Liu]

i am still trying to understand how to use the lemmas in that file to show that a bijective monoid homomorphism is a mul_equiv in order to prove example : free_group punit ≃* multiplicative ℤ := . i'm confused about the notation here:

/-- The identity map is a multiplicative isomorphism. -/
@[refl, to_additive "The identity map is an additive isomorphism."]
def refl (M : Type*) [has_mul M] : M ≃* M :=
{ map_mul' := λ _ _, rfl,
..equiv.refl _}

what is the ' and the ..equiv.refl?

[Alex J. Best]

The ' is just part of the name of the field, so its not so important, why its there is a good question though but I think it can be safely ignored :smile:.
For the .. see https://leanprover.github.io/theorem_proving_in_lean/structures_and_records.html#objects where it talks about "record update".

[Johan Commelin]

@Holly Liu If you want to know more about the ', compare the output of

#print mul_equiv.map_mul'
-- vs
#print mul_equiv.map_mul

[Alex J. Best]

In this example we can see what happens if we delete it:

import data.equiv.mul_add
/-- The identity map is a multiplicative isomorphism. -/
def refl (M : Type*) [has_mul M] : M ≃* M :=
{ map_mul' := λ _ _, rfl}

we get the errors:

4:0: error:
invalid structure value { ... }, field 'to_fun' was not provided
4:0: error:
invalid structure value { ... }, field 'inv_fun' was not provided
4:0: error:
invalid structure value { ... }, field 'left_inv' was not provided
4:0: error:
invalid structure value { ... }, field 'right_inv' was not provided

so the .. is filling in the values of all these fields using the values from docs#equiv.refl.

[Holly Liu]

ok, thanks!

[Holly Liu]

where is map_mul defined?

[Holly Liu]

tried searching mathlib but couldn't find it

[Holly Liu]

nvm, i found it oops

[Holly Liu]

in the exercises that were given to me (which are very neat btw), could you explain the

def Z2_rels : set (free_group bool) := { free_group.of tt * free_group.of ff * (free_group.of tt)⁻¹
* (free_group.of ff)⁻¹ }

? i think i understand that these are supposed to be relations but i'm confused on what part of it is the relation, e.g. is it saying something like free_group.of tt, free_group.of ff, (free_group.of tt)⁻¹, and (free_group.of ff)⁻¹ are elements of the same equivalence class?

[Kevin Buzzard]

free_group.of is the natural map from a type S to the free group on S

[Alex J. Best]

Nothing specifically marks this as a relation (there is no specific type for relations in groups that is). Relations are some elements of a (free) group, that are meant to equal one in the group being presented (in the sense of https://en.wikipedia.org/wiki/Presentation_of_a_group). So this is a set of distinct elements all of which we will want to quotient the free group by. So this is saying we want the product `free_group.of tt * free_group.of ff * (free_group.of tt)⁻¹

• (free_group.of ff)⁻¹ to equal one when we make the quotient, though that happens at a later step. This will be a group where free_group.of tt and free_group.of ff` commute.

[Holly Liu]

oh i see. so we are saying that free_group.of tt * free_group.of ff * (free_group.of tt)⁻¹ * (free_group.of ff)⁻¹ = free_group.of ff * free_group.of tt * (free_group.of tt)⁻¹ * (free_group.of ff)⁻¹ = 1 ?

[Holly Liu]

so if we quotient the free group by this set, we are saying it is the smallest normal subgroup of the free group which contains the relation? so the subgroup only contains one element which is the relation itself?

[Holly Liu]

or wait, do you mean we are quotienting the free group by each free_group.ofterm?

[Alex J. Best]

Yeah you want to quotient by the smallest normal subgroup containing the relation indeed. But i guess that happens at a later step in the code?

[Holly Liu]

hm the next part of the code is

example : presented_group Z2_rels ≃* multiplicative ( ℤ × ℤ ) := sorry

and Z2_rels is not used again. i guess the presented_group Z2_rels part is quotienting the set?

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

[Holly Liu]

Kyle Miller said:

A single application of the reduction relation is represented by the following inductive type:

/-- Reduction step: `w * x * x⁻¹ * v ~> w * v` -/
inductive red.step : list (α × bool) → list (α × bool) → Prop
| bnot {L₁ L₂ x b} : red.step (L₁ ++ (x, b) :: (x, bnot b) :: L₂) (L₁ ++ L₂)

If you squint hard enough, you might see the resemblance.

Then, the free group with generators from the type α is given by the type quot red.step α (this is the definition of free_group). This creates a quotient type, where terms of quot red.step α correspond to equivalence classes under the equivalence relation generated by red.step.

this was from a while ago, but i was wondering if quot red.step α is both a quotient and a free group?

[Ayush Agrawal]

Hi Guys! I have recently started exploring Lean and group theory at the same time. Can anyone recommend some resource where I can find some simple example proofs related to Group theory. Any advice would be helpful!

[Kevin Buzzard]

If you scroll up you'll see several other people asking the same question :-)

I ran a workshop on groups and subgroups -- notes are here. https://xenaproject.wordpress.com/2021/01/28/formalising-mathematics-workshop-2/ It might make sense to do workshop 1 first though...

[Ayush Agrawal]

Thanks @Kevin Buzzard I'll go through this thread and thanks for sharing the resource!!