What do we get with the Axiom of Choice (AC) in Functional Analysis that cannot be accomplished with Zermelo-Fraenkel (ZF) plus the Axiom of Dependent Choice (DC)?
So, for instance, just dusted off and opened my old class notes and saw
- Hahn-Banach (see note below)
Baire Category (see note below)
Open Mapping / Closed Graph thrms
- Uniform Boundedness Principle
- Projection Lemma (Hilbert Space)
- Unit Ball is weak-* compact (Banach-Algaoglu)
- Riesz Representation Theorem (see note below)
- Spectral Theorem
- Separation of Convex sets by Hyperplanes
- Basic theorems about distribution functions/L^P spaces
... and any other theorems you can think of that fit in this theme of being well known to anyone who took a basic course in functional analysis, and useful to people who use analysis in their work. Please add to list b/c I am sure I forgot some theorems.
(note on Hahn-Banach: In the spirit of the question, the most concrete form that is still abstract enough to use in the proofs of the other theorems is fine here. For instance, in my notes I have $p$ sublinear on a N.V.S. $X$ and $V$ a subspace of $X$, $f\in V^*$ and $|f|\le p$ on $V$ as the assumptions.
note on Baire Category: The version that every complete metric space (or Banach space) is a Baire space would likely be sufficient here since I believe that the second one that locally compact Hausdorff spaces are Baire might not be standard material for a basic course in Functional Analysis. Please correct me if I'm wrong!)
So, which require AC if one already accepts ZF+DC?
Edit This is intended to be more a question about the internal logical dependencies of Functional Analysis than about logic and set theory. A good answer does not need to prove each of the theorems separately. In particular, One might show theorems $n_1$ and $n_2$ can be proven with DC by citing good links. Then say "a standard proof for $n_3$ uses $n_1$ and some epsilon delta stuff. A standard proof $n_4$ uses $n_2$ and $n_3$ plus image of compact sets is compact, so also doesn't need full AC." For the ones that do need AC, maybe a good link for one and then a link showing that others are equivalent under ZF.
In other words, what I am looking for is for someone to take the few theorems about DC vs. AC that have already been proven, and flesh this out to the rest of (basic) functional analysis by discussing logical dependencies within the field of functional analysis.
Please only assume a background in functional analysis, not in Foundations (sets/logic/etc. beyond everyday use). References to other questions where the details have been worked out in more rigour are quite sufficient.
There is an obvious item missing from your list: the existence of nonmeasurable sets. The second Solovay model (see here) is a model of ZF+DC and all of its sets are Lebesgue measurable. Without being able to mention the existence of nonmeasurable sets it becomes difficult to motivate the machinery of $\sigma$-algebras. Furthermore Terry Tao has pointed out some nifty applications of nonmeasurable sets, particularly in the context of Robinson's framework.
In another direction, you can't even start talking about the Stone-Čech compactification, e.g., $\beta\mathbb N$, unless you have something stronger than DC.
My guess would be that the existence of an invariant subspace of a polynomially compact operator on Hilbert space cannot be established without a stronger form of choice. Certainly Lomonosov's proof, while simple, uses powerful fixed-point results that most likely rely on AC.