Zulip Chat Archive

Stream: maths

Topic: coercion from `rat` to a `char_p` field


Yury G. Kudryashov (Apr 09 2020 at 18:06):

Currently rat.cast defines coe from rat to any division_ring. Is it useful to have coercion to a division ring of non-zero characteristic?

Alex J. Best (Apr 09 2020 at 18:19):

Sounds useful to me!

Yury G. Kudryashov (Apr 09 2020 at 18:25):

When is it useful?

Yury G. Kudryashov (Apr 09 2020 at 18:25):

I mean, it is not a ring_hom in this case.

Alex J. Best (Apr 09 2020 at 18:29):

Well it's convenient right? I would like to talk about 1/2 is in zmod p. If you have a coe from int to any ring and an inv on your ring then having a/b map to a * b^(-1) seems natural.

Yury G. Kudryashov (Apr 09 2020 at 18:33):

Maybe you're right. Though having ↑a + ↑b not always equal to ↑(a + b) seems strange.

Kevin Buzzard (Apr 09 2020 at 19:12):

This sounds like a computer scientist's coercion. I'd happily have a map from Z(p)\mathbb{Z}_{(p)}, the localisation of the integers away from the prime ideal (p)(p), to a division ring of characteristic pp, and what the computer scientists decide to do with 1/p1/p is their own business. It should be a ring homomorphism on this subset I guess.


Last updated: Dec 20 2023 at 11:08 UTC