## Stream: Is there code for X?

### Topic: Semigroup morphisms

#### Nicolò Cavalleri (Aug 31 2020 at 10:00):

We do not have semigroup morphisms in mathlib, right?

#### Kenny Lau (Aug 31 2020 at 10:05):

yeah unfortunately we don't have them for semigroups

#### Nicolò Cavalleri (Aug 31 2020 at 10:05):

This is for monoids only it seems

#### Patrick Massot (Aug 31 2020 at 10:05):

Oh yes, this is not general enough.

#### Patrick Massot (Aug 31 2020 at 10:05):

But we used to have them unbundled, I'm sure.

docs#is_mul_hom

#### Patrick Massot (Aug 31 2020 at 10:06):

Even more general than semigroup.

#### Nicolò Cavalleri (Aug 31 2020 at 10:08):

Ok I do not plan to implement them but I'm proving results that are valid for them as well so I guess I'll just write some TODOs

what results?

#### Nicolò Cavalleri (Aug 31 2020 at 10:09):

Some sufficient conditions for multiplication to be continuous in topological monoids

#### Kevin Buzzard (Aug 31 2020 at 10:26):

I guess there would be no harm in writing a bundled mul_hom, but we already used the \to* notation for monoid homs. If it's just a few lemmas then perhaps one doesn't need notation at all?

#### Kevin Buzzard (Aug 31 2020 at 10:26):

PS isn't multiplication by definition continuous in a topological monoid?

#### Nicolò Cavalleri (Aug 31 2020 at 10:46):

Kevin Buzzard said:

PS isn't multiplication by definition continuous in a topological monoid?

Yeah sure haha I mean just one of the two monoids is a priori a topological monoid, I did not give a precise answer because my point was really about semigroups, so I thought people did not care too much about other details

#### Nicolò Cavalleri (Aug 31 2020 at 10:51):

Kevin Buzzard said:

I guess there would be no harm in writing a bundled mul_hom, but we already used the \to* notation for monoid homs. If it's just a few lemmas then perhaps one doesn't need notation at all?

Yeah I think there is no need for notation! I do not have a lot of time to write bundled mul_homs and generalize lemmas for them but if someone wants to do it I think that'd be cool

#### Kevin Buzzard (Aug 31 2020 at 11:07):

the usual API for these things is just id and comp, plus maybe the fact that if you have an equiv between has_muls such that one of the maps is mul_hom, then so is the other one.

#### Kevin Buzzard (Aug 31 2020 at 11:07):

Do you need much more than this?

#### Eric Wieser (Oct 03 2020 at 09:26):

Presumably the approach here would be to replace

structure monoid_hom (M : Type*) (N : Type*) [monoid M] [monoid N] :=
(to_fun : M → N)
(map_one' : to_fun 1 = 1)
(map_mul' : ∀ x y, to_fun (x * y) = to_fun x * to_fun y)


with

structure mul_hom (M : Type*) (N : Type*) [has_mul M] [has_mul N] :=
(to_fun : M → N)
(map_mul' : ∀ x y, to_fun (x * y) = to_fun x * to_fun y)

structure monoid_hom (M : Type*) (N : Type*) [monoid M] [monoid N] extends mul_hom M N :=
(map_one' : to_fun 1 = 1)


and move some of the monoid_hom.* lemmas to mul_hom.*?

Worth a shot!

#### Johan Commelin (Oct 03 2020 at 10:57):

I've tried replacing the monoid M and monoid N assumptions by has_mul M, has_one M and has_mul N, has_one N.... that refactor is a disaster. I gave up.

#### Eric Wieser (Oct 05 2020 at 09:31):

I've attempted to do this in #4423

#### Eric Wieser (Oct 05 2020 at 09:36):

It seems that homomorphisms are in dire need of some combination of metaprogramming or type classes

Last updated: May 17 2021 at 14:12 UTC