Zulip Chat Archive

Stream: maths

Topic: do non-cyclic groups exist?


view this post on Zulip 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 GG is abelian then GG is cyclic". [GG a group]

view this post on Zulip Mario Carneiro (Nov 05 2018 at 17:49):

Why not use C_2^2?

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 17:50):

I did...

view this post on Zulip Kenny Lau (Nov 05 2018 at 17:50):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 05 2018 at 17:50):

no, I mean zmod 2 x zmod 2

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 17:50):

the problem is still there

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 17:50):

I mean the problem I highlight is still there

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 17:50):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 17:51):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 05 2018 at 17:51):

or maybe you could even do some pigeonhole argument

view this post on Zulip Mario Carneiro (Nov 05 2018 at 17:52):

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

view this post on Zulip 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 0n<m0\leq n<m I believe

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 17:52):

Is is_cyclic decidable?

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 17:52):

For infinite groups it sounds scary

view this post on Zulip Mario Carneiro (Nov 05 2018 at 17:52):

for finite groups everything is decidable

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 17:52):

for finite groups I guess I believe you

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 17:52):

right

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 05 2018 at 17:54):

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

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 17:54):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 17:55):

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

view this post on Zulip Mario Carneiro (Nov 05 2018 at 17:55):

by the pigeonhole principle it works for finite groups though

view this post on Zulip Mario Carneiro (Nov 05 2018 at 17:56):

technically, it does work for Z since it is cyclic

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 17:56):

rofl

view this post on Zulip Mario Carneiro (Nov 05 2018 at 17:56):

but it doesn't work for Z^2

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 17:56):

indeed :-)

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 17:56):

Wait

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 17:56):

what is order of an element of infinite order?

view this post on Zulip Mario Carneiro (Nov 05 2018 at 17:56):

infinite

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 17:56):

I'm surprised it's not 37

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 17:57):

oh Ok

view this post on Zulip Mario Carneiro (Nov 05 2018 at 17:57):

oh you mean in lean

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 17:57):

right

view this post on Zulip Mario Carneiro (Nov 05 2018 at 17:57):

maybe 0?

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 17:57):

exactly!

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 17:57):

That's what i said

view this post on Zulip Mario Carneiro (Nov 05 2018 at 17:57):

no, like actually 0

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 17:57):

right

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 17:57):

"the canonical junk value"

view this post on Zulip Mario Carneiro (Nov 05 2018 at 17:58):

like characteristic 0

view this post on Zulip Mario Carneiro (Nov 05 2018 at 17:58):

like not junk 0

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 17:58):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 05 2018 at 17:59):

exactly

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 17:59):

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

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 17:59):

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

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 18:00):

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

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 18:00):

so it's really not 0 here

view this post on Zulip Mario Carneiro (Nov 05 2018 at 18:02):

I think you should stop worrying about infinite groups here

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 18:02):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 05 2018 at 18:04):

i.e. S3 is not cyclic

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 18:04):

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

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 18:04):

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

view this post on Zulip Mario Carneiro (Nov 05 2018 at 18:04):

oh yeah, that's even easier

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 18:05):

and subgroups of an abelian group are abelian

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 18:05):

If only my minions had started on group theory!

view this post on Zulip Mario Carneiro (Nov 05 2018 at 18:05):

do we have the fundamental theorem of cyclic groups?

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 18:06):

is there really a fundamental theorem of cyclic groups?

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 18:06):

Is there a fundamental theorem for an arbitrary subject?

view this post on Zulip Mario Carneiro (Nov 05 2018 at 18:06):

the classification of finite cyclic groups also sounds pretty cool

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 18:06):

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

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 18:07):

or possibly "polynomial equations", my memory fails me

view this post on Zulip Mario Carneiro (Nov 05 2018 at 18:07):

and now "geometry" means "equations"

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 18:07):

only algebraic geometry

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 18:07):

what's the fundamental theorem of geometry?

view this post on Zulip Chris Hughes (Nov 05 2018 at 18:08):

What is the fundamental theorem of cyclic groups?

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 18:08):

Do we have that in Lean?

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 18:08):

I don't know what the FTCG is

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 18:08):

It will either be the classification

view this post on Zulip Mario Carneiro (Nov 05 2018 at 18:08):

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

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 18:08):

or the universal property

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 18:08):

apparently it's the classification

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 18:09):

what's the fundamental theorem of cyclic semimodules?

view this post on Zulip Mario Carneiro (Nov 05 2018 at 18:09):

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

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 18:09):

a semimodule is cyclic if it has a generator

view this post on Zulip 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/IR/I for some ideal II of the commutative ring RR

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 18:10):

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

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 18:11):

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

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 18:11):

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

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 18:11):

or any examples other than N\mathbb{N}

view this post on Zulip 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,...?

view this post on Zulip Reid Barton (Nov 05 2018 at 18:13):

Yes

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 18:14):

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

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 18:14):

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

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 18:14):

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

view this post on Zulip Reid Barton (Nov 05 2018 at 18:14):

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

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 18:15):

Maybe the toric variety guys think about that case

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 18:15):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 18:17):

no it can't be that crazy

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 18:17):

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

view this post on Zulip Reid Barton (Nov 05 2018 at 18:19):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 18:20):

we seem to have wandered a bit

view this post on Zulip 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

view this post on Zulip 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