generalizing Abelianization to `Semigroup`/ any `Mul`

Stream: mathlib4

[Edward van de Meent]

Right now, in mathlib, docs#Abelianization is defined only for Groups, and definitionally equal to the group quotient by the commutator subgroup. For my personal project i need some free constructions like the free commutative monoid on a type, which could make use of a generalization of this concept, allowing us to define FreeCommMonoid A := Abelianization (FreeMonoid A) and similar.

However, since the "normal subgroup trick" for creating quotients only works on groups, generalizing this concept does require changing the definition to going through the more general docs#Con. Is this a desirable refactor?

[Aaron Liu]

You can define FreeCommMonoid A := Multiset A, though I do agree it would be desirable to generalize Abelianization

[Edward van de Meent]

i don't know that there is proper API for 1 and multiplication on Multiset though...

[Edward van de Meent]

aamof, i suspect there isn't

[Aaron Liu]

docs#Multiset.prod is your evaluation map.

[Aaron Liu]

Multiset has the additive 0 and +

[Edward van de Meent]

@loogle AddMonoid (Multiset ?A)

[loogle]

:shrug: nothing found

[Aaron Liu]

@loogle AddComnMonoid (Multiset _)

[loogle]

:exclamation: unknown identifier 'AddComnMonoid'

[Aaron Liu]

@loogle AddCommMonoid (Multiset _)

[loogle]

:shrug: nothing found

[Aaron Liu]

Found it: docs#Multiset.instAddCancelCommMonoid

[Edward van de Meent]

anywho, the precise construction of FreeCommMonoid is really a different question