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.

Now, I would be very embarrassed if you asked me to justify that assertion, but I am pretty sure that GAGA doesn't use the axiom of choice. It is a very natural, very functorial argument that seems canonical from beginning to end.

About the air of magic of GAGA... Well, I think it is not so magic. Serre himself says that it was a very natural thing to do at that time and place -- and he doesn't say that just out of modesty; for instance, he doesn't say that for all his articles. Instead of magic, it was a technical tour de force, where in a prefiguration of Grothendieck's style the right notions (such as flatness) were developed and applied with exquisite precision. But once you have observed the elementary fact that any meromorphic function on the projective line is actually a rational function (a quotient of two polynomials), you have the prototype of all Gaga's result and it is not a tremendous stretch to imagine that everything which is analytic in the projective world is also algebraic.

-
I'm not so sure that it's as straightforward as you say. If I give you an analytic coherent sheaf, would you be able to give me the algebraic coherent sheaf that induces it? –  Makhalan Duff Jan 21 '13 at 4:46
Duff is right. It is generally not well understood how to find the algebraic sheaf that induces a particular algebraic sheaf. It is very misleading to say that GAGA is obvious in any way. –  James D. Taylor Jan 21 '13 at 5:12
@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
*sorry, I meant: "the algebraic sheaf that induces a particular analytic sheaf". @nosr, that sounds more along the lines I was thinking of, but I can't say that I myself am familiar with all the details of the proof. It most certainly is false that GAGA is constructive, and there have been many papers trying to understand the relationship between the analytic side and the algebraic side better. –  James D. Taylor Jan 21 '13 at 5:35
@James D. Taylor: Serre has said that he chose the title of the paper to have the acronym GAGA (as a baby says) because once he had the idea of the descending induction on cohomological degree (a brilliant new idea at that time!) and the graph trick, the rest of the paper was like child's play. All of the hard analytic input (such as the vanishing theorems and finiteness theorems) was already known before the GAGA work was done, and so is not part of the novelty of the paper (but does contain the deepest input into the arguments). Being non-constructive doesn't make it magical. –  user28172 Jan 21 '13 at 5:36