## Stream: maths

### Topic: do non-cyclic groups exist?

#### Kevin Buzzard (Nov 05 2018 at 17:47):

import group_theory.order_of_element

@[derive decidable_eq]
inductive G : Type
| PP : G
| PM : G
| MP : G
| MM : G

namespace G

instance : fintype G := {
elems := {PP,PM,MP,MM},
complete := λ g, by cases g;simp
}

def mul : G → G → G
| PP PP := PP
| PP PM := PM
| PP MP := MP
| PP MM := MM
| PM PP := PM
| PM PM := PP
| PM MP := MM
| PM MM := MP
| MP PP := MP
| MP PM := MM
| MP MP := PP
| MP MM := PM
| MM PP := MM
| MM PM := MP
| MM MP := PM
| MM MM := PP

instance : group G :=
{ mul := mul,
mul_assoc := dec_trivial,
one := PP,
one_mul := dec_trivial,
mul_one := dec_trivial,
inv := id,
mul_left_inv := dec_trivial
}

example : ¬ (is_cyclic G) := sorry

end G


This is my attempt to prove that non-cyclic groups exist in Lean. I had perhaps naively thought that I was going to get the whole way there with dec_trivial, but I've just realised that my claim that a group is not cyclic is not immediately decidable. For each element g I need to come up with an element h such that h is not in the cyclic group generated by g, which involves showing that for all integers n, h isn't g^n. This suddenly looks a bit more painful than I wanted it to be. Any ideas on how to proceed?

This is motivated by a second year problem sheet question: "True or false? If $G$ is abelian then $G$ is cyclic". [$G$ a group]

#### Mario Carneiro (Nov 05 2018 at 17:49):

Why not use C_2^2?

I did...

#### Kenny Lau (Nov 05 2018 at 17:50):

oh right, and then there (should) be some lemmas about orders of elements in product

#### Kevin Buzzard (Nov 05 2018 at 17:50):

The issue is that proving something isn't cyclic involves checking that infinitely many calculations don't work out

#### Mario Carneiro (Nov 05 2018 at 17:50):

no, I mean zmod 2 x zmod 2

#### Kevin Buzzard (Nov 05 2018 at 17:50):

the problem is still there

#### Kevin Buzzard (Nov 05 2018 at 17:50):

I mean the problem I highlight is still there

#### Kevin Buzzard (Nov 05 2018 at 17:50):

It's just that there's less set-up ;-)

#### Reid Barton (Nov 05 2018 at 17:50):

if you want to do it by dec_trivial, maybe prove that it suffices to consider n < |G| by Lagrange

#### Kevin Buzzard (Nov 05 2018 at 17:51):

or even $0\leq n<|G|$. Is this already in Lean?

#### Mario Carneiro (Nov 05 2018 at 17:51):

You just check that for every element of the group there is a proper subgroup that contains it

#### Reid Barton (Nov 05 2018 at 17:51):

or maybe you could even do some pigeonhole argument

#### Mario Carneiro (Nov 05 2018 at 17:52):

or you could prove that is_cyclic is decidable and then decide it

#### Kevin Buzzard (Nov 05 2018 at 17:52):

If I do the Lagrange thing then it becomes dec_trivial again because @Kenny Lau recently PR'd a decidability instance for $0\leq n I believe

#### Kevin Buzzard (Nov 05 2018 at 17:52):

Is is_cyclic decidable?

#### Kevin Buzzard (Nov 05 2018 at 17:52):

For infinite groups it sounds scary

#### Mario Carneiro (Nov 05 2018 at 17:52):

for finite groups everything is decidable

#### Kevin Buzzard (Nov 05 2018 at 17:52):

for finite groups I guess I believe you

right

#### Mario Carneiro (Nov 05 2018 at 17:53):

It's easy to write a program to calculate the order of an element in a finite group, maybe Chris has already done it

#### Mario Carneiro (Nov 05 2018 at 17:54):

so you just run that on everything and it comes up less than |G| each time

#### Kevin Buzzard (Nov 05 2018 at 17:54):

@Chris Hughes what do you recommend -- I suspect you know well what is there.

#### Kevin Buzzard (Nov 05 2018 at 17:54):

Definition of is_cyclic is not "there's an element of order equal to the order of the group" as this would not work for Z

#### Kevin Buzzard (Nov 05 2018 at 17:55):

I see. So for finite groups one wants "is_cyclic iff exists element of order |G|"

#### Mario Carneiro (Nov 05 2018 at 17:55):

by the pigeonhole principle it works for finite groups though

#### Mario Carneiro (Nov 05 2018 at 17:56):

technically, it does work for Z since it is cyclic

rofl

#### Mario Carneiro (Nov 05 2018 at 17:56):

but it doesn't work for Z^2

indeed :-)

Wait

#### Kevin Buzzard (Nov 05 2018 at 17:56):

what is order of an element of infinite order?

infinite

#### Kevin Buzzard (Nov 05 2018 at 17:56):

I'm surprised it's not 37

oh Ok

#### Mario Carneiro (Nov 05 2018 at 17:57):

oh you mean in lean

right

maybe 0?

exactly!

#### Kevin Buzzard (Nov 05 2018 at 17:57):

That's what i said

#### Mario Carneiro (Nov 05 2018 at 17:57):

no, like actually 0

right

#### Kevin Buzzard (Nov 05 2018 at 17:57):

"the canonical junk value"

#### Mario Carneiro (Nov 05 2018 at 17:58):

like characteristic 0

like not junk 0

#### Kevin Buzzard (Nov 05 2018 at 17:58):

oh, you're right: there is an argument which says the order really is zero

#### Kevin Buzzard (Nov 05 2018 at 17:59):

the order of an element should really be the ideal of Z consisting of n such that g^n=id

exactly

#### Kevin Buzzard (Nov 05 2018 at 17:59):

and if you really want a number, then choose the generator which is in nat

#### Kevin Buzzard (Nov 05 2018 at 17:59):

fortunately, the order of an infinite group in Lean is probably 0 ;-)

#### Kevin Buzzard (Nov 05 2018 at 18:00):

I guess there are two order functions, one for cardinals and one for finite cardinals

#### Kevin Buzzard (Nov 05 2018 at 18:00):

so it's really not 0 here

#### Mario Carneiro (Nov 05 2018 at 18:02):

I think you should stop worrying about infinite groups here

#### Kevin Buzzard (Nov 05 2018 at 18:02):

:-) Yeah, especially given that I proved that G was a fintype

#### Kevin Buzzard (Nov 05 2018 at 18:03):

Here's a challenge -- prove that permutations of a type are cyclic iff the type has at most 2 terms.

#### Mario Carneiro (Nov 05 2018 at 18:04):

i.e. S3 is not cyclic

#### Kevin Buzzard (Nov 05 2018 at 18:04):

Could also say perms are abelian iff type has at most 2 terms.

#### Kevin Buzzard (Nov 05 2018 at 18:04):

Well, do we know that subgroups of a cyclic group are cyclic?

#### Mario Carneiro (Nov 05 2018 at 18:04):

oh yeah, that's even easier

#### Kevin Buzzard (Nov 05 2018 at 18:05):

and subgroups of an abelian group are abelian

#### Kevin Buzzard (Nov 05 2018 at 18:05):

If only my minions had started on group theory!

#### Mario Carneiro (Nov 05 2018 at 18:05):

do we have the fundamental theorem of cyclic groups?

#### Kevin Buzzard (Nov 05 2018 at 18:06):

is there really a fundamental theorem of cyclic groups?

#### Kevin Buzzard (Nov 05 2018 at 18:06):

Is there a fundamental theorem for an arbitrary subject?

#### Mario Carneiro (Nov 05 2018 at 18:06):

the classification of finite cyclic groups also sounds pretty cool

#### Kevin Buzzard (Nov 05 2018 at 18:06):

I just had a rant in a lecture about how the fundamental theorem of algebra had a really terrible name

#### Kevin Buzzard (Nov 05 2018 at 18:06):

it was named when "algebra" meant the same as "equations", according to Wikipedia

#### Kevin Buzzard (Nov 05 2018 at 18:07):

or possibly "polynomial equations", my memory fails me

#### Mario Carneiro (Nov 05 2018 at 18:07):

and now "geometry" means "equations"

#### Kevin Buzzard (Nov 05 2018 at 18:07):

only algebraic geometry

#### Kevin Buzzard (Nov 05 2018 at 18:07):

what's the fundamental theorem of geometry?

#### Chris Hughes (Nov 05 2018 at 18:08):

What is the fundamental theorem of cyclic groups?

#### Kevin Buzzard (Nov 05 2018 at 18:08):

Do we have that in Lean?

#### Kevin Buzzard (Nov 05 2018 at 18:08):

I don't know what the FTCG is

#### Kevin Buzzard (Nov 05 2018 at 18:08):

It will either be the classification

#### Mario Carneiro (Nov 05 2018 at 18:08):

every cyclic group is isomorphic to Z/nZ for some n, or Z

#### Kevin Buzzard (Nov 05 2018 at 18:08):

or the universal property

#### Kevin Buzzard (Nov 05 2018 at 18:08):

apparently it's the classification

#### Kevin Buzzard (Nov 05 2018 at 18:09):

what's the fundamental theorem of cyclic semimodules?

#### Mario Carneiro (Nov 05 2018 at 18:09):

I'm pretty sure no one calls it a fundamental theorem except me

#### Kevin Buzzard (Nov 05 2018 at 18:09):

a semimodule is cyclic if it has a generator

#### Kevin Buzzard (Nov 05 2018 at 18:10):

People certainly talk about cyclic modules, and the fundamental theorem for them is that a module is cyclic iff it's isomorphic to $R/I$ for some ideal $I$ of the commutative ring $R$

#### Kevin Buzzard (Nov 05 2018 at 18:10):

(and I guess there's an easy generalisation to the non-commutative case)

#### Kevin Buzzard (Nov 05 2018 at 18:11):

but I don't know enough about semirings to know how this generalises

#### Kevin Buzzard (Nov 05 2018 at 18:11):

e.g I don't know the definition of a semiring

#### Kevin Buzzard (Nov 05 2018 at 18:11):

or any examples other than $\mathbb{N}$

#### Kevin Buzzard (Nov 05 2018 at 18:13):

Can you have a semimodule for nat whose underlying set is {0,1,2,3} and if you keep adding 1 you get the sequence 0,1,2,3,2,3,2,3,2,3,...?

Yes

#### Kevin Buzzard (Nov 05 2018 at 18:14):

so the fundamental theorem has to deal with both the "tail" and the "loop"

#### Kevin Buzzard (Nov 05 2018 at 18:14):

eew and if the semiring is non-semiNoetherian then this might be pretty ghastly

#### Kevin Buzzard (Nov 05 2018 at 18:14):

I can see why they didn't catch on in the maths community

#### Reid Barton (Nov 05 2018 at 18:14):

even if it's, like, $\mathbb{N}^2$ I think things will get complicated

#### Kevin Buzzard (Nov 05 2018 at 18:15):

Maybe the toric variety guys think about that case

#### Kevin Buzzard (Nov 05 2018 at 18:15):

don't they do submonoids of N^2 etc?

#### Kevin Buzzard (Nov 05 2018 at 18:17):

For N^2 you can imagine a wildly complicated module where the two generators ("up" and "right") get you through some maze and if you deviate beyond some perimeter then you have to go back to the start

#### Kevin Buzzard (Nov 05 2018 at 18:17):

no it can't be that crazy

#### Reid Barton (Nov 05 2018 at 18:17):

The difficulty is that a congruence (an equivalence relation "~" such that a ~ a' and b ~ b' implies a + a' ~ b + b') is no longer uniquely determined by the set of a for which a ~ 0

#### Kevin Buzzard (Nov 05 2018 at 18:17):

I would need some sort of free semiring for that sort of fun

#### Reid Barton (Nov 05 2018 at 18:19):

when forming the quotient of some algebraic object, you're really quotienting out by a congruence

#### Reid Barton (Nov 05 2018 at 18:20):

it's just that the ability to subtract lets us identify congruences with (for example) submodules, so now submodules are also the things you can quotient by

#### Kevin Buzzard (Nov 05 2018 at 18:20):

wait -- I thought we were trying to prove that C_2 x C_2 wasn't cyclic

#### Kevin Buzzard (Nov 05 2018 at 18:20):

we seem to have wandered a bit

#### Kevin Buzzard (Nov 08 2018 at 21:03):

I still can't prove that Z/2 x Z/2 is not cyclic using dec_trivial. Here's an even easier instance of things failing:

import group_theory.order_of_element

@[derive decidable_eq]
inductive G : Type
| P : G
| M : G

namespace G

instance : fintype G := {
elems := {P,M},
complete := λ g, by cases g;simp
}

def mul : G → G → G
| P P := P
| P M := M
| M P := M
| M M := P

instance : group G :=
{ mul := mul,
mul_assoc := dec_trivial,
one := P,
one_mul := dec_trivial,
mul_one := dec_trivial,
inv := id,
mul_left_inv := dec_trivial
}

#eval to_bool (M ∈ finset.image (pow P) (finset.range (order_of P)))
-- #reduce to_bool (M ∈ finset.image (pow P) (finset.range (order_of P))) -- deterministic timeout

-- #eval to_bool (M ∈ gpowers P) -- maximum class-instance resolution depth has been reached

-- example : ¬ (M ∈ gpowers P) := dec_trivial -- max class-instance res

end G


#### Kevin Buzzard (Nov 08 2018 at 21:06):

Note also

#check @decidable_gpowers
/-
decidable_gpowers :
Π {α : Type u_1} {a : α} [_inst_1 : group α] [_inst_2 : fintype α] [_inst_3 : decidable_eq α],
decidable_pred (gpowers a)
-/


Last updated: May 09 2021 at 11:09 UTC