Lemma 106.6.2. Let $\mathcal{X}$ be a locally Noetherian algebraic stack. Let $x \in |\mathcal{X}|$ be a finite type point Morphisms of Stacks, Definition 100.18.2). Let $d \in \mathbf{Z}$. The following are equivalent

1. there exists a scheme $U$, a smooth morphism $U \to \mathcal{X}$, and a finite type point $u \in U$ mapping to $x$ such that $2\dim (\mathcal{O}_{U, \overline{u}}) - \dim (\mathcal{O}_{R, e(\overline{u})}) = d$, and

2. for any scheme $U$, a smooth morphism $U \to \mathcal{X}$, and finite type point $u \in U$ mapping to $x$ we have $2\dim (\mathcal{O}_{U, \overline{u}}) - \dim (\mathcal{O}_{R, e(\overline{u})}) = d$.

Here $R = U \times _\mathcal {X} U$ with projections $s, t : R \to U$ and diagonal $e : U \to R$ and $R_ u$ is the fibre of $s : R \to U$ over $u$.

Proof. Suppose we have two smooth neighbourhoods $(U, u)$ and $(U', u')$ of $x$ with $u$ and $u'$ finite type points. After shrinking $U$ and $U'$ we may assume that $u$ and $u'$ are closed points (by definition of finite type points). Then we choose a surjective étale morphism $W \to U \times _\mathcal {X} U'$. Let $W_ u$ be the fibre of $W \to U$ over $u$ and let $W_{u'}$ be the fibre of $W \to U'$ over $u'$. Since $u$ and $u'$ map to the same point of $|\mathcal{X}|$ we see that $W_ u \cap W_{u'}$ is nonempty. Hence we may choose a closed point $w \in W$ mapping to both $u$ and $u'$. This reduces us to the discussion in the next paragraph.

Assume $(U', u') \to (U, u)$ is a smooth morphism of smooth neightbourhoods of $x$ with $u$ and $u'$ closed points. Goal: prove the invariant defined for $(U, u)$ is the same as the invariant defined for $(U', u')$. To see this observe that $\mathcal{O}_{U, u} \to \mathcal{O}_{U', u'}$ is a flat local homomorphism of Noetherian local rings and hence

$\dim (\mathcal{O}_{U', \overline{u}'}) = \dim (\mathcal{O}_{U, \overline{u}}) + \dim (\mathcal{O}_{U'_ u, \overline{u}'})$

by Algebra, Lemma 10.112.7. (We omit working through all the steps to relate properties of local rings and their strict henselizations, see More on Algebra, Section 15.45). On the other hand we have

$R' = U' \times _{U, t} R \times _{s, U} U'$

Thus we see that

$\dim (\mathcal{O}_{R', e(\overline{u}')}) = \dim (\mathcal{O}_{R, e(\overline{u})}) + \dim (\mathcal{O}_{U'_ u \times _ u U'_ u, (\overline{u}', \overline{u}')})$

To prove the lemma it suffices to show that

$\dim (\mathcal{O}_{U'_ u \times _ u U'_ u, (\overline{u}', \overline{u}')}) = 2\dim (\mathcal{O}_{U'_ u, \overline{u}'})$

Observe that this isn't always true (example: if $U'_ u$ is a curve and $u'$ is the generic point of this curve). However, we know that $u'$ is a closed point of the algebraic space $U'_ u$ locally of finite type over $u$. In this case the equality holds because, first $\dim _{(u', u')}(U'_ u \times _ u U'_ u) = 2\dim _{u'}(U'_ u)$ by Varieties, Lemma 33.20.5 and second the agreement of dimension with dimension of local rings in closed points of locally algebraic schemes, see Varieties, Lemma 33.20.3. We omit the translation of these results for schemes into the language of algebraic spaces. $\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).