# Zulip Chat Archive

## Stream: new members

### Topic: free_group is a quotient

#### Holly Liu (Jul 31 2021 at 22:52):

i was wondering whether `free_group α`

is both a free group and a quotient? it's defined as a free group but it is also a quotient over the relation `free_group.red.step`

:`w * x * x⁻¹ * v ~> w * v`

.

#### Eric Wieser (Jul 31 2021 at 22:55):

src#free_group certainly confirms that `free_group`

is *implemented* as a quotient. What meaning are you ascribing to "*is* a quotient"?

#### Holly Liu (Jul 31 2021 at 23:21):

i was under the assumption that implementing it as a quotient is the same as defining it as a quotient group. so `free_group α`

is a set containing cosets that divide the group... now i'm confused about what group is being divided. but if it is like this, then i think it's not a free group anymore since its elements are the cosets, not words.

#### Adam Topaz (Jul 31 2021 at 23:31):

The quotient in this implementation is a quotient of types, not a quotient of groups.

#### Adam Topaz (Jul 31 2021 at 23:35):

What's going on in this definition is this: Let $S$ be a set, and consider the collection $\mathcal{L}$ of lists whose terms all come from, say, $S \times \{\pm 1\}$. Take the quotient of this *set* by the coarsest equivalence relation for which $L_1 + [(x,1)] + [(x,-1)] + L_2$ and $L_1 + [(x,-1)] + [(x,1)] + L_2$ are both related to $L_1 + L_2$ (here $L_i$ are arbitrary lists and $[ t]$ is the singleton list). This is the *set* on which you can define a group structure which yields the free group.

#### Adam Topaz (Jul 31 2021 at 23:36):

In mathlib, we use `bool`

instead of $\{\pm 1\}$ just for convenience.

#### Holly Liu (Jul 31 2021 at 23:40):

ohh i see. thank you!! i didn't realize there was a quotient of types.

#### Kevin Buzzard (Aug 01 2021 at 10:50):

Your question indicates that you might be thinking about these things in the wrong way. *It does not matter* what the definition of a free group is in Lean. What matters is that for any construction you want to do with or theorem you want to apply to free groups, eg given a map from X to Y then there's an induced group homomorphism from the free group on X to the free group on Y, there will be a definition or theorem for this in Lean. The free group is a group and there will be a construction for this in lean. If you're reading mathlib about free groups then you should *not* read the definition (indeed even mathlib's definition of a *group* is incomprehensible!). You should read the statements of the theorems proved just after the definition. They are your API. Mathlib's free groups are not quotient groups or equivalence classes or sets or anything you've ever heard of, but this should not matter to do if all you want to do is use them.

#### Holly Liu (Aug 03 2021 at 22:36):

ok that's understandable. i was trying to read the definitions so i could understand why relations can be formulated as `set (free_group ℕ)`

(which i think i may post as a separate thread). however i'll try to focus my attention on theorems, as you said.

Last updated: Dec 20 2023 at 11:08 UTC