Should we allow `algebra_map R A` for noncommutative `R`?

Stream: general

[Eric Wieser]

In #8516, I tried to remove docs#matrix.scalar because I thought it was the same as algebra_map R (matrix n n R). What I realize now is that that algebra_map only exists when R is commutative, due to the typeclass requirements of algebra.

Should we extract a has_algebra_map R A typeclass from algebra R A which is just docs#algebra without the commutes' field or requirement that R be commutative (aka a canonical ring hom and a proof it's compatible with smul? This feels like it would come up for polynomials over non-commutative coefficients too.

[Anne Baanen]

I think a has_canonical_ring_hom R A typeclass will be a good idea, in fact I suspect we will want it for groups too.

[Eric Wieser]

I was just thinking that we probably want it for groups

[Eric Wieser]

Which I suspect opens a can of worms regarding definitional diamonds so I might just do the ring hom version