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