Zulip Chat Archive

Stream: Is there code for X?

Topic: Kernel of product morphism

Riccardo Brasca (May 27 2021 at 08:27):

Let $f \colon A \to A_1$ and $g\colon B \to B_1$ be morphisms of groups, monoids... whatever. Do we have something like that the kernel of $f \times g \colon A \times B \to A_1 \times B_1$ is (isomorphic to) $\ker f \times \ker g$ ? Thank's!

Johan Commelin (May 27 2021 at 08:32):

As subobjects they should be equal on the nose. But I don't think we have this in mathlib.

Johan Commelin (May 27 2021 at 08:33):

Do we have subgroup.product which takes the product of two subgroups and returns a subgroup of the product group?

Riccardo Brasca (May 27 2021 at 08:37):

We have docs#submonoid.prod , so I guess the other version are there too

Riccardo Brasca (May 27 2021 at 08:37):

But I didn't check

Eric Wieser (May 27 2021 at 08:37):

Do we even have a name for that product operation? It looks like docs#prod.map, but you want a monoid_hom version of it

Eric Wieser (May 27 2021 at 08:37):

It might be near docs#monoid_hom.fst

Eric Wieser (May 27 2021 at 08:38):

Ah, docs#monoid_hom.prod_map

Riccardo Brasca (May 27 2021 at 08:39):

Yes, the map is there. I will do the part about the kernel

Riccardo Brasca (May 27 2021 at 08:40):

And I agree that they should be equal, being subobjects...

Riccardo Brasca (May 27 2021 at 12:50):

#7729
Am I missing something or we cannot speak about the kernel of a monoid_hom? Note that docs#monoid_hom.ker is for groups.

Kevin Buzzard (May 27 2021 at 13:00):

Isn't there something like mker?

Kevin Buzzard (May 27 2021 at 13:01):

This is the problem with not having group_hom, and using monoid_hom to do group homomorphisms.

Riccardo Brasca (May 27 2021 at 13:04):

I don't see any way of producing the kernel of f : G →* N is G and N are only monoids. But to be honest I don't need it, I was just surprised by this.

Kevin Buzzard (May 27 2021 at 13:04):

Doesn't seem to be -- maybe the point is that the monoid hom kernel isn't very useful? (e.g. the image isn't cosets of the kernel etc)

Kevin Buzzard (May 27 2021 at 13:05):

The correct object to have for a monoid hom is the equivalence relation defined by $g\sim h\iff f(g)=f(h)$ . For groups, this equivalence relation is determined by the kernel, but for monoids it is not.

Eric Wieser (May 27 2021 at 13:08):

Same thing applies for ring_hom.sker (to match docs#ring_hom.srange) which also doesn't exist. I think it's a combination of it not being very useful and the fact that adding it would result in a huge amount of work duplicating all the definitions

Riccardo Brasca (May 27 2021 at 13:09):

I agree that it's not very useful :)

Last updated: Dec 20 2023 at 11:08 UTC