Restriction of `monoid_hom` to units?

Stream: Is there code for X?

[Michael Stoll]

There is docs#monoid_hom.to_hom_units, which, given a monoid_hom from a group G to M gives a monoid_hom from G to the units of M.
Do we also have a conversion from a monoid_hom between two monoids to a monoid_hom between there unit groups?

[Riccardo Brasca]

This is docs#units.map

[Michael Stoll]

Thanks! Is there also a way to extend a homomorphism between the unit groups to a homomorphism between the monoids by extending by zero (when the target is a monoid_with_zero, otherwise it does not make sense).

[Riccardo Brasca]

I think you have to do this by hand, using docs#function.extend

[Eric Wieser]

Something like docs#with_zero.lift?

[Eric Wieser]

Hmm, I assume we have the monoid_with_zero version of that somewhere

[Eric Rodriguez]

Michael Stoll said:

Thanks! Is there also a way to extend a homomorphism between the unit groups to a homomorphism between the monoids by extending by zero (when the target is a monoid_with_zero, otherwise it does not make sense).

As in all of the other results get sent to zero?

[Michael Stoll]

Yes.