Does the proof of GAGA use the axiom of choice?

Serre's GAGA result roughly states the following. Let $X$ be a complex projective algebraic variety. Then the natural functor from the category of coherent sheaves over the algebraic structure sheaf of $X$ to the category of coherent sheaves over the analytic structure sheaf of $X$ is an equivalence of categories.

This theorem always seemed to have the air of magic to me. Things that are analytic must come from algebra. I want to dust away some of this magic, and get a clearer picture. With this goal in mind, I have skimmed the proof of GAGA.

The proof of GAGA is rather involved. It uses Cartan's theorem A for both the algebraic and analytic cases, the isomorphism of the completions of the stalks of the structure sheaf in the algebraic case and the analytic case, and a variety of technical results. After having done that for a few days, I still remain with a sense of amazement and a basic lack of understanding about what makes this work. This brings me to the precise phrasing of my question: (which will hopefully help me find the precise step where the magic happens)

Question

Does the proof of Serre's GAGA theorem use the axiom of choice? If so, at what step does this happen?

-
What the theorem says is that «things that complex analytical must come from algebra», not topological. When you say it that way, it is not thaaaaat surprising, really. –  Mariano Suárez-Alvarez Jan 21 '13 at 4:13
Mariano, it is! Think for example on the case of curves. There it does reduce to saying "topological". –  Makhalan Duff Jan 21 '13 at 4:47
Not really. There are many more continuous maps between projective curves than algebraic ones (as you know!) –  Mariano Suárez-Alvarez Jan 21 '13 at 5:42
There are two different questions one could ask: one is whether Serre's proof of GAGA uses the axiom of Choice, another is whether one can find a metamathematical argument that GAGA must be provable without Choice (an argument similar to the well-known fact that "any arithmetical statement that is provable in ZFC is provable in ZF alone"). I'm pretty convinced the answer of the second question is "yes" (perhaps something like "encode the analytic sheaf as a real number $x$ and argue in $L[x]$ where Choice holds"). But then, that's not what you asked. –  Gro-Tsen Jan 21 '13 at 10:41
Isn't the axiom of choice used all over the place in commutative algebra and algebraic geometry? I would be quite surprised when Serre's proof, and in particular all the already known results which he uses, never uses the axiom of choice. –  Martin Brandenburg Jan 22 '13 at 9:23

First, let me say that the statement of GAGA you recall is true only for a complex algebraic variety that is projective. In general, it is false: take $X$ an affine space, and consider the morphisms from the structural sheaf to itself in both the algebraic and analytic categories. They are just the algebraic, resp. holomorphic function on the affine spaces, which obviously are not the same.
@Makhalan Duff: The proof isn't "constructive", but not because of axiom of choice (which plays no role). The source of all "algebraicity" is algebraicity of $\Gamma(P^n, O(k))$'s and the ability to make resolutions by finite sums of $O(k)$'s (rests on non-constructive facts: coherence of $O_X$, finite-dimensionality of coherent analytic cohomology, and especially the cohomological vanishing properties of $O(1)$ in the coherent analytic theory), coupled with vanishing of all coherent analytic $H^i(P^n,F)$'s for $i > n$ and vanishing of higher analytic cohomology of $O(k)$ ($k>0$). –  user28172 Jan 21 '13 at 5:28