The Stacks project

Proof. The limit, if it exists, represents the functor that associates to an object $T$ the set

In fact we will show this functor is isomorphic to the one displayed in the lemma. The map in one direction is given by the rule

This satisfies the conditions of the lemma because

by the relations we recalled above the lemma. To construct a map in the other direction we have to associate to a system $(f_0, \ldots , f_{n + 1})$ as in the displayed formula of the lemma a system of maps $f_\alpha$. Let $\alpha : [k] \to [n + 1]$ be given. Since $k \leq n$ the map $\alpha$ is not surjective. Hence we can write $\alpha = \delta ^{n + 1}_ i \circ \psi$ for some $0 \leq i \leq n + 1$ and some $\psi : [k] \to [n]$. We have no choice but to define

Of course we have to check that this is independent of the choice of the pair $(i, \psi )$. First, observe that given $i$ there is a unique $\psi$ which works. Second, suppose that $(j, \phi )$ is another pair. Then $i \not= j$ and we may assume $i < j$. Since both $i, j$ are not in the image of $\alpha$ we may actually write $\alpha = \delta ^{n + 1}_{i, j} \circ \xi$ and then we see that $\psi = \delta ^ n_{j - 1} \circ \xi$ and $\phi = \delta ^ n_ i \circ \xi$. Thus

as desired. We still have to verify that the maps $f_\alpha$ so defined satisfy the rules of a system of maps $(f_\alpha )_\alpha$. To see this suppose that $\psi : [k'] \to [k]$, $\alpha : [k] \to [n + 1]$ with $k, k' \leq n$. Set $\alpha ' = \alpha \circ \psi$. Choose $i$ not in the image of $\alpha$. Then clearly $i$ is not in the image of $\alpha '$ also. Write $\alpha = \delta ^{n + 1}_ i \circ \phi$ (we cannot use the letter $\psi$ here because we've already used it). Then obviously $\alpha ' = \delta ^{n + 1}_ i \circ \phi \circ \psi$. By construction above we then have

as desired. We leave to the reader the pleasant task of verifying that our constructions are mutually inverse bijections, and are functorial in $T$. $\square$