Free proper action quotient manifold

The map $q$ is open: if $O\subseteq M$ is open, then $q^{-1}(q(O))={\bigcup }_{g\in G}g\cdot O$ is open, so $q(O)$ is open by the quotient topology. It is a continuous surjection by definition and hence also satisfies [F2].

The orbit relation $R=\{(g\cdot x,x):g\in G,x\in M\}$ is closed in $M\times M$. To see this without a sequential choice argument, first note that the proper map $\mathrm{\Theta }:G\times M\to M\times M$ is closed. If $C\subseteq G\times M$ is closed and $z\mathrm{\notin }\mathrm{\Theta }(C)$, local compactness gives an open neighborhood $V$ of $z$ inside a compact set $K$. Then $C\cap {\mathrm{\Theta }}^{-1}(K)$ is compact, so its image $A$ is compact and hence closed by [F4]. The open set $V\setminus A$ contains $z$ and misses $\mathrm{\Theta }(C)$, because every point of $V$ lies in $K$. Thus $\mathrm{\Theta }(C)$ is closed. Taking $C=G\times M$ gives that $R$ is closed.

Distinct orbits have representatives $x,y$ with $(x,y)\mathrm{\notin }R$. By step 1.2 and the product topology, there are neighborhoods $U\ni x$ and $V\ni y$ with $(U\times V)\cap R=\mathrm{\varnothing }$. The open sets $q(U)$ and $q(V)$ from step 1.1 are disjoint: a common orbit would contain some $u\in U$ and $v\in V$, putting $(u,v)$ in $R$. Hence $M\mathrm{/}G$ is Hausdorff.

If $\{B_j:j\in \mathbb{N}\}$ is a countable base of $M$, then $\{q(B_j):j\in \mathbb{N}\}$ is a countable base of $M\mathrm{/}G$. Indeed, for open $W\subseteq M\mathrm{/}G$ and $q(x)\in W$, choose $B_j$ with $x\in B_j\subseteq q^{-1}(W)$; then $q(x)\in q(B_j)\subseteq W$, and $q(B_j)$ is open by step 1.1. Thus the quotient is second countable.

Let $S$ be a slice from [F1] and put $O=G\cdot S$. The restriction $q{\mathrm{\mid }}_S:S\to q(O)$ is bijective. It is a homeomorphism: it is continuous, while for open $W\subseteq S$ the saturation $G\cdot W$ corresponds under the diffeomorphism $G\times S\to O$ to $G\times W$, so it is open and $q(W)$ is open by step 1.1. These homeomorphisms give $M\mathrm{/}G$ local Euclidean charts modelled on $S$, whose dimension is $\dim M-\dim G$ by the product diffeomorphism in [F1].

The slice charts are smoothly compatible. Near a point in the overlap of slices $S$ and $T$, use the diffeomorphism $G\times T\to G\cdot T$ from [F1]. Its $T$-component, restricted to a neighborhood in $S$, is exactly the transition map $(q{\mathrm{\mid }}_T{)}^{-1}\circ q{\mathrm{\mid }}_S$, and is smooth. They therefore define a smooth atlas. In the corresponding product coordinates $G\times S$ on $M$ and slice coordinates $S$ on $M\mathrm{/}G$, the map $q$ is $(g,s)\mapsto s$, so it is a smooth surjective submersion.

Finally suppose two smooth structures on the same orbit space make $q$ a smooth submersion. By [F5], relative to the first structure $q$ has a smooth local section $s$ near every quotient point. The identity from the first quotient manifold to the second is locally $q_2\circ s$, hence smooth; reversing the two structures proves that its inverse is smooth. Thus the structures coincide. Steps 2.1–3.1 prove existence, Hausdorffness, second countability, dimension, and submersivity, and this step proves uniqueness. Only finite local selections occur, so no choice principle is used.