Zulip Chat Archive

Stream: general

Topic: A Counting Argument


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

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

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

view this post on Zulip Mario Carneiro (Feb 03 2019 at 10:20):

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

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

view this post on Zulip Kevin Buzzard (Feb 03 2019 at 12:16):

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

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

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

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

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

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

view this post on Zulip Mario Carneiro (Feb 03 2019 at 12:35):

it's usually a lemma in Sylow

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

view this post on Zulip Mario Carneiro (Feb 03 2019 at 12:37):

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

view this post on Zulip Mario Carneiro (Feb 03 2019 at 12:37):

unless there is some silly restriction on "allowable proofs"

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

view this post on Zulip Mario Carneiro (Feb 03 2019 at 12:40):

equiv_sigma_subtype

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

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

view this post on Zulip 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=1xyxy=1 so xy=y1x1=yxxy=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 ss has order 2 and tt has order 3 then the group is {1,t,t2,s,st,st2}\{1,t,t^2,s,st,st^2\} and it's just a case of working out tsts; you go through the possibilities and figure out what's going on It's pretty tedious.

view this post on Zulip 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 C3C_3 and C2C_2; the two actions of C2C_2 on C3C_3 give the two groups.

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

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

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

view this post on Zulip Kenny Lau (Feb 03 2019 at 21:20):

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

view this post on Zulip Kevin Buzzard (Feb 03 2019 at 22:07):

This sort of problem is notoriously difficult

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

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

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

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