Zulip Chat Archive

Stream: new members

Topic: order of element


view this post on Zulip Alena Gusakov (Jun 24 2020 at 22:47):

So I'd like to prove some things about the order of an element of a group. Based on the definitions/lemmas in group_theory/order_of_element, it seems like what's happening is the group is simply declared as finite, which forces the elements to have finite order. What I'd like to know is whether there's a way to declare some element a : G for (possibly infinite) group G such that order_of a exists, i.e. it's finite. Would I have to grab a finite subgroup of G in order to do that, or is there another way?

view this post on Zulip Alena Gusakov (Jun 24 2020 at 22:49):

(sorry this might be a question that belongs in #Is there code for X? now that I think about it)

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 22:50):

Is it not the case that there's a function which works in general and returns 0 if it has infinite order?

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 22:51):

The cunning way to do the order of an element gg of a group GG in general is to consider the kernel of the map ZG\mathbb{Z}\to G sending nn to gng^n.

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 22:51):

It's principal with a canonical generator.

view this post on Zulip Jalex Stark (Jun 24 2020 at 22:59):

i don't see the function kevin is asking about anywhere nearby docs#order_of

view this post on Zulip Jalex Stark (Jun 24 2020 at 23:00):

but the approach used there will let you define order_of on anything for which you can prove is torsion

view this post on Zulip Alena Gusakov (Jun 25 2020 at 01:05):

I guess what I'm trying to prove is more like, if there exists some element of G of finite order n, then...etc

view this post on Zulip Alena Gusakov (Jun 25 2020 at 01:14):

So it's like, in general, I'm trying to construct the statement order_of a = n → something regardless of whether there actually is an element of finite order in the given group

view this post on Zulip Alena Gusakov (Jun 25 2020 at 01:17):

If the group has no elements of finite order besides the identity, the thing I want to prove is trivially true so it technically is a true statement regardless of whether the group is finite

view this post on Zulip Jalex Stark (Jun 25 2020 at 01:39):

yes, i think the things you're saying mean the same thing I said. You can look at the implementation of order_of_element and add an extra hypothesis ∃ n, x ^ n = 1

view this post on Zulip Jalex Stark (Jun 25 2020 at 01:40):

all of the proofs will go through, changing at most one line in each one

view this post on Zulip Jalex Stark (Jun 25 2020 at 01:41):

maybe I don't know where you are stuck

view this post on Zulip Alena Gusakov (Jun 25 2020 at 01:46):

Ah gotcha, that works. Thanks!

view this post on Zulip Jalex Stark (Jun 25 2020 at 01:57):

and this clearly belongs in mathlib, but I don't know how one would organize it


Last updated: May 14 2021 at 22:15 UTC