Where do we need the axiom of choice in Riemannian geometry? A friend of mine is a differential geometer, and keeps insisting that he doesn't need the axiom of choice for the things he does. I'm fairly certain that's not true, though I haven't dug into the details of Riemannian geometry (or the real analysis it's based on, or the topology, or the theory of vector spaces, etc...) to try and find a theorem or construction that uses the axiom of choice, or one of its logical equivalences.
So do you know of any result in Riemannian geometry that needs the axiom of choice? They should be there somewhere, I particularily suspect that one or more is hidden in the basic topology results one uses.
 A: Your friend will probably weasel out of this example by claiming that it isn't strictly "Riemannian" geometry, but it's definitely differential geometry.  The example is the Hodge theorem, which asserts that every cohomology class of a Riemannian manifold is represented by a unique harmonic form (where "harmonic" is with respect to the Laplace-Beltrami operator).  I highly doubt that a proof can be crafted without some reasonably serious functional analysis; the standard approach uses elliptic theory and Sobolev theory which requires the Banach-Alaoglu theorem which in turn requires the Tychonoff theorem.  In general I would wager that any result which involves geometric PDE theory (including some results in, say, minimal surface theory which genuinely are Riemmannian) is going to demand the axiom of choice at some level.
Other than that, you might check out the work of Alexander Nabutovsky.  He has obtained some really serious results about the structure of geodesics and on the moduli space of Riemannian metrics using techniques from logic and computability theory - I wouldn't be surprised if AC is hiding somewhere.
A: It looks to me like the Arzelà--Ascoli theorem needs at least some weak form of choice.  (I have started an MO question to clarify this.)  One often uses this in geometry; for example, to guarantee the existence of minimizing geodesics connecting pairs of points.
Edit: See Andres Caicedo's answer on MO (at above link).  The answer is affirmative.  Also, the database list of equivalents he mentions contains some very innocuous-looking statements that I bet your friend has never thought twice about using.
A: It is very possible that your colleague generally avoids using the axiom of choice, because manifolds are relatively concrete objects.  Assuming that your friend is studying only separable manifolds, or better yet only compact ones, that makes it possible to do many constructions very explicitly, without using the axiom of choice. This is similar to the way that various principles of analysis that require the axiom of choice in general do not require the axiom of choice when they are applied to Euclidean spaces. 
So you're right that it may be easier to find AC in the background results.  The trouble is that many of these background results are studied in far more generality than they are used. For example, suppose an analyst uses the fact that $[0,1]\times[0,1]$ is compact. This fact follows from Tychonoff's theorem, which for general topological spaces does require the axiom of choice. But we could prove the compactness of the unit square more directly, avoiding the axiom of choice altogether (this relies on the separability of the square, in particular). 
So sometimes the axiom of choice is used for convenience, by the invocation of a very general result, but it could be avoided if necessary. If we were to study only smooth manifolds that had already been embedded into Euclidean space, I suspect that we would be able to do pretty much everything in Zermelo-Fraenkel set theory without the axiom of choice. But it would take careful attention in the proofs to make sure that we replace choice-based techniques with alternative methods. 
I know this isn't a direct answer to the question, but I think it's relevant since it explains a caveat with possible answers: just because a general result requires AC doesn't mean that AC is required for all consequences of that result. 
