A proposition about direct image sheaves Throughout this question I will refer to the last part of Proposition 8.3 of J. Milne's free book Lectures on Etale Cohomology. It has been asserted that given any finite morphism of schemes, say, $f:Y\rightarrow X$, and any sheaf $\mathcal{F}$ on the small etale site $Y_{et}$ of $Y$, given any geometric point $
\bar{x}\rightarrow x\in X$ (to avoid the trivial case assume $x\in \text{Im}f$ of course), the stalk $(f_{*}\mathcal{F})_{\bar{x}}$ (of the direct image sheaf) is given by the direct sum $\bigoplus_{f(y) = x} \mathcal{F}_{\bar{y}}^{d_y}$ where $d_y$ is the degree of separable extension of the corresponding residue field. Could someone please provide a hint as to how one might go about proving this statement? In particular, is the proof "deep" (requires descent etc) or is it too straightforward that the author omitted it but somehow I just do not have an idea how to approach this right now? I am not experienced at working with the etale topology, whence I do apologise in advance if there are any mistakes in this question or if it is too trivial to be posted here. Thanks in advance.
 A: So, the operative fact that you want is the following.

Proposition ([Fu, Proposition 5.3.7]): Let $f:Y\to X$ be a finite morphism of schemes, and let $\overline{x}: \mathrm{Spec}(L)\to $ be a geometric point of
$X$. Then,for any sheaf $\mathcal{F}$ one has a natural bijection
$$(f_\ast\mathcal{F})_{\overline{x}}\to\prod_{\overline{y}} \mathcal{F}_{\overline{y}}$$
(which is an isomorphism of groups if $\mathcal{F}$ is a sheaf of groups).

Check the reference for a more down-to-earth proof, but I would like to tell you what (to me) is the morally correct proof.
Let me denote by $\mathcal{O}_{X,\overline{x}}$ the local ring of $X$ at $\overline{x}$ in the etale topology. Note then that one has a natural fibered diagram
$$\begin{matrix}\bigsqcup_{\overline{y}}\mathrm{Spec}(\mathcal{O}_{Y,\overline{y}}) & \xrightarrow{j} & Y\\ \downarrow& & \downarrow\\ \mathrm{Spec}(\mathcal{O}_{X,\overline{x}}) & \xrightarrow{i} & X\end{matrix}$$
To understand the intuition for this, it's first useful to compare two situations:

*

*$Y\times_X \text{Spec}(\mathcal{O}_{X,x})$ -- the pullbcak to the Zariski local ring.

*$Y\times_X \text{Spec}(\mathcal{O}_{X,\overline{x}})$ -- the pullback to the etale local ring.

It is often the case that the scheme in the first bullet is actually connected and so in particular not isomorphic to $\bigsqcup_y \mathrm{Spec}(\mathcal{O}_{Y,y})$ (e.g. think about the squaring map on $\mathbf{G}_m$ and $x=0$). That said, this latter ring does always split (into the desired product of local rings). At a very broad level one can internalize this as 'the Zariski topology is too coarse to separate points in the fiber, but the etale topology is fine enough'. Slightly more rigorously, $Y\times_X \mathrm{Spec}(\mathcal{O}_{X,\overline{x}})$ is forced to split because $\mathcal{O}_{X,\overline{x}}$ is (strictly) Henselian, and so any finite algebra over it is a product of local algebras (e.g. see [Fu, Proposition 2.8.3]). For a complete proof, see [Fu, Proposition 2.8.20].
Now, note that one has a natural base change map
$$i^{-1}f_\ast\mathcal{F}\to f_\ast j^{-1}\mathcal{F}$$
(e.g. see the beginning of [Fu, §7.3] or Tag 0735). But, and here's the key point, since $f$ is finite this map is actually an isomorphism by the proper base change theorem (see Tag 03AU). But, what happens if compute this map on stalks? Well, on the left hand side we get
$$(i^{-1}f_\ast\mathcal{F})_{\overline{x}}=(f_\ast\mathcal{F})_{i\circ\overline{x}}=(f_\ast\mathcal{F})_{\overline{x}}$$
On the other hand, we need to compute $(f_\ast j^{-1}\mathcal{F})_{\overline{x}}$. Here we use a trick. Recall that the etale site of a strictly Henselian local ring is equivalent to the category of sets by the global section functor. From this, it's not hard to see that
$$(f_\ast j^{-1}\mathcal{F})_{\overline{x}}=(f_\ast j^{-1}\mathcal{F})(\mathrm{Spec}(\mathcal{O}_{X,\overline{x}}))$$
But, by using the above techniques in reverse (and the fact that sheaves commute with disjoint unions) this is equal to
$$\begin{aligned}(j^{-1}\mathcal{F})\left(\bigsqcup_{\overline{y}}\mathrm{Spec}(\mathcal{O}_{Y,\overline{y}})\right) &=\prod_{\overline{y}}(j^{-1}\mathcal{F})(\mathrm{Spec}(\mathcal{O}_{Y,\overline{y}})\\ &= \prod_{\overline{y}}(j^{-1}\mathcal{F})_{\overline{y}}\\ &=\prod_{\overline{y}}\mathcal{F}_{j\circ \overline{y}}\\ &= \prod_{\overline{y}}\mathcal{F}_{\overline{y}}\end{aligned}$$
(where I am conflating $\overline{y}$ and $j\circ\overline{y}$) as desired.
So, in short: this result is somewhat subtle to do correctly, but is a manifestation of the proper base change theorem and the fact that finite algebras over strictly Henselian local rings are products of local rings.
Reference:
[Fu] Fu, L., 2011. Etale cohomology theory (Vol. 13). World Scientific.
