Is Zorn's lemma required to prove the existence of a maximal atlas on a manifold? In the definition of smooth manifolds, complex manifolds, and similar constructions, one starts by defining a property on neighborhoods in the space, specifying how they relate on overlapping neighborhoods. An atlas is a set of such neighborhoods that covers the space. Some books (Lee, Warner) define the structure as the maximal atlas. Others define it as the equivalence class of compatible atlases.
I was under the impression that the advantage of using the equivalence class definition instead of the maximal atlas definition was that the proof of the existence of such a maximal atlas requires Zorn's lemma, which some prefer not to use if not absolutely necessary.
But Lee and Warner's books both contain existence proofs for this maximal atlas; they start with any atlas, and then just take the set of all compatible charts. If that argument somehow relies on Zorn's lemma (or some other variant of choice), I can't see how. So what do you say? Is choice required, assumed for convenience but not required, or just not necessary at all?
 A: Zorn's lemma is not required to prove the existence of a maximal atlas, though it is convenient. For one thing, we don't have to prove that compatibility of atlases is an equivalence relation. On the other hand, the obvious proof using Zorn's lemma requires some extra work to show that there is a unique maximal atlas containing any atlas. So let's do it without Zorn's lemma.
Definition. Two atlases on a manifold are compatible if their union is an atlas.
Lemma. Compatibility of atlases is an equivalence relation.
Proof. It is clear that compatibility is symmetric and reflexive, and it remains to be shown that compatibility is transitive. Let $\mathcal{A}_1, \mathcal{A}_2, \mathcal{A}_3$ be three atlases on a $k$-manifold $M$, and suppose $\mathcal{A}_1 \cup \mathcal{A}_2$ and $\mathcal{A}_2 \cup \mathcal{A}_3$ are atlases. We wish to show $\mathcal{A}_1 \cup \mathcal{A}_3$ is an atlas. So let $\varphi_1 : U_1 \to \mathbb{R}^k$ be a chart in $\mathcal{A}_1$, $\varphi_3 : U_3 \to \mathbb{R}^k$ be a chart in $\mathcal{A}_3$. $\mathcal{A}_2$ is an atlas, so for each point $x$ in $U_1 \cap U_3$ there is a chart $\varphi_2 : U_2 \to \mathbb{R}^k$ in $\mathcal{A}_2$ such that $x \in U_2$; but $\varphi_1$ and $\varphi_2$ are compatible and $\varphi_2$ and $\varphi_3$ are compatible so we see that $\varphi_1$ and $\varphi_3$ are locally compatible at $x$. (Here, ‘compatible’ means that the transition map satisfies the relevant regularity condition. There may well be invocations of the axiom of choice hidden here, but I will assume that there are not.) Moreover, $x$ is arbitrary in $U_1 \cap U_3$ so this shows $\varphi_1$ and $\varphi_3$ are compatible; and $\varphi_1$ and $\varphi_3$ are also arbitrary, so $\mathcal{A}_1 \cup \mathcal{A}_3$ is an atlas.
Lemma. The class of atlases on a manifold is a set.
Proof. The class of atlases is a subclass of the set
$$\mathscr{P} \left( \bigcup_{U \in \mathscr{P}(M)} \{ U \to \mathbb{R}^k \} \right)$$
where $\{ U \to \mathbb{R}^k \}$ denotes the set of all functions $U \to \mathbb{R}^k$, so by the axiom of separation,  the class of atlases is a set.
Lemma. The union of arbitrarily many pairwise compatible atlases is an atlas.
Proof. Immediate.
Theorem. Every atlas is contained in a unique maximal atlas.
Proof. From the above, it is clear that every atlas $\mathcal{A}$ is contained in some equivalence class of atlases, and this equivalence class is a set of compatible atlases. Let $\overline{\mathcal{A}}$ be the union of all those atlases. Then $\mathcal{A} \subseteq \overline{\mathcal{A}}$, and $\overline{\mathcal{A}}$ is the unique maximal atlas containing $\mathcal{A}$: for if $\mathcal{A} \subseteq \mathcal{A}'$, then $\mathcal{A}$ and $\mathcal{A}'$ are compatible, so $\mathcal{A}' \subseteq \overline{\mathcal{A}}$ by construction.

For the sake of completeness I sketch a proof using Zorn's lemma.
Theorem. Every atlas is contained in a maximal atlas.
Proof. The set of all atlases containing $\mathcal{A}$ partially ordered by inclusion is a chain-complete poset: indeed, it is clear that if we have a chain $\{ \mathcal{A}_\alpha \}$, then $\bigcup_\alpha \mathcal{A}_\alpha$ is also an atlas. Thus, the hypotheses of Zorn's lemma are satisfied and there is some maximal atlas containing $\mathcal{A}$.
