[Merged by Bors] - feat(group_theory/free_product): equivalence with reduced words

[dwarn]

We show that each element of the free product is represented by a unique reduced word.

---

• depends on: [Merged by Bors] - feat(group_theory/group_action): a monoid action determines a monoid hom #8253
• depends on: [Merged by Bors] - feat(algebra/opposites): functoriality of the opposite monoid #8254
• depends on: [Merged by Bors] - feat(group_theory/free_product): the free product of an indexed family of monoids #8256

[dwarn]

I marked this RFC because there are a couple open design questions. Most importantly: should we have a canonical definition of the coproduct, and if so what should it be? There is already a nice "automated" construction in algebra.category.Mon.colimits. The construction there is diametrically opposite to the one here. This one is sort of "maximally efficient": we only ever consider expressions in normal form, there is no need to quotient, we needed to know beforehand what the normal forms should be (so this doesn't work for say general pushouts, where there is no normal form), we need some decidability assumptions to compute in the coproduct, and we can easily tell when two elements of the coproduct are distinct. The construction in algebra.category.Mon.colimits is maximally inefficient: you start with all sorts of syntactic expressions then quotient to get rid of redundancy, you don't need to know anything about monoids beforehand, the construction is the same for any colimit, and there is no way to prove that two elements of the coproduct are distinct other than showing they map to distinct things in some other monoid. For better or worse, you get the universal property and nothing else. A third, sort of intermediate, construction would be to quotient a certain list monoid, analogously to the current construction of free groups.

If we don't define the coproduct as reduced words, we can still use the material in this PR to prove that the coproduct doesn't make too many identifications -- you just need to let the coproduct act on the reduced words. If we do define the coproduct as reduced words, there is still the question of decidability assumptions. It doesn't seem ideal to have multiplication depend on decidability instances. Should we use classical instances throughout?

I should say that constructively, the approach in this PR is not as satisfying as the current construction of free groups. By working with unreduced words, then quotienting and proving confluence, you get constructive proofs of various injectivity statements, even without decidability assumptions. However Lean can't tell the difference between constructive and non-constructive proofs of injectivity. The upshot of the approach in this PR is that it's considerably simpler than dealing with confluence.

[dwarn]

I noticed that there's an old WIP PR #2578 by @urkud which does the same thing as this one, but with a different approach. I also cleaned this one up a bit.

[semorrison]

Sorry, I'm not going to have a chance to look at this soon; limited Lean time. One request would just be that David's explanation above about the relationship with algebra.category.Mon.colimits goes into doc-strings somewhere! It's very helpful.

[dwarn]

After thinking a bit about this, I would slightly prefer to change the setup here, starting from some quotient definition of the free product as in #2578, and then proving that it's equiv with reduced words. Currently I jump through some hoops to give free_product its monoid structure and universal property without too much duplication. I think starting from another free product, and proving that it's equiv with reduced words, would make the argument more focused. There wouldn't be too much work involved in this change, but I won't have time for it anytime soon.

[sgouezel]

ok, seems reasonable. Let me mark this as WIP then.

[ChrisHughes24]

The only comment I have on this is that it's often not a good idea to define a new type only to prove it's isomorphic to another type. My feeling is that either word should either be the definition of the coproduct or all the structure that is currently on word should be put directly on the coproduct. So my feeling is that the type word shouldn't be part of the API, the API should be a map from coproduct to lists with a proof that the result is reduced etc., and the map from lists to coproduct etc, as well as an induction principle and stuff like that, all defined directly on the coproduct.

[dwarn]

@ChrisHughes24 this sounds reasonable -- the API should mainly expose one of free_product and word, and probably it should be free_product (word is not always so nice because you need decidable instances, and putting a monoid structure on word directly gets a little confusing). In this perspective, word is there only to give things like decidable equality to the free_product.

I haven't thought much about creating an API in this PR. But it should be straightforward to build an API on top of this, proving things like decidable equality in free_product. Lemmas about word that are in this PR might not be too useful outside of proving the equivalence with free_product, so I'm not sure they should be transferred to free_product.

[jcommelin]

I think it would be good to see more API before merging this. @dwarn Do you think you can add some?

[dwarn]

I added some decidable equality instances and reorganized the code to be more user friendly.

I'm not sure what else to add. Maybe an analogue of equiv_pair for free_product instead of just word (you need something similar to this to prove that free_group (fin 2) is not amenable / Banach-Tarski), but maybe this is better left for another PR.

[sgouezel]

LGTM, thanks!

[sgouezel]

bors r+
Thanks!

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Build failed:

• Build mathlib

[sgouezel]

Can you merge master and fix the build?
bors r-

[ChrisHughes24]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests