I had in mind the $\sigma$-algebra structure on $\overline{\mathbb Q}_p$ induced by the Borel-algebra on all finite extensions of $\mathbb Q_p$ (and the standard one on $\mathbb C$). For each finite extension of $\mathbb Q_p$ there is a measurable bijection between it and $\mathbb C$. By rearranging them for different extensions one should (I haven't properly checked it though) get the bijection for $\overline{\mathbb Q}_p$.

There is even a measurable (defined appropriately) bijection between them so that's no problem. Let me rephrase my objection. There have been things in the past that I have considered obviously false but were wrong about. I certainly don't exclude the possibility that someone could give a convincing construction of an isomorphism which would force me to modify my intuition. However, the axiom of choice is sufficiently nebulous so that the fact that it implies the existence rather has made me put it on the restricted list of results whose acceptability I prefer to judge on a case by case basis.

Yes, if you look at the proof of Steinitz theorem it is in the construction of transcendence bases that the axiom choice is most heavily used. (It is also used in the extension to the algebraic closure but that is much more benign.)

@Thomas: As I understand it Freyd meant (and I just tried to follow him) the subcategory of the stable category consisting of finite complexes and their shifts (which of course can be defined without embedding it in the larger category).

@François: I completely agree with you and I also tried to explain that in my original answer. @Minhyong: What is the original isomorphism $F \simeq K$ in the case at hand?

(cont'd) Things become more complicated when you are saying that two uncountable algebraically closed fields of the same characteristic and cardinality isomorphic. That uses the axiom of choice even with the bijection given. Note that I rather accept consequences of the axiom of choice on a case by case basis. Hence, the case of an embedding of the p-adic field into is one that I have met so many times so I had to take a stand. The case of for instance the existence of a maximal is different because there are so many natural cases where it can be proved without the axiom of choice.

To take your question first. You are assuming we have a bijection between $S$ and $T$ which of course allows us to give a very explicit formula for the isomorphism between $Q(S)$ and $Q(T)$. This is completely constructive, there is of course a free variable or universal quantifier for the bijection but that is no problem, you get the bijection as input and don't bother where it comes from.

(cont'd) I think that if you look at Thomason's proof it seems that the split reductive proof is done by using that the group scheme is the pullback from a group scheme over $\mathbb Z$ which is another way of interpreting SGA III I believe.

Interesting approach. However, if I understand SGA III:Exp XIII right there are is only one infinitesimal deformation of a reductive group (the reduction to the split case is easy) and hence in that case there is nothing to prove. (All linearly reductive groups are reductive so that condition does not give us anything new.) So I think that unfortunately you were right in believing that the stack techniques can be avoided and that there are lots of interesting cases left.

So may recollection was so vague that I got even the direction wrong...

@Eric: This is not a correct description of Freyd's conjecture. It says that stable homotopy groups give a full embedding of the finite homotopy category into that of modules over the stable homotopy ring of spheres. The stable homotopy category also is not abelian, it is triangulated. It is even known that the stable homotopy category is not the derived category of a ring. (I think it may be the derived category of a differential graded ring and I even have some vague recollection that this has been proved.)

A stupid answer is to compose $\pi$ with the zero section of $\overline\pi$, I assume you want to rule that out...