Lemma 106.5.10. If $f: \mathcal{U} \to \mathcal{X}$ is a smooth morphism of locally Noetherian algebraic stacks, and if $u \in |\mathcal{U}|$ with image $x \in |\mathcal{X}|$, then

$\dim _ u (\mathcal{U}) = \dim _ x(\mathcal{X}) + \dim _{u} (\mathcal{U}_ x).$

Proof. Choose a smooth surjective morphism $V \to \mathcal{U}$ whose source is a scheme, and let $v\in |V|$ be a point mapping to $u$. Then the composite $V \to \mathcal{U} \to \mathcal{X}$ is also smooth, and by Lemma 106.5.4 we have $\dim _ x(\mathcal{X}) = \dim _ v(V) - \dim _ v(V_ x),$ while $\dim _ u(\mathcal{U}) = \dim _ v(V) - \dim _ v(V_ u).$ Thus

$\dim _ u(\mathcal{U}) - \dim _ x(\mathcal{X}) = \dim _ v (V_ x) - \dim _ v (V_ u).$

Choose a representative $\mathop{\mathrm{Spec}}k \to \mathcal{X}$ of $x$ and choose a point $v' \in | V \times _{\mathcal{X}} \mathop{\mathrm{Spec}}k|$ lying over $v$, with image $u'$ in $|\mathcal{U}\times _{\mathcal{X}} \mathop{\mathrm{Spec}}k|$; then by definition $\dim _ u(\mathcal{U}_ x) = \dim _{u'}(\mathcal{U}\times _{\mathcal{X}} \mathop{\mathrm{Spec}}k),$ and $\dim _ v(V_ x) = \dim _{v'}(V\times _{\mathcal{X}} \mathop{\mathrm{Spec}}k).$

Now $V\times _{\mathcal{X}} \mathop{\mathrm{Spec}}k \to \mathcal{U}\times _{\mathcal{X}}\mathop{\mathrm{Spec}}k$ is a smooth surjective morphism (being the base-change of such a morphism) whose source is an algebraic space (since $V$ and $\mathop{\mathrm{Spec}}k$ are schemes, and $\mathcal{X}$ is an algebraic stack). Thus, again by definition, we have

\begin{align*} \dim _{u'}(\mathcal{U}\times _{\mathcal{X}} \mathop{\mathrm{Spec}}k) & = \dim _{v'}(V\times _{\mathcal{X}} \mathop{\mathrm{Spec}}k) - \dim _{v'}(V \times _{\mathcal{X}} \mathop{\mathrm{Spec}}k)_{u'}) \\ & = \dim _ v(V_ x) - \dim _{v'}( (V\times _{\mathcal{X}} \mathop{\mathrm{Spec}}k)_{u'}). \end{align*}

Now $V\times _{\mathcal{X}} \mathop{\mathrm{Spec}}k \cong V\times _{\mathcal{U}} (\mathcal{U}\times _{\mathcal{X}} \mathop{\mathrm{Spec}}k),$ and so Lemma 106.5.9 shows that $\dim _{v'}((V\times _{\mathcal{X}} \mathop{\mathrm{Spec}}k)_{u'}) = \dim _ v(V_ u).$ Putting everything together, we find that

$\dim _ u(\mathcal{U}) - \dim _ x(\mathcal{X}) = \dim _ u(\mathcal{U}_ x),$

as required. $\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).