MonoidHom.quotient_ker_equiv_range

Stream: Is there code for X?

[Violeta Hernández]

We have a bunch of versions of the first isomorphism theorem, but is there one for docs#MonoidHom.ker ?

[Antoine Chambert-Loir]

Probably not because this is more subtle: the quotient has to be taken by the equivalence relation which is generated by $f(x)=f(y)$.

[Kevin Buzzard]

Yes, the kernel isn't enough information to determine the image for monoids (for example if you give Fin n the monoid structure it should have, which is x+y=n-1 if in reality it's >= n-1) then the obvious map from Nat is surjective with trivial kernel.

[Adam Topaz]

We do have docs#Con

[Adam Topaz]

These are setoids which are "compatible with multiplication".

[Adam Topaz]

import Mathlib

example {α : Type*} [Monoid α] (S : Con α) : Monoid S.Quotient := inferInstance

[Adam Topaz]

That's essentially the only way to talk about quotients of monoids. You can take whatever relation you like and look at the congruence relation generated by it with docs#conGen and only then take the quotient.

[Antoine Chambert-Loir]

My earlier claim is that for good structures which have subtraction, the compatible equivalence relation generated by $f(x)=f(y)$ is determined by the class of the adequate zero/one element. But quotient_rel_equiv_range would work as well.
The analogue for semirings is missing too.

[Violeta Hernández]

I should specify that I am in fact working with groups

[Violeta Hernández]

But to my understanding MonoidHom is still the structure to be used

[Violeta Hernández]

Is there some theorem like Con.ker = MomoidHom.ker?

[Adam Topaz]

Oh, for groups everything works as you expect. You probably want to take a look around QuotientAddGroup.quotientKerEquivOfRightInverse

[Eric Wieser]

Violeta Hernández said:

We have a bunch of versions of the first isomorphism theorem, but is there one for docs#MonoidHom.ker ?

I'm confused, isn't docs#QuotientGroup.quotientKerEquivRange precisely what you're asking for?

[Eric Wieser]

Or did you mean to ask about docs#MonoidHom.mker, which seems to be what everyone is assuming you meant?

[Violeta Hernández]

Eric Wieser said:

Violeta Hernández said:

We have a bunch of versions of the first isomorphism theorem, but is there one for docs#MonoidHom.ker ?

I'm confused, isn't docs#QuotientGroup.quotientKerEquivRange precisely what you're asking for?

Ah, I think that's it

[Violeta Hernández]

That's quite an annoying naming discrepancy, I was finding all the versions of this theorem except for this one

[David Ang]

I think that's because the isomorphism theorems for groups were the first ones written, back when there were no naming convention for these things? I found it annoying too, and it would be great if someone makes them consistent.