Polynomial maps

Stream: general

[David Ang]

Currently docs#polynomial.map takes in a ring_hom and returns an ordinary function, while docs#polynomial.map_ring_hom takes in a ring_hom and returns a ring_hom, but @Eric Wieser suggested that perhaps docs#polynomial.map should remain unbundled but takes in an ordinary function. Then docs#polynomial.map_ring_hom could remain the way it is, and maybe have things like polynomial.map_add_hom etc too. Everything would be similar for the family of docs#polynomial.eval maps as well. What do people think? The context is that I've been wanting to have a map across docs#polynomial.derivative to simulate partial derivatives in things like R[X][X], but currently docs#polynomial.map does not accept a linear_map so I had to unwrap into a finsupp and use docs#to_finsupp_iso to get back to polynomial.

[David Ang]

I would open a poll but I think the options are quite open ended so maybe a discussion would be better.

[Eric Wieser]

One argument in favor of this; it is already how the bundling is handled for the analogous docs#finsupp.map_domain (c.f. docs#finsupp.map_domain.add_monoid_hom).

[Kevin Buzzard]

Oh yes, polynomial.map is kind of ridiculous! Why ask for a ring hom if you're only going to return a function?