I am not very familiar with the mathematics, can you explain a little bit what is the point of the main theorem?

I am not very familiar with the mathematics, can you explain a little bit what is the point of the main theorem?

There's a normal form (and reduced form) for words in the amalgamated product. The main application of this is that it implies the injectivity of the maps into the amalgamated product and the theorem inf_of_range_eq_base_range.

Other than that, I don't directly know any applications, but the similar result about reduced forms for HNNExtensions is used to prove things like the decision procedure for groups presented by a single relation.

So I suppose it's useful to know this reduced form theorem, because then you know a lot about which words are equal to each other, and which words are in the base subgroup and things like this, but I couldn't say anything more concrete.

The maths look great, I would just be happy to see more documentation (featuring prominently the word "amalgamated product" here and there, because it's the name I know for these objects, not the categorical ones pushouts or coproducts, but I realize it's a question of personal taste or personal culture -- but it would be good to make sure that anyone with any culture can find this with a good old grep).

I chose the word pushout, because as far as I know, the phrase amalgamated product only refers to the case when all maps in the diagram are injective. This is basically the interesting case, but the construction works the rest of the time.

bors r+
Thanks!

Pull request successfully merged into master.

Build succeeded:

• Check all files imported
• Lint style
• Build