It is well known that the Stone–Čech compactification $\beta \mathbb N^+$ of the positive natural numbers has the structure of a compact left semitopological semigroup and hence, by Ellis's lemma, has idempotents. The usual proof of Ellis's lemma uses Zorn's lemma. Idempotent ultrafilters are clearly non-principal. It is known that the existence of non-principal ultrafilters is weaker than the axiom of choice. 


My question is whether the existence of idempotent ultrafilters in $\beta \mathbb N^+$ is still weaker than choice?



Is choice needed to establish the existence of idempotent ultrafilters?
Yes, it's still weaker. To build a model of ZF in which choice fails but $\beta\mathbb N^+$ has idempotents, start with a model of ZFC (which will, of course, have idempotent ultrafilters in $\beta\mathbb N^+$). Add a lot of Cohen-generic subsets of some regular cardinal $\kappa$ well above the cardinal of the continuum; forcing conditions are partial functions of size $<\kappa$. No new reals are added, and your idempotent ultrafilters from the ground model are still idempotent ultrafilters (and AC still holds). Now pass to the symmetric submodel given by the group of automorphisms of your forcing that permutes the names of the added Cohen subsets, with the filter determined by supports of size $<\kappa$. That model violates choice, because you can't well-order the power set of $\kappa$. But the ground model's reals and ultrafilters haven't been touched, so you still have the same idempotent ultrafilters that you had to start with.


