Categories internal to schemes and subschemes of invertible arrows Let  $X = (X_1 \rightrightarrows X_0)$ be a category in schemes, such that the source and target maps are both smooth. By an argument using finite limits we can construct a subscheme $X_1^{iso} \subset X_1$ such that  $X^{iso} = (X_1^{iso} \rightrightarrows X_0)$ is a groupoid in schemes, and this is universal in the sense that any internal functor $Y\to X$ from a groupoid $Y$ factors (strictly!) through $X^{iso}$.
My question is, can we show that the source and target maps of $X^{iso}$, which are composites $X_1^{iso} \hookrightarrow X_1 \to X_0$, are also smooth? If the inclusion of the scheme of invertible arrows was an open immersion I think we would be done.
I would also be happy if the proof only went through for algebraic spaces instead of schemes (this might be easier, who knows!).
This is a vast generalisation of the question I asked at M.SE a while back, which dealt with the case that the category $X$ was a monoid. User 'Matt E' showed it was true for the case that the monoid was smooth and of finite type over a field.
 A: The answer to your question is "yes".  We need the following properties of $X_1^{iso}$:


*

*The map $X_1^{iso} \to X_1$ given by $(f,g) \mapsto f$ on scheme-valued points is a monomorphism.  This is straightforward from uniqueness of inverses.

*$s,t: X_1 \to X_0$ are formally smooth.  We use this for existence of a lift of an infinitesimal deformation.

*$s,t: X_1 \to X_0$ are locally of finite presentation.  Using basic permanence properties (see e.g., Stacks 02KL with $X=S=X_1$ and $Y = X_0$), we find that $i: X_0 \to X_1$ is also locally of finite presentation.  Combining with the fiber product construction, the two maps from $X_1^{iso}$ to $X_0$ are also lfp.

*Infinitesimal formal categories are formal groupoids.  This is basically the statement that tangent spaces have abelian group structure.
We will show that the monomorphism $X_1^{iso} \to X_1$ is formally étale by rephrasing Matt E's argument in a bit more generality.  
Let $j: U \to T$ be a closed immersion of affine schemes over $X_0$ defined by a square zero ideal $I$.  Let $\bar{f}$ be a $U$-point of $X_1^{iso}$, and let $f$ be a $T$-point of $X_1$, such that $f \circ j$ is equal to $\bar{f}$ followed by the monomorphism.  By assumption, $\bar{f}$ has an inverse $\bar{g}$, and by formal smoothness of both $s,t: X_1 \to X_0$, there exists some $T$-point $\tilde{g}$ of $X_1$ that restricts to the $U$-point $\bar{g}$.
We now translate by $\tilde{g}$ to bring us to an infinitesimal neighborhood of the origin.  $\bar{g}$ and $\bar{f}$ are inverses as $U$-points, so $\tilde{g} f$ and $f \tilde{g}$ are $T$-points whose restriction to $U$ factors through identity.  The square zero condition on $I$ gives an additive bijection between lifts of the identity and elements of $\operatorname{Hom}_{\mathcal{O}_U}(e_U^*\Omega_{X_1/X_0},I)$, where $e_U: U \to X_1$ is the identity section (SGAI Exp. 3 Proposition 5.1).  Because the Hom space is an abelian group, we can easily form inverses by negating.  Translating back yields $(\tilde{g} f)^{-1} \tilde{g} = \tilde{g} (f \tilde{g})^{-1}$ as the unique inverse of $f$.
To summarize, if $f$ is a $T$-point in $X_1$ whose restriction to $U$ factors through $X_1^{iso}$, then there is a unique $T$-point $(f,f^{-1})$ in $X_1^{iso}$ that maps to $f$.  Thus, $X_1^{iso} \to X_1$ is formally étale, and the composition with either source or target $X_1 \to X_0$ is formally smooth and locally of finite presentation, hence smooth.
This argument works for algebraic spaces without change (although you may need to find new references).
A: I claim that the answer to your question is "yes" if $X_1$ is separated and umramified over our base scheme $S$. I'm not saying that that this (strong?) assumption is essential. It is just precisely what one needs in my easy proof:
First we have to define $X_1^{iso}$. Consider the fiber product $X_1 \times_{X_0 \times_S X_0} X_1$ with respect to $(t,s) : X_1 \to X_0 \times_S X_0$ and $X_0 \times_S X_0 \leftarrow X_1 : (s,t)$. Intuitively (and this holds verbatim in the functorial picture), it consists of morphisms $(f,g)$ such that we can compose $f \circ g$ and $g \circ f$. Define a morphism $\alpha : X_1 \times_{X_0 \times X_0} X_1 \to X_1 \times X_1 \times X_1 \times X_1$ by $\alpha(f,g)=(i(s(f)),i(s(g)),m(f,g),m(g,f))$, where $i : X_0 \to X_1$ is the unit and $m : X_1 \times_{t,X_0,s} X_1 \to X_1$ is the composition. Besides, we have the diagonal $\Delta_{X_1 \times X_1}$ mapping $(a,b) \mapsto (a,b,a,b)$. Then we define $X_1^{iso}$ by the cartesian square
$$\begin{matrix} X_1^{iso} & \rightarrow & X_1 \times X_1 \\\\ \downarrow j & & ~~ \downarrow\Delta_{X_1 \times X_1} \\\\ X_1 \times_{X_0 \times X_0} X_1 & \xrightarrow{\alpha} & X_1 \times X_1 \times X_1 \times X_1 \end{matrix}$$
Then $X_1^{iso}$ consists of pairs of morphisms $(f,g)$ such that $f \circ g$ and $g \circ f$ are well-defined and equal the identity. The map $X_1^{iso} \to X_1$ is defined as the composition
$$X_1^{iso} \xrightarrow{j} X_1 \times_{X_0 \times X_0} X_1 \xrightarrow{\mathrm{pr_1}} X_1.$$
In general, this is a locally closed immersion. Now $X_1$ is separated, hence the same is true for $X_1 \times X_1$ and its diagonal is a closed immersion. Hence, $j$ is a closed immersion. Now, if I am not mistaken, in general $\Delta_X$ is formally smooth iff $X$ is formally unramified, and $\Delta_X$ is of finite presentation when $X$ is of finite presentation. Hence, by our assumption, $j$ is even smooth. And $\mathrm{pr}_1$ is some base change of the morphism $(s,t) : X_1 \to X_0 \times X_0$, which is smooth since it is the smooth diagonal $\Delta_{X_1}$ followed by the smooth morphism $s \times t : X_1 \times X_1 \to X_0 \times X_0$.
This shows that $X_1^{iso} \to X_1$ is smooth. In particular, the compositions $s,t : X_1^{iso} \to X_1 \rightrightarrows X_0$ are smooth.
