Polynomial.map ZeroHom

Stream: mathlib4

[Bolton Bailey]

Watching over my video from last week, I remebered a question I had. Is there a reason docs#Polynomial.map takes a RingHom rather than a ZeroHom?

[Bolton Bailey]

(I guess I can't think of an application)

[David Ang]

Mapping the derivative linear map across a polynomial ring over a polynomial ring can’t be done currently :/

[David Ang]

I think it's even possible to let it take in a regular function? I tried refactoring it about a year ago and it was slightly fiddly, so I gave up.

[Eric Wieser]

Note that docs#DFinsupp.mapRange and docs#Finsupp.mapRange both take unbundled zero_homs

[Eric Wieser]

Most of the polynomial API is unfortunately built from scratch instead of saying "oh, we already defined this for finsupp let's just reuse it"

[Notification Bot]

This topic was moved here from #general > Polynomial.map ZeroHom by Kyle Miller.