Zulip Chat Archive

Stream: triage

Topic: issue #1563: order of element


view this post on Zulip Random Issue Bot (Jan 18 2021 at 14:46):

Today I chose issue 1563 for discussion!

order of element
Created by @Johan Commelin (@jcommelin) on 2019-10-17
Labels: easy, needs-refactor

Is this issue still relevant? Any recent updates? Anyone making progress?

view this post on Zulip Random Issue Bot (Jan 23 2021 at 14:43):

Today I chose issue 1563 for discussion!

order of element
Created by @Johan Commelin (@jcommelin) on 2019-10-17
Labels: easy, needs-refactor

Is this issue still relevant? Any recent updates? Anyone making progress?

view this post on Zulip Kevin Buzzard (Jan 23 2021 at 14:58):

A bunch of theorems in that file are true for infinite groups if you define the order of an element of infinite order to be 0. I'm surprised that this was not the convention chosen by Johannes.

view this post on Zulip Kevin Buzzard (Jan 23 2021 at 14:59):

Even more are true if you use fincard (the cardinal of an infinite set being 0)

view this post on Zulip Julian Külshammer (Jan 23 2021 at 15:59):

I recently looked at this issue and was confused as to why the order of an element is only defined for finite groups. This seems like it wouldn't scale well in the future.

view this post on Zulip Kevin Buzzard (Jan 23 2021 at 16:07):

One issue is that nat is much easier to work with than enat (:= N{}\mathbb{N}\cup\{\infty\}), and lean likes total functions. The rather esoteric solution of letting elements of infinite order have order 0 looks weird to mathematicians but actually works really nicely, and this is because a conceptual way of thinking about the order of g is the kernel of the map from Z to G sending 1 to g; this kernel has a unique nonnegative generator which one could define to be the order.

view this post on Zulip Julian Külshammer (Jan 23 2021 at 16:16):

Another question I had regarding this issue was why the characteristic of a ring is not defined as the order of 1? If one defined the order here as zero if infinite, then this would also agree with characteristic 0.

view this post on Zulip Kevin Buzzard (Jan 23 2021 at 16:23):

I agree that this would be a nice way to do it! Perhaps the answer is simply that it was done another way and we now have an API which works, so why change it? It doesn't really matter what the definitions are as long as the API is there.


Last updated: May 09 2021 at 16:20 UTC