Free Groups Formalized

Since a few months, I have been playing around with Isabelle, a theorem prover system. I find it very intriguing to have proofs of mathematical statements checked by something as pendantic and comprehensive as a machine. Mathematicians always claim that their statements are true in all eternity, but the proofs are just checked by error-prone human beings. Especially with complex, large proofs that are only read by a handful of people, I doubt that these are always fully correct. Note that this does not imply that I doubt that the results are correct. They probably are. But a bit of doubt remains. A computer-checked proof, in contrast, can not accidentially omit corner cases, leave out seemingly “trivial” assumtions of used theorems or be misled by slightly differing definition from different sources.

I was hoping to check at least parts of my diploma thesis using Isabelle, but it turns out that the standard algebra library shipped with Isabelle is not complete enough. Even free groups were missing. This was motivation enough to try to formalize them and prove the universal property and some isomorphisms (The free group over the empty set is the unit group, the free group over one generator is the additive group of integers and free groups over sets of same cardinality are isomophic). I submitted the resulting theory to the Archive of Formal Proofs and it was accepted. You can view the complete document or the document without proofs.

I did not formalize the fact that isomorphic free groups have bases of same cardinality. As far as I know there is no simple argument that works directly with free groups. The proofs I have seen pass to the abelianization of the free group, i.e. the free module over ℤ and apply the well known proof from the analogous statement about vector spaces. But if someone knows an elementary proof of this fact, I’d like to hear about it.


Did you try with covering spaces? - i.e., the same way as the sensible proof that a subgroup of a free group is free.
#1 Anon am 2010-07-03T13:46:38+00:00
I doubt that it will be much easier, as it would involve results from Topology. But maybe... do you have a pointer to such a proof?
#2 Joachim Breitner (Homepage) am 2010-07-03T14:04:34+00:00
How about counting the homomorphisms to the group of order 2?
#3 Christian Sievers am 2010-09-09T21:32:41+00:00
Not sure... can you elaborate?
#4 Joachim Breitner (Homepage) am 2010-09-10T08:44:40+00:00
By the universal property, Hom(F(X),C2) corresponds to the mappings from X to (the underlying set of) C2 of which there are 2^card(X).
Isomorphic grops have "essentially the same" homomorphisms to C2 (after all, Hom is a functor; a direct proof that the cardinality is the same is also simple).

So if card(X) and card(Y) are different, F(X) and F(Y) have a different number of homomorphisms to C2 and cannot be isomorphic.

Not sure how difficult it is to convince Isabelle, but I think this qualifies as a more elementary proof.
#5 Christian Sievers am 2010-09-10T10:05:40+00:00
That sounds sensible. I’m not sure how many lemmas are used implicitly by you that need to be proven first in Isabelle, but I’ll try it some time. Thanks!
#6 Joachim Breitner (Homepage) am 2010-09-10T13:20:55+00:00
Hmm, after thinking some about it, I noticed that you reduced the question to the following proposition:
"|P(X)| = |P(Y)| ==> |X| = |Y|"
which is obviously true for finite sets. But does it hold for inifinite sets? (My feeling says yes..) And how do you prove it?
#7 Joachim Breitner (Homepage) am 2010-09-18T13:46:21+00:00
Might this actually require the generalized continuum hypothesis?
#8 Joachim Breitner (Homepage) am 2010-09-18T14:24:03+00:00
It follows from GHC and need not be true without, but if I understand correctly, it can be true without GHC. See:
#9 Christian Sievers am 2010-10-07T21:56:43+00:00
Ok, it’s actually simpler: Your approach works for finite bases, and I just finished formalizing it in Isabelle.

For inifinite bases there is not much to show as then the cardinality of the free group is the same as that of the basis. Unfortunately, _this_ fact is not easy to be shown in Isabelle/HOL, due to lack of cardinal numbers (In Isabelle/ZF it would probably work.)
#10 Joachim Breitner (Homepage) am 2010-09-19T13:58:41+00:00

Have something to say? You can post a comment by sending an e-Mail to me at <mail@joachim-breitner.de>, and I will include it here.