Lie quotient of Group by finite group Suppose we had a locally compact group $G$ which had a finite subgroup $K$ with the property that $G/K$ is a Lie group.
Does $G$ inherit the structure of a Lie group from $G/K$ (which would be compatible with its existing topology)?

Edit:  I asked the question very briefly because it is simple to state, but I don't want to give the impression that I haven't thought about this so let me elaborate on my thought process.
It seems that intuitively, if I start with a Lie group, and assume it was the quotient of some locally compact $G$ by a finite normal subgroup $K$, then my original group $G$ would (at least topologically) look like a disjoint union of copies of $G/K$.  A new coordinate chart for $G$ could be formed by making "copies" of the coordinate patches for $G/K$ (one copy for each of the elements of $K$).  It seems as I write this that the answer must be yes but I have yet to work it out fully and would love to have confirmation.
 A: In fact, you do not even need to assume that $G$ is locally compact and $K$ is finite. It suffices to assume that $K$ is discrete, but you do need to assume that $G$ is Hausdorff (and 2nd countable, the latter is automatic if $K$ is finite and $G/K$ is a manifold), otherwise you can take a nontrivial finite group $G$ with the trivial topology and $K=G$. Then $G/K=\{1\}$ is a Lie group (of course), but $G$ is not a Lie group as it is non-Hausdorff. 
As for a proof, note that, in view of discreteness of $K$ in $G$, the quotient map $p: G\to H=G/K$ is a covering map. A covering space of a smooth manifold, $p: X\to M$, has a natural structure of a differentiable manifold making the covering map a local diffeomorphism (local charts from $X$ to $R^n$ will be compositions of local charts on $M$ with the projection $p$). 
Thus, we equip $G$ with the structure of a smooth manifold. It remains to show that group operations are smooth. I will prove this for the product map $m: G\times G\to G$, since the proof for the inversion is similar. Let $m': H\times H\to H$ be the product map. Smoothness is a local property, so consider open subsets $U, V\subset G$ such that $p$ is 1-1 on both, as well as on $W=m(U\times V)$. Since $p: G\to H$ is a homomorphism, we have $p\circ m = m'\circ (p\times p)$, where
$$
p\times p: G\times G\to H\times H. 
$$ 
Therefore, the restriction of $m$ to $U\times V$ can be written as the composition 
$$
p^{-1} \circ m' \circ (p\times p)|U\times V,
$$
where $p^{-1}$ is understood as the inverse to $p: W\to p(W)\subset H$. Since $p^{-1}, p$ and $m'$ are all smooth, so is $m|U\times V$. qed 
