Defining cyclic groups

Stream: maths

[Chris Hughes]

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]

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]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Mario Carneiro]

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

[Kenny Lau]

code not by me

[Mario Carneiro]

I know, chris reads this too

[Mario Carneiro]

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

[Mario Carneiro]

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

[Chris Hughes]

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]

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

[Mario Carneiro]

How would you need that?

[Chris Hughes]

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]

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

[Kenny Lau]

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

[Mario Carneiro]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Chris Hughes]

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]

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

[Mario Carneiro]

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

[Chris Hughes]

More or less. Maybe I could do it differently.

[Mario Carneiro]

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]

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

[Kenny Lau]

multiplicative (Zmod n)

[Chris Hughes]

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