Abstract definition of properly discontinuous action A discrete group $G$ acts properly discontinuously on a manifold $M$ if the set $\{g\in G\mid gK\cap K\neq \emptyset \}$ is finite for every compact $K\subset M$.
Is there a more abstract characterisation of this property?
I am looking for something that looks like a diagram, a functor or anything vaguely related (to homological algebra, category theory). I have had a look at the relevant pages on nlab, but, although there is a description for a proper map of schemes, I can't think of any formal way of characterising a proper map of topological spaces.
EDIT: I think my question was somewhat imprecise. (Apologies.)
How can the concept of a proper action be defined for group objects in an arbitrary category $\mathcal C$ such that it reduces to a proper action of a Lie group in the category of smooth manifolds and a properly discontinuous action of a group (object) in the category of sets?
And, what are the conditions on the category $\mathcal C$ for such a definition to make sense?
 A: (This answer started out as a comment, but got too long, and perhaps there is something that may be gleaned that will help the OP)
The problem with this question for me is that you are assuming that such a thing can be done with just an abstract category. This is not possible. The data involved is not just a category but at least a pair of categories $D$, $C$ with a fully faithful inclusion $D\to C$ and a class of maps $E$ in $C$ that 'behave like proper maps'. Then one can specialise to the case of $D = Set$, $C = Mfld$ and $E =$ proper maps. 
If you are working in a category where the objects behave like spaces (e.g. an extensive category), then perhaps some ideas can be brought over. For instance, there is a definition of a compact object in a category, but this doesn't agree with the usual definition of compact for the category of topological spaces (whether it does for manifolds is an interesting question that Urs Schreiber is trying to answer at present, at least in the setting of manifolds embedded in $Sh(Mfld)$). One could try to define a proper map in a finitely complete category as a map $f:A \to B$ such that $f^*:CptSub(B) \to CptSub(A)$ preserves compact objects (here $CptSub(A)$ is the subset of the set of subobjects consisting of the compact objects), but I don't know if this class of maps satisfies the conditions that would make it 'behave like proper maps' - it depends on how you define this.
The real question for you is why do you want to do this? What categories are you thinking of applying this abstract description to? If some sorts of categories of spaces, like schemes, algebraic spaces, generalised topological spaces of various sorts, generalised manifolds of various sorts, or even toposes, then there are probably already definitions that will achieve what you want. If you really are set on using an arbitrary category, or using categories of things which aren't like spaces (e.g. an abelian category), then it is hard to see what you are trying to achieve.
I hope this helps.
