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?
Best Answer
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.