Zulip Chat Archive

Stream: maths

Topic: isomorphism of rings of integers with different radices


view this post on Zulip Roman Bars (Feb 07 2021 at 17:48):

So in Lean there is the standard definition of natural numbers as an inductive type with 0 and such as the constructors. We can also define binary natural numbers with 0, "append 0" and "append 1" as constructors and so on for any number of digits. To all of these types we can add negative numbers and make them into rings.

Can we formalize the idea that for any given number of digits all of these rings are isomorphic?

view this post on Zulip Kevin Buzzard (Feb 07 2021 at 18:04):

Yes, and I would imagine that all these things are done. There is pos_num and num in something like data.num.basic.

view this post on Zulip Mario Carneiro (Feb 07 2021 at 18:04):

For the case of binary natural numbers this is formalized as docs#num.to_nat_inj and similar theorems

view this post on Zulip Mario Carneiro (Feb 07 2021 at 18:05):

although it appears that the statement that num and nat are isomorphic as semirings is not explicitly stated, since it's a fairly low level file

view this post on Zulip Mario Carneiro (Feb 07 2021 at 18:08):

In general, however, rather than constructing a bunch of isomorphic types, I would prefer to see alternate constructors and recursors on nat that allow it to be viewed as binary natural numbers or ternary or phinary or what have you

view this post on Zulip Mario Carneiro (Feb 07 2021 at 18:09):

in the case of binary, this is the bit0 and bit1 functions (on nat), plus docs#nat.binary_rec

view this post on Zulip Bryan Gin-ge Chen (Feb 07 2021 at 18:21):

Along the lines of alternate constructors, there's also docs#nat.of_digits going from lists of natural numbers back to natural numbers.

view this post on Zulip Johan Commelin (Feb 08 2021 at 06:02):

@Roman Bars There is one technical downside to making all these new definitions. Even if you prove that nat is isomorphic to nat_in_base 5, if you prove a lemma about one of them, it isn't transparently automatically true for the other.

view this post on Zulip Johan Commelin (Feb 08 2021 at 06:02):

So the usual approach in formalisation is to build functions (like nat.of_digits that Bryan linked to above) that allow you to treat nat as if it were nat_in_base 5.

view this post on Zulip Johan Commelin (Feb 08 2021 at 06:03):

And there should be lemmas that show that nat.of_digits behaves exactly the way it should with respect to addition, multiplication, etc...


Last updated: May 19 2021 at 02:10 UTC