Zulip Chat Archive
Stream: triage
Topic: issue #3975: remove the coercion from zmod n to other rings
Random Issue Bot (Mar 04 2021 at 14:21):
Today I chose issue 3975 for discussion!
remove the coercion from zmod n to other rings
Created by @Johan Commelin (@jcommelin) on 2020-08-29
Labels: needs-refactor
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Apr 18 2021 at 14:22):
Today I chose issue 3975 for discussion!
remove the coercion from zmod n to other rings
Created by @Johan Commelin (@jcommelin) on 2020-08-29
Labels: needs-refactor
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Nov 11 2021 at 14:19):
Today I chose issue 3975 for discussion!
remove the coercion from zmod n to other rings
Created by @Johan Commelin (@jcommelin) on 2020-08-29
Labels: needs-refactor
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Dec 08 2021 at 14:20):
Today I chose issue 3975 for discussion!
remove the coercion from zmod n to other rings
Created by @Johan Commelin (@jcommelin) on 2020-08-29
Labels: needs-refactor
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Feb 21 2022 at 14:13):
Today I chose issue 3975 for discussion!
remove the coercion from zmod n to other rings
Created by @Johan Commelin (@jcommelin) on 2020-08-29
Labels: needs-refactor
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Sep 24 2022 at 14:17):
Today I chose issue 3975 for discussion!
remove the coercion from zmod n to other rings
Created by @Johan Commelin (@jcommelin) on 2020-08-29
Labels: needs-refactor
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jun 21 2023 at 14:07):
Today I chose issue 3975 for discussion!
remove the coercion from zmod n to other rings
Created by @Johan Commelin (@jcommelin) on 2020-08-29
Labels: needs-refactor
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jul 28 2023 at 14:06):
Today I chose issue 3975 for discussion!
remove the coercion from zmod n to other rings
Created by @Johan Commelin (@jcommelin) on 2020-08-29
Labels: needs-refactor
Is this issue still relevant? Any recent updates? Anyone making progress?
Kevin Buzzard (Jul 28 2023 at 14:28):
I used to be really anti this coercion full stop but recently I've been working with a student who has been using them. However they seem to have to continually change the coercion to the coercion from to followed by the sensible coercion from to the target ring. So perhaps one approach is to allow the coercion to but not allow it in general?
Johan Commelin (Jul 29 2023 at 06:09):
But the coercion to Int is quite unnatural from a maths POV. So if that's to be used, I would rather just see it appear explicitly in the goal view as a named function.
Kevin Buzzard (Jul 29 2023 at 08:47):
Yes; the advantage is that the coercion to Int is just one unnatural function and developing some API for it is I think a better way to go than introducing all these weird functions from Z/nZ to any ring and then having even less that one can say about them.
Maybe the answer is just to use API for val (the map to Nat) and then demand that the user goes through Nat every time, i.e. remove the coercion and encourage the route via Nat. I just suggested int because you sometimes want to do subtraction.
Eric Wieser (Jul 29 2023 at 09:57):
The route through val is nonsense for ZMod 0 though
Kevin Buzzard (Jul 29 2023 at 10:32):
Aah! So maybe we want to encourage the route through Int?
Eric Wieser (Jul 29 2023 at 10:47):
I mean, probably we actualy want to encourage the route through docs#ZMod.lift
Kevin Buzzard (Jul 29 2023 at 10:53):
The issue is that sometimes you really do want to lift from Z/nZ to Z, e.g. to do some auxiliary construction and then prove it's well-defined.
Last updated: Dec 20 2023 at 11:08 UTC