name of ring hom associated to function

Stream: maths

[Kevin Buzzard]

of_real is the function from $\mathbb{R}$ to $\mathbb{C}$. The bundled ring hom will hence have to be called something else. What should it be called? Of_real? Same question for complex.conj

[Johan Commelin]

We've been using the ugly _hom suffix, or a l, a, r prefix for "linear", "alg_hom", or "ring_hom".

[Johan Commelin]

I don't like any of these

[Johan Commelin]

Now that inferring arguments of bundled homs has been fixed (last week, thanks Gabriel :tada:), I think of_real should be the ring hom, and of_real' the underlying function.

[Mario Carneiro]

I'm not sure I like that idea. There are lots of homs that a function could be, but only one base function, so it makes sense to give the base function the "preferred" name. Plus, usually the base function comes up more often in statements than the hom, unless you set things up so that the coerced hom is the name of the base function (which only works if there is only one hom you can build over a function). of_real might be a bit special in this regard because it will usually be referred to via coe

[Johan Commelin]

I would like mv_polynomial.map to return a ring_hom instead of a function. I don't want to use mv_polynomial.map_hom.

[Johan Commelin]

I think int.cast_ring_hom R is an ugly mouthful for an "invisible" map

[Yury G. Kudryashov]

I think that of_real should be an alg_hom while coe should be defined without of_real.