Zulip Chat Archive

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?

Patrick Massot (Aug 31 2020 at 10:04):

docs#monoid_hom?

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.

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

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

Kenny Lau (Aug 31 2020 at 10:08):

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

Scott Morrison (Oct 03 2020 at 10:45):

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: Dec 20 2023 at 11:08 UTC