Zulip Chat Archive
Stream: new members
Topic: Group theory
Sai Gopal (Jun 25 2021 at 06:44):
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 (Jun 25 2021 at 06:45):
import topology.basic
means: grab everything that's in src/topology/basic.lean
and import it into the environment.
Johan Commelin (Jun 25 2021 at 06:46):
So now import group_theory.<some_nice_file>
that you find by browsing mathlib
Sai Gopal (Jun 25 2021 at 06:48):
instead of .<>
Can you tell me which file has all basics of GT ?
Johan Commelin (Jun 25 2021 at 06:49):
You should rather be precise about what you want to do.
Johan Commelin (Jun 25 2021 at 06:50):
What is the exact maths statement that you want to formalize in Lean?
Johan Commelin (Jun 25 2021 at 06:50):
There is also the directory src/algebra/group/
which contains a lot of lowlevel stuff: https://github.com/leanprovercommunity/mathlib/tree/master/src/algebra/group
Sai Gopal (Jun 25 2021 at 06:53):
So How do I include this ?
Kevin Buzzard (Jun 26 2021 at 10:37):
Import the name of the file
Holly Liu (Jun 28 2021 at 21:29):
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 (Jun 28 2021 at 21:39):
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 (Jun 28 2021 at 21:44):
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 (Jun 28 2021 at 21:45):
It's maybe not what you want, but we have docs#is_free_group
Eric Wieser (Jun 28 2021 at 21:46):
As well as docs#free_group
Holly Liu (Jun 28 2021 at 22:33):
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 (Jun 28 2021 at 22:35):
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 (Jun 28 2021 at 22:39):
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 (Jun 28 2021 at 22:39):
Which says that the group of integers is a free group on a single element.
Eric Wieser (Jun 28 2021 at 22:48):
And then you could PR it to mathlib :)
Holly Liu (Jul 04 2021 at 20:22):
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⟩
Eric Wieser (Jul 04 2021 at 20:29):
instance : has_one _
is specifying what 1
means in that example. Is that your question?
Holly Liu (Jul 05 2021 at 23:43):
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 (Jul 05 2021 at 23:43):
thanks again.
Kyle Miller (Jul 06 2021 at 01:39):
@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 lefttoright 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 (Jul 06 2021 at 16:33):
@Kyle Miller thanks for the very thorough explanation.
Holly Liu (Jul 06 2021 at 20:38):
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 (Jul 06 2021 at 20:42):
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#implicitarguments
Holly Liu (Jul 06 2021 at 20:43):
ah i see.
Malvin Gattinger (Jul 06 2021 at 20:45):
Ah, so $ does the same as in Haskell, nice to know.
Kyle Miller (Jul 06 2021 at 20:46):
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 (Jul 06 2021 at 20:52):
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 (Jul 06 2021 at 20:55):
Ah, thanks. The ( ) notation to turn infix into prefix works just for $ or in general with all infix notations?
Eric Wieser (Jul 06 2021 at 21:42):
It works on all infix notation
Eric Wieser (Jul 06 2021 at 21:43):
We also have (+ 1)
which expands to λ x, x + 1
for all infix operators
Eric Wieser (Jul 06 2021 at 21:44):
So I guess ($ x)
is docs#function.eval x
Holly Liu (Jul 06 2021 at 22:21):
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 read the doc and i think i understand.@
, 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)
.
Eric Rodriguez (Jul 06 2021 at 22:27):
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 (Jul 06 2021 at 22:33):
oh I see this was mentioned above
Eric Wieser (Jul 06 2021 at 22:34):
I think by infix
I mean "anything that unfolds to the same type of notation command as infix
"
Eric Wieser (Jul 06 2021 at 22:35):
#print notation
doesn't show anything but notation
; the other keywords seem to just be shorthands
Kyle Miller (Jul 06 2021 at 23:07):
@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 (Jul 06 2021 at 23:30):
ok i think that makes sense. thanks a lot! that was really clear and easy to understand.
Holly Liu (Jul 10 2021 at 01:01):
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 (Jul 10 2021 at 04:40):
{G : Type*} [group G] [fintype G]
?
Eric Wieser (Jul 10 2021 at 04:41):
fintype.card G
is then the number of elements
Kyle Miller (Jul 10 2021 at 05:49):
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 (Jul 10 2021 at 18:51):
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 (Jul 10 2021 at 18:52):
Can you post a link to the maths definition you're trying to formalise?
Holly Liu (Jul 10 2021 at 18:53):
i'm not sure if braid groups are formalized yet? i think i'm mostly using free groups: https://github.com/leanprovercommunity/mathlib/blob/49bf1fdecf56ce9ae3e6d15953896996af596c07/src/group_theory/free_group.lean#L385
Holly Liu (Jul 10 2021 at 18:59):
oh wait was this what you meant? https://en.wikipedia.org/wiki/Braid_group
Kevin Buzzard (Jul 10 2021 at 18:59):
Oh we're talking about braid groups? Why not just formalise them as the presentation on that Wikipedia page?
Holly Liu (Jul 10 2021 at 19:06):
do you mean like when its saying 'the group whose elements are equivalence classes of nbraids (e.g. under ambient isotopy), and whose group operation is composition of braids'? or is there code somewhere i'm not seeing?
Kevin Buzzard (Jul 10 2021 at 19:12):
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_{n1}$ 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 n2$ and $\sigma_i\sigma_j=\sigma_j\sigma_i$ for $1\leq i\leq j2\leq n3$. That wouldn't be too hard to put into Lean.
David Wärn (Jul 10 2021 at 19:13):
There is docs#presented_group
Holly Liu (Jul 10 2021 at 19:21):
ah ok, i'll try that. i don't fully understand what all those words mean together yet...
Holly Liu (Jul 10 2021 at 19:25):
oh so would we just construct a specific quotient of the free group that contains only those two equivalence classes?
Kevin Buzzard (Jul 10 2021 at 20:09):
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 (Jul 10 2021 at 20:55):
hm alright, i'll read up on that.
Kevin Buzzard (Jul 10 2021 at 21:47):
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 (Jul 21 2021 at 21:58):
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:

why do
set
and equivalence relations map to aProp
in their definitions:def set (α : Type u) := α → Prop
andconstant quot : Π {α : Sort u}, (α → α → Prop) → Sort u
wherer : (α → α → Prop)
? 
for universe
u
,#check Sort u
evaluatesSort u
as having typeType u
, however the documentation says types are really justSort
s, i.e.Prop
abbreviatesSort 0
,Type
abbreviatesSort 1
, andType u
abbreviatesSort (u+1)
. is the point ofSort
just to have an umbrella set that includes bothProp
andType
?  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 (Jul 21 2021 at 22:04):
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 (Jul 21 2021 at 22:06):
Adam Topaz said:
have at least three unrelated questions here...
yeah i keep going down these rabbit holes...
Eric Wieser (Jul 21 2021 at 22:08):
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 (Jul 21 2021 at 22:09):
oh, i will do that
Adam Topaz (Jul 21 2021 at 22:14):
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 (Jul 21 2021 at 22:22):
thanks, that makes more sense
Heather Macbeth (Jul 21 2021 at 22:23):
Adam Topaz said:
example : free_group punit ≃* ℤ := sorry
example : free_group punit ≃* multiplicative ℤ := sorry
?
Adam Topaz (Jul 21 2021 at 22:25):
Oops!
Adam Topaz (Jul 21 2021 at 22:25):
Yes
Adam Topaz (Jul 21 2021 at 22:25):
Same for the other sorry's as well
Adam Topaz (Jul 21 2021 at 22:27):
Fixed! Thanks @Heather Macbeth !
Holly Liu (Jul 22 2021 at 19:43):
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 (Jul 22 2021 at 19:47):
vscode will tell you what notation means if you hover over it
Holly Liu (Jul 22 2021 at 19:48):
is it nvm let me copy paste first\approx *
?
Mario Carneiro (Jul 22 2021 at 19:49):
it will also tell you how to write it
Holly Liu (Jul 23 2021 at 23:43):
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 (Jul 23 2021 at 23:58):
"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 (Jul 24 2021 at 00:10):
ohh ok
Holly Liu (Jul 24 2021 at 00:15):
where is punit
defined btw? i found punit.lean but it calls punit from somewhere else.
Adam Topaz (Jul 24 2021 at 00:15):
Holly Liu (Jul 24 2021 at 00:26):
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 (Jul 24 2021 at 00:30):
punit
is a type with a single term called punit.star
Adam Topaz (Jul 24 2021 at 00:32):
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 (Jul 24 2021 at 00:32):
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 (Jul 24 2021 at 01:51):
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 (Jul 24 2021 at 03:26):
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 (Jul 24 2021 at 03:27):
In practice, you're probably better off using some lemma about how a bijective monoid_hom is a mul_equiv
Thomas Browning (Jul 24 2021 at 03:28):
Holly Liu (Jul 26 2021 at 17:31):
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 (Jul 26 2021 at 17:34):
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 (Jul 26 2021 at 17:39):
@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 (Jul 26 2021 at 17:39):
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 (Jul 26 2021 at 19:24):
ok, thanks!
Holly Liu (Jul 27 2021 at 01:41):
where is map_mul
defined?
Holly Liu (Jul 27 2021 at 01:42):
tried searching mathlib but couldn't find it
Holly Liu (Jul 27 2021 at 01:44):
nvm, i found it oops
Holly Liu (Jul 28 2021 at 05:57):
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 (Jul 28 2021 at 06:15):
free_group.of
is the natural map from a type S to the free group on S
Alex J. Best (Jul 28 2021 at 11:15):
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 ttand
free_group.of ff` commute.
Holly Liu (Jul 28 2021 at 22:41):
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 (Jul 28 2021 at 22:43):
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 (Jul 28 2021 at 22:45):
or wait, do you mean we are quotienting the free group by each free_group.of
term?
Alex J. Best (Jul 28 2021 at 23:24):
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 (Jul 29 2021 at 02:39):
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 (Jul 29 2021 at 02:55):
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 typequot red.step α
(this is the definition offree_group
). This creates a quotient type, where terms ofquot red.step α
correspond to equivalence classes under the equivalence relation generated byred.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 (Oct 04 2021 at 14:02):
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 (Oct 04 2021 at 14:03):
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/formalisingmathematicsworkshop2/ It might make sense to do workshop 1 first though...
Ayush Agrawal (Oct 04 2021 at 14:05):
Thanks @Kevin Buzzard I'll go through this thread and thanks for sharing the resource!!
Last updated: Dec 20 2023 at 11:08 UTC