Lemma 106.6.4. Suppose that $\mathcal{X}$ is an algebraic stack, locally of finite type over a locally Noetherian scheme $S$. Let $x_0 : \mathop{\mathrm{Spec}}(k) \to \mathcal{X}$ be a morphism where $k$ is a field of finite type over $S$. Represent $\mathcal{F}_{\mathcal{X}, k, x_0}$ as in Remark 106.2.11 by a cogroupoid $(A, B, s, t, c)$ of Noetherian complete local $S$-algebras with residue field $k$. Then

$\text{the dimension of the local ring of }\mathcal{X}\text{ at }x_0 = 2\dim A - \dim B$

Proof. Let $s \in S$ be the image of $x_0$. If $\mathcal{O}_{S, s}$ is a G-ring (a condition that is almost always satisfied in practice), then we can prove the lemma as follows. By Lemma 106.2.8, we may find a smooth morphism $U \to \mathcal{X}$, whose source is a scheme, containing a point $u_0 \in U$ of residue field $k$, such that induced morphism $\mathop{\mathrm{Spec}}(k) \to U \to \mathcal{X}$ coincides with $x_0$ and such that $A = \mathcal{O}_{U, u_0}^\wedge$. Write $R = U \times _\mathcal {X} U$. Then we may identify $\mathcal{O}_{R, e(u_0)}^\wedge$ with $B$. Hence the equality follows from the definitions.

In the rest of this proof we explain how to prove the lemma in general, but we urge the reader to skip this.

First let us show that the right hand side is independent of the choice of $(A, B, s, t, c)$. Namely, suppose that $(A', B', s', t', c')$ is a second choice. Since $A$ and $A'$ are versal rings to $\mathcal{X}$ at $x_0$, we can choose, after possibly switching $A$ and $A'$, a formally smooth map $A \to A'$ compatible with the given versal formal objects $\xi$ and $\xi '$ over $A$ and $A'$. Recall that $\widehat{\mathcal{C}}_\Lambda$ has coproducts and that these are given by completed tensor product over $\Lambda$, see Formal Deformation Theory, Lemma 89.4.4. Then $B$ prorepresents the functor of isomorphisms between the two pushforwards of $\xi$ to $A \widehat{\otimes }_\Lambda A$. Similarly for $B'$. We conclude that

$B' = B \otimes _{(A \widehat{\otimes }_\Lambda A)} (A' \widehat{\otimes }_\Lambda A')$

It is straightforward to see that

$A \widehat{\otimes }_\Lambda A \longrightarrow A \widehat{\otimes }_\Lambda A' \longrightarrow A' \widehat{\otimes }_\Lambda A'$

is formally smooth of relative dimension equal to $2$ times the relative dimension of the formally smooth map $A \to A'$. (This follows from general principles, but also because in this particular case $A'$ is a power series ring over $A$ in $r$ variables.) Hence $B \to B'$ is formally smooth of relative dimension $2(\dim (A') - \dim (A))$ as desired.

Next, let $l/k$ be a finite extension. let $x_{l, 0} : \mathop{\mathrm{Spec}}(l) \to \mathcal{X}$ be the induced point. We claim that the right hand side of the formula is the same for $x_0$ as it is for $x_{l, 0}$. This can be shown by choosing $A \to A'$ as in Lemma 106.2.5 and arguing exactly as in the preceding paragraph. We omit the details.

Finally, arguing as in the proof of Lemma 106.2.10 we can use the compatibilities in the previous two paragraphs to reduce to the case (discussed in the first paragraph) where $A$ is the complete local ring of $U$ at $u_0$ for some scheme smooth over $\mathcal{X}$ and finite type point $u_0$. Details omitted. $\square$

In your comment you can use Markdown and LaTeX style mathematics (enclose it like $\pi$). A preview option is available if you wish to see how it works out (just click on the eye in the toolbar).