polynomial ring homs

Stream: maths

[Johan Commelin]

@Scott Morrison you mentioned on a PR page that there are good reasons to not bundle up all the mv_polynomial.{eval,map,rename,*} into ring homs directly. Can you please tell me what those reasons are?

[Scott Morrison]

The problem is just that for some of these to even be ring homs requires commutativity assumptions (typically on the "target"), yet we sometimes want to use the maps when the targets are not commutative.

[Scott Morrison]

A concrete example is that to prove Cayley-Hamilton we use the evaluation map for polynomials with matrix coefficients, which is not a ring hom.

[Scott Morrison]

We could just have two names, e.g. eval_noncomm (which might be a bundled add_monoid_hom) and eval (as a ring hom).

[Johan Commelin]

Ok, that makes total sense. Thanks.