It is a [known theorem](http://books.google.com.au/books?id=87vtu4HbdawC&lpg=PA114&ots=VtyWCoKPHj&dq=local%20bisections%20lie%20groupoid&pg=PA129#v=onepage&q&f=false) that an internal equivalence of Lie groupoids (finite dimensional manifolds!) - that is an equivalence in the 2-category of Lie groupoids, smooth functors and transformations - is a weak equivalence: a fully faithful essentially surjective functor. Here we say a functor is essentially surjective is the map expressing this fact is not only surjective but a surjective *submersion*.


I'm interesting an analogues of this fact for *Frechet* Lie groupoids - groupoids internal to the category of Frechet manifolds, where the source and target are submersions of Frechet manifolds (this is stronger than surjective on tangent spaces - need local charts where the map looks like projection out of a direct sum).


The proof for Lie groupoids relies on the fact that Lie groupoids admit local bisections through every arrow $g$. These are maps $X\_0 \supset U \stackrel{f}{\to} X\_1$ where $s(g) \in U$, an open subset of $X\_0$ such that $f(s(g)) = g$, and $t\circ f:U \to X\_0$ is an open embedding. So far so good, the existence of local bisections depends on the characterisation of a submersion as locally a projection out of a direct sum, but with a small twist, which I haven't thought about, but don't expect to cause trouble.


The problem is showing that the 'surjective implies submersion' part of the proof, which [uses](http://books.google.com.au/books?id=87vtu4HbdawC&lpg=PA114&ots=VtyWCoKPHj&dq=local%20bisections%20lie%20groupoid&pg=PA129#v=onepage&q&f=false) a different characterisation of submersions of finite-dimensional manifolds, namely that admit local sections through every point in their codomain. This is false in the general Frechet case, but it doesn't mean the proof couldn't be rewritten to use the other characterisation of submersions (locally a projection).


My question is: has this been done?



Internal equivalence implies weak equivalence for Frechet Lie groupoids?
There is a characterisation of weak equivalences which works in internal categories in a) finitely complete categories and b) finite-dimensional Lie groupoids (and in fact Lie categories). In the case of Lie groupoids, an internal functor $f\colon X\to Y$ is a weak equivalence in the sense of being fully faithful and essentially surjective (as mentioned in the question) if and only if there is a fully faithful functor $j\colon Y'\to Y$ with object component a surjective submersion, a functor $s\colon Y' \to X$ and a natural isomorphism $j\simeq f\circ s$. This latter property one might call locally weakly split.


An internal equivalence gives an example of a locally weakly split functor, with $j=id$, for groupoids or categories internal to any sort of category (with a notion of covers, to make sense of essential surjectivity and the analogue of the functor $j$). One only really needs the property of being locally weakly split in order to talk about localisations of 2-categories of internal groupoids to 2-categories of presentable stacks. I don't mention it, but that is the motivation in my [recent paper](http://dx.doi.org/10.1007/s10485-015-9400-4).


