free_group is a quotient

Stream: new members

[Holly Liu]

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]

src#free_group certainly confirms that free_group is implemented as a quotient. What meaning are you ascribing to "is a quotient"?

[Holly Liu]

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]

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

[Adam Topaz]

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]

In mathlib, we use bool instead of $\{\pm 1\}$ just for convenience.

[Holly Liu]

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

[Kevin Buzzard]

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]

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.