Quotient manifold by a closed Lie subgroup

By [A1], put $\mathfrak{g}=T_{e}G$ and $\mathfrak{h}=T_{e}H$. By [F1], choose a linear projection of $\mathfrak{g}$ onto $\mathfrak{h}$ and put $\mathfrak{m}$ equal to its kernel, so $\mathfrak{g}=\mathfrak{m}\oplus \mathfrak{h}$.

Give $G\mathrm{/}H$ the quotient topology. The map $q$ is open, since $q^{-1}(q(O))=OH={\bigcup }_{h\in H}Oh$ for every open $O\subseteq G$. It is Hausdorff: the orbit relation $R=\{(g_1,g_2):g_1^{-1}{g}_2\in H\}$ is closed, and for two inequivalent points choose a product neighborhood $O_1\times O_2$ disjoint from $R$; the open sets $q(O_1)$ and $q(O_2)$ are then disjoint. Images of a countable basis of $G$ form a countable basis of $G\mathrm{/}H$.

Define $\mathrm{\Psi }:\mathfrak{m}\times H\to G$ by $\mathrm{\Psi }(X,h)=\exp (X)h$. By [F3], its differential at $(0,e)$ is $(X,Y)\mapsto X+Y$, an isomorphism by step 1.1. By [F2], after restricting to neighborhoods $W\subseteq \mathfrak{m}$ and $V\subseteq H$, $\mathrm{\Psi }$ is a diffeomorphism $W\times V\to U$, where $U$ is an identity neighborhood.

Shrink $W$ and $U$ so that if $X,Y\in W$ and $\exp (X{)}^{-1}\exp (Y)\in H$, then this element lies in $V$. This is possible by continuity at $(0,0)$. Uniqueness in the product chart then gives $X=Y$. Hence $S=\exp (W)$ meets each left coset represented in $U$ exactly once. Also $q(U)=q(S)$, because $\mathrm{\Psi }(X,h)H=\exp (X)H$.

The bijection $q{\mathrm{\mid }}_S:S\to q(U)$ from step 3.1 is a homeomorphism. Indeed, $q{\mathrm{\mid }}_S$ is continuous. If $A=\exp (B)\subseteq S$ is open, with $B\subseteq W$ open, then $\mathrm{\Psi }(B\times V)$ is open in $G$ and has quotient image exactly $q(A)$; openness of $q$ from step 1.2 makes $q(A)$ open. Thus $X\mapsto \exp (X)H$ is a chart from $W$ onto $q(U)$. In this chart and the product chart of step 2.1, $q$ is $(X,h)\mapsto X$.

Translate this chart: for $g\in G$, use $gS$ over $q(gU)$. Fix a coset in $q(gU)\cap q(g^{\mathrm{\prime }}U)$, represented in the first chart by $z=g\exp (X_0)$. Since its coset is also represented in $g^{\mathrm{\prime }}U$, there is $h_0\in H$ with $z{h}_0\in g^{\mathrm{\prime }}U$. The set $g^{\mathrm{\prime }}U$ is open, so for $X$ in a neighbourhood of $X_0$ inside the first chart, $g\exp (X)h_0\in g^{\mathrm{\prime }}U$. Apply the inverse of the translated product diffeomorphism $g^{\mathrm{\prime }}\mathrm{\Psi }:W\times V\to g^{\mathrm{\prime }}U$ to this smooth representative and take its $\mathfrak{m}$-component. Right multiplication by the fixed $h_0$ does not change the coset, so this component is exactly the second-chart coordinate of $q(g\exp X)$. It is smooth near $X_0$; reversing the roles of $g,g^{\mathrm{\prime }}$ proves the reverse transition smooth. These charts therefore form a smooth atlas. By step 4.1, $q$ is locally a projection and hence a surjective submersion of rank $\dim \mathfrak{m}$. Thus $\dim (G\mathrm{/}H)=\dim \mathfrak{m}=\dim G-\dim H$.

The action map $a:G\times G\mathrm{/}H\to G\mathrm{/}H$ is smooth. Near any $(g_0,x_0)$, choose a local smooth section $s$ of $q$ around $x_0$ from step 5.1. There $a(g,x)=q(gs(x))$, a composite of smooth maps. This expression is independent of the lift because $q(gsh)=q(gs)$.

Suppose another smooth structure with the same quotient topology makes $q$ a surjective submersion. By [F5], that submersion and the constructed one have smooth local sections. On a neighborhood carrying a section $s$ of the constructed quotient, the identity from the constructed quotient to the other one is $q_{\mathrm{o}\mathrm{t}\mathrm{h}\mathrm{e}\mathrm{r}}\circ s$; using a section $s^{\mathrm{\prime }}$ of the other quotient gives $q_{\mathrm{c}\mathrm{o}\mathrm{n}\mathrm{s}\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{c}\mathrm{t}\mathrm{e}\mathrm{d}}\circ s^{\mathrm{\prime }}$ in the reverse direction. Hence the identity is a diffeomorphism, proving uniqueness. If $H=G$ the quotient is a point; if $H=\{e\}$ the construction recovers $G$. Disconnected and zero-dimensional groups are included. Countable choice is used through [A1] and [F3]. The finite-dimensional projection, inverse-function, quotient-topology, and constant-rank arguments add no choice.