do non-cyclic groups exist?

Stream: maths

[Kevin Buzzard]

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]

Why not use C_2^2?

[Kevin Buzzard]

I did...

[Kenny Lau]

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

[Kevin Buzzard]

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

[Mario Carneiro]

no, I mean zmod 2 x zmod 2

[Kevin Buzzard]

the problem is still there

[Kevin Buzzard]

I mean the problem I highlight is still there

[Kevin Buzzard]

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

[Reid Barton]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Reid Barton]

or maybe you could even do some pigeonhole argument

[Mario Carneiro]

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

[Kevin Buzzard]

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<m$ I believe

[Kevin Buzzard]

Is is_cyclic decidable?

[Kevin Buzzard]

For infinite groups it sounds scary

[Mario Carneiro]

for finite groups everything is decidable

[Kevin Buzzard]

for finite groups I guess I believe you

[Kevin Buzzard]

right

[Mario Carneiro]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

by the pigeonhole principle it works for finite groups though

[Mario Carneiro]

technically, it does work for Z since it is cyclic

[Kevin Buzzard]

rofl

[Mario Carneiro]

but it doesn't work for Z^2

[Kevin Buzzard]

indeed :-)

[Kevin Buzzard]

Wait

[Kevin Buzzard]

what is order of an element of infinite order?

[Mario Carneiro]

infinite

[Kevin Buzzard]

I'm surprised it's not 37

[Kevin Buzzard]

oh Ok

[Mario Carneiro]

oh you mean in lean

[Kevin Buzzard]

right

[Mario Carneiro]

maybe 0?

[Kevin Buzzard]

exactly!

[Kevin Buzzard]

That's what i said

[Mario Carneiro]

no, like actually 0

[Kevin Buzzard]

right

[Kevin Buzzard]

"the canonical junk value"

[Mario Carneiro]

like characteristic 0

[Mario Carneiro]

like not junk 0

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

exactly

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

so it's really not 0 here

[Mario Carneiro]

I think you should stop worrying about infinite groups here

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

i.e. S3 is not cyclic

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

oh yeah, that's even easier

[Kevin Buzzard]

and subgroups of an abelian group are abelian

[Kevin Buzzard]

If only my minions had started on group theory!

[Mario Carneiro]

do we have the fundamental theorem of cyclic groups?

[Kevin Buzzard]

is there really a fundamental theorem of cyclic groups?

[Kevin Buzzard]

Is there a fundamental theorem for an arbitrary subject?

[Mario Carneiro]

the classification of finite cyclic groups also sounds pretty cool

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

or possibly "polynomial equations", my memory fails me

[Mario Carneiro]

and now "geometry" means "equations"

[Kevin Buzzard]

only algebraic geometry

[Kevin Buzzard]

what's the fundamental theorem of geometry?

[Chris Hughes]

What is the fundamental theorem of cyclic groups?

[Kevin Buzzard]

Do we have that in Lean?

[Kevin Buzzard]

I don't know what the FTCG is

[Kevin Buzzard]

It will either be the classification

[Mario Carneiro]

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

[Kevin Buzzard]

or the universal property

[Kevin Buzzard]

apparently it's the classification

[Kevin Buzzard]

what's the fundamental theorem of cyclic semimodules?

[Mario Carneiro]

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

[Kevin Buzzard]

a semimodule is cyclic if it has a generator

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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,...?

[Reid Barton]

Yes

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Reid Barton]

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

[Kevin Buzzard]

Maybe the toric variety guys think about that case

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

no it can't be that crazy

[Reid Barton]

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]

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

[Reid Barton]

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

[Reid Barton]

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]

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

[Kevin Buzzard]

we seem to have wandered a bit

[Kevin Buzzard]

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]

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)
-/