A Counting Argument

Stream: general

[Ken Lee]

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]

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]

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]

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

[Neil Strickland]

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]

Perhaps related: https://github.com/ImperialCollegeLondon/xena-UROP-2018/blob/master/src/xenalib/keji_lemma.lean

[Kevin Buzzard]

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]

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]

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]

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

[Mario Carneiro]

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]

it's usually a lemma in Sylow

[Kevin Buzzard]

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]

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

[Mario Carneiro]

unless there is some silly restriction on "allowable proofs"

[Mario Carneiro]

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]

equiv_sigma_subtype

[Mario Carneiro]

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]

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]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

This sort of problem is notoriously difficult

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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]

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