Zulip Chat Archive

Stream: maths

Topic: name of ring hom associated to function


view this post on Zulip Kevin Buzzard (May 28 2020 at 15:26):

of_real is the function from R\mathbb{R} to C\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

view this post on Zulip Johan Commelin (May 28 2020 at 15:35):

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

view this post on Zulip Johan Commelin (May 28 2020 at 15:35):

I don't like any of these

view this post on Zulip Johan Commelin (May 28 2020 at 15:36):

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.

view this post on Zulip Mario Carneiro (May 28 2020 at 16:37):

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

view this post on Zulip Johan Commelin (May 28 2020 at 16:40):

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.

view this post on Zulip Johan Commelin (May 28 2020 at 16:41):

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

view this post on Zulip Yury G. Kudryashov (May 29 2020 at 05:02):

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


Last updated: May 11 2021 at 15:12 UTC