I have a Banach manifold $\mathcal{M}$ and I have a Lie group $G$, that is finite dimensional, such that $G$ acts freely on $\mathcal{M}$. I would like to know if $\mathcal{M} / G$ is a Banach manifold as well or not.


I know that this is true if $\mathcal{M}$ is a finite dimensional smooth manifold, and we have the quotient manifold theorem (for example in Lee's book). But I'm struggling to come up with a reference that discussess the infinite dimensional case. Can someone point me to a source that discusses these issues? I looked at Lang's book "Fundamentals of Differential Geometry", but did not find this discussed (assuming I did not miss something).



Quotient by freely acting group on Banach manifold
In finite dimensions, properness of the action is all you need for a slice theorem (and thus for the manifold structure of the quotient). However, in the Banach realm, properness is not enough. For example, the translation action of $c\_0 \subseteq l\_\infty$ of sequences converging to zero on the Banach space $l\_\infty$ of
bounded sequences is proper but $c\_0$ doesn't have a topological complement (which would be the tangent space of the slice).


If I may reference my own work, in [Slice theorem and orbit type stratification in infinite
dimensions](https://arxiv.org/pdf/1812.04698.pdf) we discuss these and other problems in infinite dimensions. Theorem 3.5 gives a general slice theorem (which even holds for manifolds modeled on locally convex spaces, not necessarily Banach ones). It requires four conditions, which in the Banach setting you can verify as follows:


* the stabilizer is a principal Lie subgroup of the acting group: this follows from Theorem IV.3.16. of Neeb's [Towards a Lie theory of locally convex groups](https://link.springer.com/article/10.1007/s11537-006-0606-y). This is stated without proof there and references the still unpublished book by Neeb and Glöckner; I'm sure they will send you their existing manuscript.
* The orbit is a locally closed submanifold: use the inverse function theorem (cf Proposition 3.17 which discusses the way harder case of tame Fréchet manifolds)
* Existence of a local addition and invariant topological metric: if you have a strong invariant Riemann metric, then this should be automatic. If not, you need some other additional structure that provides you a "local linearization" (e.g. equivariantly embed your manifold in a Banach space with a linear action).


I think Bourbaki "Lie groups and Lie algebras" also discusses the Banach case, but I don't have it hand right now to double check.


