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 SS be a set, and consider the collection L\mathcal{L} of lists whose terms all come from, say, S×{±1}S \times \{\pm 1\}. Take the quotient of this set by the coarsest equivalence relation for which L1+[(x,1)]+[(x,1)]+L2L_1 + [(x,1)] + [(x,-1)] + L_2 and L1+[(x,1)]+[(x,1)]+L2L_1 + [(x,-1)] + [(x,1)] + L_2 are both related to L1+L2L_1 + L_2 (here LiL_i are arbitrary lists and [t][ 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 {±1}\{\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