I am currently teaching a topics course where I talk about some discrete groups acting properly. A student asked a very basic question that stumped me: what is the precise relationship between proper discontinuity and existence of a fundamental domain? Namely, let $G$ be a discrete group acting on a topological space $X$. Recall that the action is *properly discontinuous* if for every compact subset $K \subset X$, the set
$$\{g \in G | gK \cap K \neq \emptyset \}$$
is finite. A *fundamental domain* is a subset $U \subset X$ such that its images by all elements of $G$ are disjoint and cover $X$ (possibly up to some "thin" set, e.g. the boundary of $U$).

Is there any theorem saying that the action is proper if and only if there exists a "sufficiently nice" fundamental domain on $X$, possibly with some additional conditions?

This seems to be taken for granted by everyone, and I often used it as an explanation of what a "properly discontinuous action" means intuitively. But to my extreme surprise, a search for precise references brought up almost nothing. I only found one statement of this sort: Theorem 3.6 in T. Drumm and V. Charette, "Complete Lorentzian 3-manifolds" (in Contemporary Mathematics, vol. 639 "Geometry, Groups and Dynamics", pp. 43--72). This statement seems to be actually wrong, as the well-known counterexample of the cyclic group generated by $\left( \begin{smallmatrix} 2 & 0 \\ 0 & 1/2 \end{smallmatrix} \right)$ acting on a closed quadrant (or on $\mathbb{R}^2 \setminus \{0\}$) seems to contradict it (unless I missed some additional assumptions they made somewhere).

Possible restrictions needed to make it work:

- Clearly we need to impose some regularity condition on $U$, to prevent people from just picking a point in every orbit at random and pretending that the resulting mess is a fundamental domain. One that is often used is being
*regular*in the topological sense, i.e. open with $\overset{\circ}{\overline{U}} = U$, or (which is closely related) closed with $\overline{\overset{\circ}{U}} = U$. - We need a local finiteness condition (e.g. every compact set meets only finitely many tiles), to exclude the counterexample above.
- Points with nontrivial stabilizers are annoying, as pointed out in the comments. We must either restrict our attention to free actions, or modify the definitions somehow. (It would still be nice to be able to deal with orbifolds.)
- Maybe things are simpler for groups acting on smooth manifolds by diffeomorphisms? Or if we have some sort of measure? Or something else?

I tried to think a little about this on my own. The "if" part seems more or less doable by hand. For the "only if" part however, I don't really know how to proceed. There is indeed a well-known theorem that says that if you have a proper action, then you have a nice (Hausdorff) quotient. But then you would have to somehow prove that by "cutting open" this quotient in a suitable way, you can flatten it and lift it to a fundamental domain - which seems really hard to do in general. Case in point: there is one example of proper actions from my field (namely the Margulis spacetimes - see for example "Properly Discontinuous Groups of Affine Transformations: A Survey" by H. Abels) which was found in 1983, but the description of the fundamental domain (the "crooked planes" construction) was not done until 1992.