Free actions and double coset manifolds Double coset spaces are often manifolds. For example, locally symmetric spaces and more generally Clifford-Klein space forms. A familiar family of examples are the surfaces of genus $ g $
$$
\Gamma_g \backslash SL_2(\mathbb{R}) / SO_2(\mathbb{R})
$$
where $ \Gamma_g $ is a Fuchsian surface group of genus $ g $. Indeed any compact hyperbolic manifold of any dimension is a double coset space. Another very interesting manifold of a very totally sort which is also a double coset space is the Gromoll-Meyer exotic 7 sphere
$$
Sp(2) \backslash Sp(2) \times Sp(2) / Sp(1) \cong S^7_{exotic}
$$
Let $ G $ be a (compact) Lie group, $ H,K $ closed subgroups.
A sufficient condition for
$$
H\backslash G/K
$$
to be a manifold is that $ H $ acts freely on $ G/K $ (we must in addition assume that the action of $ H $ is properly discontinuous if $ G $ is not assumed compact).
Is this condition also necessary? Is it true that if $ G $ is a compact Lie group, and $ H,K $ are closed subgroups such that $ H \cap K =1 $, then $ H\backslash G/K $ is a manifold if and only if $ H $ acts freely on $ G/K $?
Note: The explicit equivalence relation for this biquotient
$$
G \rightarrow H \backslash G/K
$$
is the relation
$$
g \sim hgk
$$
for all $ h \in H, k \in K $
 A: This is true.  Allow me first to recall some background, and set up notation.
Recall that is a compact Lie group $H$ acts on a manifold $M$, then an orbit $H\cdot p$ for $p\in M$ is called principal if the isotropy group $H_p$ is, up to conjugacy, a subgroup of all other isotropy groups.  The point $p$ is called a regular point.  It's a general fact that such orbits always exist (in fact, they are dense in $M$).
Given an isometric $H$ action on $M$, the slice theorem says that around any orbit $H\cdot p$, there is a neighborhood of the form $U:= H\times_{H_p} V$ where $V:=(T_p H\cdot p)^\bot \subseteq T_p M$, and where $H_p$ acts on $V$ linearly via the differential.  The $H$ action on $U$ is left multiplication, and it is easy to see that $\pi(U) = U/H$ is homeomorphic to $ V/H_p$ (diffeomorphic if $U/H$ is a smooth manifold).
Note that the $H_p$ action on $V$ is isometric, so preserves the spheres of various radii centered at the origin.  It follows that a curve $\gamma(t) = [(e, tv)]$ (where $v\in V$ is arbitrary) gives a tangent vector in $U$ which is non-zero when projected to $V/H_p$ (assume that $\pi:U\rightarrow V/H_p$ is actually smooth.)
We also point out another important fact:  the $H_p$ action on $V$ is trivial iff $H\cdot p$ is a principal orbit.
Proposition:  Suppose a compact Lie group $H$ acts on a smooth manifold $M$ so that $M/H$ has the structure of a smooth manifold for which the natural map $M\rightarrow M/H$ is smooth.  Then all the orbits are principal.
Proof:  By averaging a Riemannian metric, we may assume the action is isometric.  Since being a submersion is a local property, we may assume without loss of generality that $M = U = H\times_{H_p} B$ for some $p\in M$.
Select $h\in H_p$ and $v\in V$ and consider the curve $\gamma(t) = [(e,t( v- hv)]$.  If $v-hv\neq 0$, then $\gamma$ is a radial curve, so by what was said above, its derivative projects to a non-zero tangent vector in $V/H_p$.  On the other hand by definition of $V/H_p$, $\pi(v) = \pi(hv)$, so $\pi\circ \gamma$ is constant, which implies $\gamma'(0)\in \ker d\pi$.  This contradiction can only be avoided if $v-hv = 0$.  That is, $hv = v$.  Since $h\in H_p$ and $v\in V$ were arbitrary, the $H_p$ action on $V$ is trivial, so $p$ is regular. $\square$
Proposition:  If $H,K\subseteq G$ are all compact Lie groups and $H\cap K = \{e\}$, then $H\backslash G/ K$ is a smooth manifold in such a way that $\pi:G\rightarrow H\backslash G/K$ is smooth if and only if the $H$ action on $G/K$ is free.
Proof:  You already know that if the $H$ action is free, then $H\backslash G/K$ is a smooth manifold with $\pi$ smooth.  So let's prove the other direction.
By the previous proposition, the assumption that $G\rightarrow H\backslash G/K$ is smooth implies that, for the $H$ action on $G/K$, that all orbits are principal.  In particular, all the isotropy groups are conjugate.
Now, let's compute the isotropy group $H_{[e]}$ at the identity coset $eK\in G/K$.  Given $h\in H$, we have $heK = K$ if and only $h\in K$.  Since $H\cap K = \{e\}$, $h = e$.  Thus, $H_{[e]} = \{e\}\subseteq H$.
Of course, conjugating the identity gives the identity, so all isotropy groups must be $\{e\}$.  But this is obviously equivalent to the $H$ action being free.  $\square$
