Locally constant functions form a sheaf with constant stalks

${\underset{‾}{A}}_{\mathrm{l}\mathrm{o}\mathrm{c}}$ with the usual restriction maps is a presheaf of sets: the restriction $f{\mathrm{\mid }}_V$ of a locally constant $f:U\to A$ to an open $V\subseteq U$ is locally constant, since a neighbourhood of $y\in V$ on which $f$ is constant is again a neighbourhood of $y$ in $V$ on which $f{\mathrm{\mid }}_V$ is constant; and ${\rho }_U^U=\mathrm{id}$ and ${\rho }_W^U={\rho }_W^V\circ {\rho }_V^U$ hold because both sides are the same function $W\to A$ [F1].

Locality holds: if $f,g\in {\underset{‾}{A}}_{\mathrm{l}\mathrm{o}\mathrm{c}}(U)$ satisfy $f{\mathrm{\mid }}_{U_i}=g{\mathrm{\mid }}_{U_i}$ for every $i$, then given $x\in U$ the cover provides an index $i$ with $x\in U_i$, and $f(x)=f{\mathrm{\mid }}_{U_i}(x)=g{\mathrm{\mid }}_{U_i}(x)=g(x)$; hence $f=g$ as functions.

For $x\in X$ define ${\mathrm{e}\mathrm{v}}_x:{\underset{‾}{A}}_{\mathrm{l}\mathrm{o}\mathrm{c},x}\to A$ by ${\mathrm{e}\mathrm{v}}_x[(U,f)]:=f(x)$, where $[(U,f)]$ denotes the class of a pair. This is well defined: if $(U,f)\sim (V,g)$ then $f$ and $g$ agree on a smaller open neighbourhood $W$ of $x$ [F3], so $f(x)=g(x)$; and it is additive in the sense of respecting the group operations when $A$ is an abelian group, since sums are formed pointwise.

Gluing holds: let $f_i\in {\underset{‾}{A}}_{\mathrm{l}\mathrm{o}\mathrm{c}}(U_i)$ satisfy $f_i{\mathrm{\mid }}_{U_i\cap U_j}=f_j{\mathrm{\mid }}_{U_i\cap U_j}$ for all $i,j$. The union of graphs $f:={\bigcup }_{i\in I}\{(x,f_i(x)):x\in U_i\}\subseteq U\times A$ is a function $U\to A$: it is total because the $U_i$ cover $U$, and it is single-valued because for $(x,a),(x,b)$ in it, say from $i$ and $j$, compatibility gives $a=f_i(x)=f_j(x)=b$. Then $f{\mathrm{\mid }}_{U_i}=f_i$, and $f$ is locally constant: for $x\in U$ pick $i$ with $x\in U_i$ and an open $V\subseteq U_i$ with $x\in V$ on which $f_i$ is constant, so that $f{\mathrm{\mid }}_V=f_i{\mathrm{\mid }}_V$ is constant. No index is selected in the definition of $f$, the graph being described by a formula. By [F2] with [step 1.2] the presheaf ${\underset{‾}{A}}_{\mathrm{l}\mathrm{o}\mathrm{c}}$ is a sheaf of sets, which is clause 1.

${\mathrm{e}\mathrm{v}}_x$ is surjective: for $a\in A$ the constant function $X\to A$ with value $a$ is locally constant, so it is an element of ${\underset{‾}{A}}_{\mathrm{l}\mathrm{o}\mathrm{c}}(X)$ whose class maps to $a$; this uses no selection, the function being given by the formula $y\mapsto a$.

${\mathrm{e}\mathrm{v}}_x$ is injective: suppose ${\mathrm{e}\mathrm{v}}_x[(U,f)]=a={\mathrm{e}\mathrm{v}}_x[(V,g)]$. By local constancy there are open neighbourhoods $U^{\mathrm{\prime }}\subseteq U$ and $V^{\mathrm{\prime }}\subseteq V$ of $x$ with $f{\mathrm{\mid }}_{U^{\mathrm{\prime }}}$ and $g{\mathrm{\mid }}_{V^{\mathrm{\prime }}}$ constant, necessarily with value $a$ because $f(x)=g(x)=a$; on the open neighbourhood $W:=U^{\mathrm{\prime }}\cap V^{\mathrm{\prime }}$ of $x$ the two functions agree, so $(U,f)\sim (V,g)$ by [F3] and the two classes coincide. Hence ${\mathrm{e}\mathrm{v}}_x$ is a bijection for every $x\in X$, which is clause 2.

Suppose now that $A$ is an abelian group. Pointwise addition makes every ${\underset{‾}{A}}_{\mathrm{l}\mathrm{o}\mathrm{c}}(U)$ an abelian group, with the empty function as the zero element over $U=\mathrm{\varnothing }$ and the constant function with value $0$ as the zero element over $U\mathrm{\ne }\mathrm{\varnothing }$; the sum and the negative of locally constant functions are locally constant, because on the intersection of neighbourhoods on which the two functions are constant the sum is constant, and the negative is constant wherever the function is; and each restriction map ${\rho }_V^U$ is a group homomorphism because $(f+g){\mathrm{\mid }}_V=f{\mathrm{\mid }}_V+g{\mathrm{\mid }}_V$ and $(-f){\mathrm{\mid }}_V=-(f{\mathrm{\mid }}_V)$ hold pointwise. By [step 2.1] the underlying set-valued presheaf is a sheaf, so by [F5] ${\underset{‾}{A}}_{\mathrm{l}\mathrm{o}\mathrm{c}}$ is a sheaf of groups, abelian since addition is pointwise abelian, that is a sheaf of abelian groups, and the category of these is abelian by [F6]. Finally the assignment $a\mapsto (x\mapsto a)$ is a group homomorphism $A\to {\underset{‾}{A}}_{\mathrm{l}\mathrm{o}\mathrm{c}}(U)$ for every open $U$, since $(x\mapsto a)+(x\mapsto b)=(x\mapsto a+b)$ pointwise and over $U=\mathrm{\varnothing }$ it is the zero homomorphism to the trivial group. This is clause 3, and the proof is complete. ∎