## Stream: general

### Topic: A Counting Argument

#### Ken Lee (Feb 03 2019 at 09:39):

I am trying to prove:

example {G : Type u} [group G] [fintype G] (HG : ∃ k : ℕ, fintype.card G = 2*k) :
∃ a : G, a ≠ 1 ∧ a = a⁻¹ := sorry


The idea of the proof is to partition the group into sets of elements with their inverses. If there are no non-identity self-inverting elements, then the group would have odd order, giving a contradiction. But I am lost as to how to formalise this into Lean.

#### Neil Strickland (Feb 03 2019 at 10:16):

I would start with fintype.exists_equiv_fin, which will give you a bijection f from G to fin (2 * k). You can then use univ.filter to split G into sets where f(g) is less than, or greater than, or equal to f(g^{-1}). Then you can show that inversion gives a bijection between the first two of these.

#### Mario Carneiro (Feb 03 2019 at 10:19):

I would prove that inv is an involution on G, and its orbits have size 2 or 1... then it's just actual counting

#### Mario Carneiro (Feb 03 2019 at 10:20):

@Chris Hughes is pretty good at this stuff, I wonder if he's tried this

#### Neil Strickland (Feb 03 2019 at 10:32):

That approach seems to need some infrastructure, e.g. a lemma that the cardinality of the union of a finite set of disjoint finite sets is the sum of the cardinalities. It would certainly be good if that was in mathlib, but I cannot find it there at the moment.

#### Kevin Buzzard (Feb 03 2019 at 12:18):

Keji had a map gbar from s to s and a function f on s such that f(x)+f(gbar x) was zero, and wanted to prove that the sum of f over all of s was zero. I muddled through in the above link. I remember it being annoying, but not ever really getting stuck.

#### Chris Hughes (Feb 03 2019 at 12:21):

I don't think it is relevant. What is weirdly relevant is a lemma in sylow, card_modeq_card_fixed_points since inv is an action of C_2 on the group.

#### Kevin Buzzard (Feb 03 2019 at 12:22):

Aah, he also had the hypothesis that f(x) wasn't f(gbar x). Chris -- if you allow Sylow then you can just show that there exists a non-trivial Sylow 2-subgroup and then invoke the lemma that every non-trivial p-group has an element of order p :-)

#### Kevin Buzzard (Feb 03 2019 at 12:23):

The proof Ken mentions (which I've lectured in 2nd year algebra) is a workaround which only works for p=2.

#### Mario Carneiro (Feb 03 2019 at 12:35):

isn't the composition of those two facts Cauchy's theorem (there is an element of order p in a group G when p | |G|)

#### Mario Carneiro (Feb 03 2019 at 12:35):

it's usually a lemma in Sylow

#### Kevin Buzzard (Feb 03 2019 at 12:37):

Right. But the general proof needs groups acting on sets etc, which we don't teach until Y3, and this p=2 version is useful for 2nd years trying to figure out what all the groups of order 6 are by bare hands.

#### Mario Carneiro (Feb 03 2019 at 12:37):

but actually yeah that's definitely easier than the counting argument

#### Mario Carneiro (Feb 03 2019 at 12:37):

unless there is some silly restriction on "allowable proofs"

#### Mario Carneiro (Feb 03 2019 at 12:39):

That approach seems to need some infrastructure, e.g. a lemma that the cardinality of the union of a finite set of disjoint finite sets is the sum of the cardinalities. It would certainly be good if that was in mathlib, but I cannot find it there at the moment.

I think there is a theorem in equiv about splitting a type along the fibers of a function

#### Mario Carneiro (Feb 03 2019 at 12:40):

equiv_sigma_subtype

#### Mario Carneiro (Feb 03 2019 at 12:44):

all the groups of order 6 are by bare hands

I wonder if we can make a group enumeration function? Like the list of all groups of order 6 up to isomorphism, such that you can check that it has cardinality 2

#### Kevin Buzzard (Feb 03 2019 at 14:53):

The naive algorithm for listing all the groups of order 6 up to isomorphism will take forever even in a non-proof-checker computer algebra package. What you want to do is to assume all Chris' Sylow stuff and then make a formally verified database of groups of small order containing each one up to isomorphism exactly once.

#### Kevin Buzzard (Feb 03 2019 at 14:58):

A completely low-level approach, which is pretty horrible, goes like this: all elements have order 1,2,3 or 6. If there's an element of order 6 then it's cyclic. If not then all non-identity elements have orders 2 or 3. By Ken's lemma there's an element of order 2. If all non-identity elements have order 2 then the group is abelian (this is on the problem sheet; $xyxy=1$ so $xy=y^{-1}x^{-1}=yx$) and choosing two elements of order 2 gives a subgroup of order 4, contradiction. So there's an element of order 3 as well, Now we have names for every element -- if $s$ has order 2 and $t$ has order 3 then the group is $\{1,t,t^2,s,st,st^2\}$ and it's just a case of working out $ts$; you go through the possibilities and figure out what's going on It's pretty tedious.

#### Kevin Buzzard (Feb 03 2019 at 14:59):

Sylow tells you immediately that there's a normal subgroup of order 3 and hence it's a semidirect product of $C_3$ and $C_2$; the two actions of $C_2$ on $C_3$ give the two groups.

#### Kevin Buzzard (Feb 03 2019 at 15:00):

I think that before we classify finite groups of small order it would be wise to classify finite abelian groups of small order, which follows from the structure theorem of finitely-generated modules over a PID.

#### Kevin Buzzard (Feb 03 2019 at 15:01):

We have all the tools for this latter result, but it's a pretty messy proof (at least the ones I've seen are). It's easier to do classification of f.g. modules over a Euclidean domain (which has the same answer), but my impression is that there's no point doing this really because ultimately we'll want PID's.

#### Mario Carneiro (Feb 03 2019 at 21:20):

The problem with this kind of argumentation is it's really tailored to the particular order (6 in this case). If you want to do the same thing with 1024 it's hopeless. I want to know if there is some in between algorithm, which uses group theory tricks but may still produce duplicates which have to be eliminated the hard way

#### Kenny Lau (Feb 03 2019 at 21:20):

We don't even know how many groups of order 2048 there are

#### Kevin Buzzard (Feb 03 2019 at 22:07):

This sort of problem is notoriously difficult

#### Kevin Buzzard (Feb 03 2019 at 22:09):

After a while we don't even have good notion. You have to start saying "well here's the multiplication table...". The problem is with p-groups (groups of prime power order). There are 20 groups of order 16 and by order 32 I think there are groups without names -- they're called "the 23rd one on the GAP database of groups of order 32" and things like that

#### Mario Carneiro (Feb 03 2019 at 23:56):

Is there an upper bound on the number of groups up to isomorphism asymptotically better than the naive one?

#### Mario Carneiro (Feb 04 2019 at 00:00):

If you view it as n permutations you get (n!)^n, which you can probably improve if you use the fact that it's a permutation in columns too, although that seems complicated

#### Reid Barton (Feb 04 2019 at 01:29):

https://groupprops.subwiki.org/wiki/Higman-Sims_asymptotic_formula_on_number_of_groups_of_prime_power_order

Last updated: May 11 2021 at 12:15 UTC