Zulip Chat Archive

Stream: maths

Topic: name of ring hom associated to function


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

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".

Johan Commelin (May 28 2020 at 15:35):

I don't like any of these

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.

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

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.

Johan Commelin (May 28 2020 at 16:41):

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

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: Dec 20 2023 at 11:08 UTC