when is multiplication a monoid homomorphism?

Stream: maths

[Ben Selfridge]

I'm not a super-duper expert in math or category theory; I'm probably at about the level of a first- or second-year graduate student in mathematics, and i'm a novice in category theory.

However, it just occurred to me that the monoid multiplication function $G \times G \to G $ is a monoid homomorphism if and only if G is abelian. That really surprised me -- intuitively I kind of assumed multiplication would obviously itself be a homomorphism!

Can anyone with more expertise confirm this for me, and perhaps elaborate if there's anything to elaborate on?

[Michał Mrugała]

Yes this is certainly true! This shows up in a lot of contexts with <algebraic structure> objects: a monoid object in the category of monoids is a commutative monoid, a group object in the category of groups is an abelian group, etc.

[Yury G. Kudryashov]

E.g., docs#MonoidHom.mul requires commutativity of the codomain.

[Yury G. Kudryashov]

This is exactly what you're talking about: docs#mulMonoidHom

[Ben Selfridge]

Thank you both.

[Bhavik Mehta]

This is a nice instance of the https://en.m.wikipedia.org/wiki/Eckmann%E2%80%93Hilton_argument

[Eric Wieser]

Which is present in mathlib too, right?

[Yury G. Kudryashov]

docs#EckmannHilton.commMonoid