Lemma 99.12.1. Let $\mathcal{X}$ be a locally Noetherian algebraic stack over a scheme $S$. Let $x \in |\mathcal{X}|$ be a point of $\mathcal{X}$. Let $[U/R] \to \mathcal{X}$ be a presentation (Algebraic Stacks, Definition 93.16.5) where $U$ is a scheme. Let $u \in U$ be a point that maps to $x$. Let $e : U \to R$ be the “identity” map and let $s : R \to U$ be the “source” map, which is a smooth morphism of algebraic spaces. Let $R_ u$ be the fiber of $s : R \to U$ over $u$. The element

$\dim _ x(\mathcal{X}) = \dim _ u(U) - \dim _{e(u)}(R_ u) \in \mathbf{Z} \cup \infty$

is independent of the choice of presentation and the point $u$ over $x$.

Proof. Since $R \to U$ is smooth, the scheme $R_ u$ is smooth over $\kappa (u)$ and hence has finite dimension. On the other hand, the scheme $U$ is locally Noetherian, but this does not guarantee that $\dim _ u(U)$ is finite. Thus the difference is an element of $\mathbf{Z} \cup \{ \infty \}$.

Let $[U'/R'] \to \mathcal{X}$ and $u' \in U'$ be a second presentation where $U'$ is a scheme and $u'$ maps to $x$. Consider the algebraic space $P = U \times _\mathcal {X} U'$. By Lemma 99.4.3 there exists a $p \in |P|$ mapping to $u$ and $u'$. Since $P \to U$ and $P \to U'$ are smooth we see that $\dim _ p(P) = \dim _ u(U) + \dim _ p(P_ u)$ and $\dim _ p(P) = \dim _{u'}(U') + \dim _ p(P_{u'})$, see Morphisms of Spaces, Lemma 66.37.10. Note that

$R'_{u'} = \mathop{\mathrm{Spec}}(\kappa (u')) \times _\mathcal {X} U' \quad \text{and}\quad P_ u = \mathop{\mathrm{Spec}}(\kappa (u)) \times _\mathcal {X} U'$

Let us represent $p \in |P|$ by a morphism $\mathop{\mathrm{Spec}}(\Omega ) \to P$. Since $p$ maps to both $u$ and $u'$ it induces a $2$-morphism between the compositions $\mathop{\mathrm{Spec}}(\Omega ) \to \mathop{\mathrm{Spec}}(\kappa (u')) \to \mathcal{X}$ and $\mathop{\mathrm{Spec}}(\Omega ) \to \mathop{\mathrm{Spec}}(\kappa (u)) \to \mathcal{X}$ which in turn defines an isomorphism

$\mathop{\mathrm{Spec}}(\Omega ) \times _{\mathop{\mathrm{Spec}}(\kappa (u'))} R'_{u'} \cong \mathop{\mathrm{Spec}}(\Omega ) \times _{\mathop{\mathrm{Spec}}(\kappa (u))} P_ u$

as algebraic spaces over $\mathop{\mathrm{Spec}}(\Omega )$ mapping the $\Omega$-rational point $(1, e'(u'))$ to $(1, p)$ (some details omitted). We conclude that

$\dim _{e'(u')}(R'_{u'}) = \dim _ p(P_ u)$

by Morphisms of Spaces, Lemma 66.34.3. By symmetry we have $\dim _{e(u)}(R_ u) = \dim _ p(P_{u'})$. Putting everything together we obtain the independence of choices. $\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).