## Stream: maths

### Topic: Defining cyclic groups

#### 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 $C_n$. Is it worth having both $\mathbb{Z}_n$ and $C_n$? It would be nice to only have one, but then $\mathbb{Z}_n$ is an add_group which obviously causes problems.

#### 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.

#### 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 $C_n$ will have a canonical generator anyway, as it should probably be defeq to $\mathbb{Z}_n$ anyway.

#### 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?

#### Chris Hughes (Jul 29 2018 at 12:21):

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

#### Mario Carneiro (Jul 29 2018 at 12:59):

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

#### 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

#### Kenny Lau (Jul 29 2018 at 13:00):

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


#### Kenny Lau (Jul 29 2018 at 13:00):

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

#### Mario Carneiro (Jul 29 2018 at 13:01):

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

code not by me

#### Mario Carneiro (Jul 29 2018 at 13:02):

I know, chris reads this too

#### Mario Carneiro (Jul 29 2018 at 13:03):

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

#### Mario Carneiro (Jul 29 2018 at 13:04):

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

#### 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.

#### Mario Carneiro (Jul 29 2018 at 13:05):

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

#### Mario Carneiro (Jul 29 2018 at 13:05):

How would you need that?

#### Chris Hughes (Jul 29 2018 at 13:07):

Parity of a permutation is a homomorphism into $C_2$. In my Sylow proof I needed to use the group action of $C_p$ that rotated the elements of a vector $G^p$

#### 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

#### Kenny Lau (Jul 29 2018 at 13:08):

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

#### 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

#### Kenny Lau (Jul 29 2018 at 13:08):

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

#### Kenny Lau (Jul 29 2018 at 13:09):

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

#### Chris Hughes (Jul 29 2018 at 13:10):

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

#### 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

#### Mario Carneiro (Jul 29 2018 at 13:13):

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

#### Chris Hughes (Jul 29 2018 at 13:13):

More or less. Maybe I could do it differently.

#### Mario Carneiro (Jul 29 2018 at 13:15):

I realize that mathematicians are used to treating $C_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

#### 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

#### Kenny Lau (Jul 29 2018 at 13:17):

multiplicative (Zmod n)

#### 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