Semigroup morphisms

Stream: Is there code for X?

[Nicolò Cavalleri]

We do not have semigroup morphisms in mathlib, right?

[Patrick Massot]

docs#monoid_hom?

[Kenny Lau]

yeah unfortunately we don't have them for semigroups

[Nicolò Cavalleri]

This is for monoids only it seems

[Patrick Massot]

Oh yes, this is not general enough.

[Patrick Massot]

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

[Patrick Massot]

docs#is_mul_hom

[Patrick Massot]

Even more general than semigroup.

[Nicolò Cavalleri]

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

[Kenny Lau]

what results?

[Nicolò Cavalleri]

Some sufficient conditions for multiplication to be continuous in topological monoids

[Kevin Buzzard]

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]

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

[Nicolò Cavalleri]

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]

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]

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]

Do you need much more than this?

[Eric Wieser]

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.*?

[Scott Morrison]

Worth a shot!

[Johan Commelin]

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]

I've attempted to do this in #4423

[Eric Wieser]

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