# Joachim Breitner's Homepage

## 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.

## Comments

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.

"|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?

http://www.math.niu.edu/~rusin/known-math/99/luzin_easton

http://echochamber.me/viewtopic.php?f=17&t=58504

http://en.wikipedia.org/wiki/Easton's_theorem

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

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.