2
$\begingroup$

I am working on the following Künneth-type isomorphism from [SGA5, exposé III, 2,3]:
$\mathrm{Settings}.$ Let $X_1, X_2$ be separated finite type schemes over the spectrum of a field $S=\mathrm{Spec}k$, $E_i, F_i \in \mathrm{D}_{ctf} (X_i)$ be constructible sheaves (with good finiteness conditions). Let $X=X_1 \times_S X_2$, $E=E_1\boxtimes_S E_2$($=pr^*_1 E_1\otimes pr^*_2 E_2$ by definition), $F=F_1\boxtimes_S F_2$.
Then we have a canonical morphism (2.2.4) $$R\mathcal{H}om(E_1,F_1)\boxtimes_S R\mathcal{H}om(E_2,F_2)\rightarrow R\mathcal{H}om(E,F).$$ (for details about this morphism, see SGA5 III (2.2.3))
$\mathrm{Prop.}$ In this case, (2.2.4) is an isomorphism.
In the proof given by Verdier there, we reduce to $E_i={f_i}_! \Lambda$ in the first step, for étale morphisms $f_i: U_i\rightarrow X_i.$
My question is the detail of this reduction.
I think this may from the resolution of an étale constructible sheaf: for any constructible sheaf of $\Lambda$-modules $F$ over $X$, one can find étale morphisms $g_i: U_i\rightarrow X$, such that $$\cdots\rightarrow{g_i}_!\Lambda\rightarrow{g_{i-1}}_!\Lambda\rightarrow\cdots \rightarrow{g_1}_!\Lambda\rightarrow F\rightarrow 0$$ is a resolution. Using this resolution we can apply a long exact sequence argument and induction (for the finiteness of $F$, the resolution is finite). But I am not sure about this.

$\endgroup$

0