11
$\begingroup$

Let $F(X)$ be the free group on a set $X$. Classically, we can prove the statement:

$F(X) \cong F(Y)$ if and only if $|X|=|Y|$.

The proofs (that I have seen) consist of turning the group isomorphism into an isomorphism of free abelian groups, then an isomorphism of vector spaces by modding out by some $p$. Where we can deduce that isomorphic vector spaces have bijective basis sets.

The last part of this proof uses AC. I came across Kleppmann - Generating sets of free groups and the axiom of choice, which proves that ZF + boolean prime ideal theorem can prove this, therefore it is weaker than AC.

I am interested in knowing how true this statement is constructively. I.e. are uses of excluded middle and choice (or rather statements weaker than choice) necessary to prove it?

Improve this question
$\endgroup$
22
  • 3
    $\begingroup$ @YCor What else could it mean? $\endgroup$
    – Mike Shulman
    Commented May 2, 2020 at 21:22
  • 1
    $\begingroup$ @MikeShulman when I first read it, I thought of it as "there exists a free generating subset of the first one and...etc." I converged to the wording I'm writing just by elimination. Actually "free" is hopelessly ambiguous since mathematicians use the same word for "free over some given subset" and "free over some subset"; of course often this doesn't matter, but precisely here it matters. $\endgroup$
    – YCor
    Commented May 2, 2020 at 21:23
  • 2
    $\begingroup$ @YCor Hopefully things are more clear now. $\endgroup$
    – Ali Caglayan
    Commented May 2, 2020 at 23:15
  • 1
    $\begingroup$ @LSpice This is Kleppmann's dissertation which I think Paul was referring to. $\endgroup$
    – Ali Caglayan
    Commented May 2, 2020 at 23:51
  • 1
    $\begingroup$ @LSpice I've changed it to "or" as that sounds better. $\endgroup$
    – Ali Caglayan
    Commented May 3, 2020 at 19:17

0

Reset to default

You must log in to answer this question.