Zulip Chat Archive

Stream: maths

Topic: Defining cyclic groups


view this post on Zulip Chris Hughes (Jul 29 2018 at 12:00):

I have quite a bit of group theory waiting to be merged, Sylow's theorems and parity of permutation over a fintype. I cannot merge it because it all depends on some definition of CnC_n. Is it worth having both Zn \mathbb{Z}_n and CnC_n? It would be nice to only have one, but then Zn\mathbb{Z}_n is an add_group which obviously causes problems.

view this post on Zulip Kevin Buzzard (Jul 29 2018 at 12:08):

We surely need a cyclic group with * as the group law. Another issue is that Z/nZ has a canonical generator, namely 1, whereas a cyclic group of order n is a group of order n with the property that a generator exists. A great example of a cyclic group is the units in (Z/pZ), with p prime. The standard proof that it's cyclic is completely nonconstructive.

view this post on Zulip Chris Hughes (Jul 29 2018 at 12:19):

Why would the presence of a canonical generator be a problem? If you don't want it, just ignore it. Any sensible computable version of CnC_n will have a canonical generator anyway, as it should probably be defeq to Zn\mathbb{Z}_n anyway.

view this post on Zulip Kenny Lau (Jul 29 2018 at 12:19):

We surely need a cyclic group with * as the group law. Another issue is that Z/nZ has a canonical generator, namely 1, whereas a cyclic group of order n is a group of order n with the property that a generator exists. A great example of a cyclic group is the units in (Z/pZ), with p prime. The standard proof that it's cyclic is completely nonconstructive.

under which definition of nonconstructive?

view this post on Zulip Chris Hughes (Jul 29 2018 at 12:21):

If you gave me a proof of that I could very easily construct a generator.

view this post on Zulip Mario Carneiro (Jul 29 2018 at 12:59):

I think is_cyclic should be a property of a group, not a particular group

view this post on Zulip Mario Carneiro (Jul 29 2018 at 12:59):

and the Fundamental Theorem of Cyclic groups says that two cyclic groups with the same cardinality are isomorphic

view this post on Zulip Kenny Lau (Jul 29 2018 at 13:00):

class cyclic_group (α : Type*) extends group α :=
(cyclic :  a,  b : α,  i : , a^i = b)

view this post on Zulip Kenny Lau (Jul 29 2018 at 13:00):

https://github.com/dorhinj/leanstuff/blob/master/gourp1.lean

view this post on Zulip Mario Carneiro (Jul 29 2018 at 13:01):

yes, except I don't think it should be part of the hierarchy

view this post on Zulip Kenny Lau (Jul 29 2018 at 13:01):

code not by me

view this post on Zulip Mario Carneiro (Jul 29 2018 at 13:02):

I know, chris reads this too

view this post on Zulip Mario Carneiro (Jul 29 2018 at 13:03):

It is certainly not true that you can construct a generator given a cyclic group

view this post on Zulip Mario Carneiro (Jul 29 2018 at 13:04):

you can at best construct a trunc generator given a fintype or enumerable cyclic group

view this post on Zulip Chris Hughes (Jul 29 2018 at 13:04):

I think is_cyclic should be a property of a group, not a particular group

But we also obviously need the fact that for all n, there exists a cyclic group of order n.

view this post on Zulip Mario Carneiro (Jul 29 2018 at 13:05):

maybe, but it depends on how you want to say it

view this post on Zulip Mario Carneiro (Jul 29 2018 at 13:05):

How would you need that?

view this post on Zulip Chris Hughes (Jul 29 2018 at 13:07):

Parity of a permutation is a homomorphism into C2C_2. In my Sylow proof I needed to use the group action of CpC_p that rotated the elements of a vector GpG^p

view this post on Zulip Mario Carneiro (Jul 29 2018 at 13:08):

For the parity example, I'm on board with Kenny's mu2, although I'm not sure what the name stands for

view this post on Zulip Kenny Lau (Jul 29 2018 at 13:08):

mu_n is the set of the n-th roots of unity in a field

view this post on Zulip Mario Carneiro (Jul 29 2018 at 13:08):

For the group action, that's obviously a subgroup of the group action of the symmetric group

view this post on Zulip Kenny Lau (Jul 29 2018 at 13:08):

I learnt it from LCFT, but I don't know if it is used elsewhere

view this post on Zulip Kenny Lau (Jul 29 2018 at 13:09):

and for the record Kevin wrote that part (and the name)

view this post on Zulip Chris Hughes (Jul 29 2018 at 13:10):

For the Sylow one, I needed to use the map from the naturals to Zn\mathbb{Z}_n, so some random subgroup is not that easy to use.

view this post on Zulip Mario Carneiro (Jul 29 2018 at 13:12):

I guess you want to know that rotate is a group hom from Z to the symmetric group

view this post on Zulip Mario Carneiro (Jul 29 2018 at 13:13):

and its image is cyclic, because the image of any group hom from Z is cyclic

view this post on Zulip Chris Hughes (Jul 29 2018 at 13:13):

More or less. Maybe I could do it differently.

view this post on Zulip Mario Carneiro (Jul 29 2018 at 13:15):

I realize that mathematicians are used to treating CnC_n as one thing, but keeping in mind the isomorphism is equality abuse of notation in this area, it's best to allow for cyclic groups to appear in situ

view this post on Zulip Mario Carneiro (Jul 29 2018 at 13:16):

That said, if you really need a concrete cyclic additive group Zmod n will do the job

view this post on Zulip Kenny Lau (Jul 29 2018 at 13:17):

multiplicative (Zmod n)

view this post on Zulip Chris Hughes (Jul 29 2018 at 13:17):

That's what I used for Sylow. It wasn't that pretty.


Last updated: May 06 2021 at 17:38 UTC