(1) In "Geometrie Microlocale", Verdier states the following theorem.
Theorem: Let $E$ be a vector space and $F$ a constructible complex on $E$. Then for $\ell$ a linear form on $E$, we have a morphism between the fibers at $0$: $$ i_0^*\psi_\ell (F) \longrightarrow i_0^*\psi_\ell(\nu_0(F)) $$ which is an isomorphism for generic $\ell$ (same thing for the vanishing cycles $\phi_\ell$).
Here $\nu_0: D^b_c(E) \to D^b_{mon}(T_0E)$ is Verdier specialization functor to the tangent cone $T_0 E = E$, i.e. the nearby cycles of $p^*F$ along the deformation of to the normal cone $t:D_0 E \to \mathbb{A}^1$.
The theorem says that when computing $\psi_\ell(F)_0$, one can usually suppose $F$ is monodromic.
Verdier doesn't prove the theorem. Instead he just gives an indication of what generic means: consider the blow-up $p:\tilde{E} \to E$ at $0$, take a stratification for which $p^*F$ is constructible and such that $p^{-1}(0)$ is reunion of strata. The condition is that the strict transform of the hyperplane $\{ \ell = 0\}$ should be transverse to the strata contained in $p^{-1}(0)$.
I don't understand how to prove the theorem based on this.
Question 1: Blowing-up a strata to get things transverse in order to compute nearby/vanishing cycles seems not uncommon. Is there some kind of machinery that makes it a standard trick?
(2) Here are my thoughts. We have a triangle $$ F \to e_* e^* F \to \bigoplus_{q=1}^{d-1} i_* i^* F(-q)[-2q] \to +1 $$ The theorem is trivial for $i_* i^* F$ so it is enough to prove that $$ i^* e_* \psi_{\tilde{\ell}} (\tilde{F}) = i^* \psi_\ell (e_* e^* F) \longrightarrow i^* \psi_{d\ell} \nu_0(e_* e^* F) = i^* (Ce)_* \psi_{d\tilde{\ell}} \nu_D (\tilde{F}) $$ is an isomorphism (with $\tilde{F} = e^* F$, $\tilde{l} = l\circ e$). But $\tilde{l}^{-1}(0) = \tilde{H} \cup D$ where $\tilde{H}$ is the strict transform of $H = \{\ell = 0\}$ and $D = e^{-1}(0)$ is the exceptionnal divisor. Outside of $H$, $\tilde{\ell}$ is an equation for $D$ and we always have $\psi_f (F) = \psi_{df} \nu_{f=0}(F)$ (in the topological setting this is proved in Kashiwara-Schapira, I don't know any reference for the étale setting) so $ \psi_{\tilde{\ell}} (\tilde{F}) \to \psi_{d\tilde{\ell}} \nu_D (\tilde{F}) $ is an isomorphism outside of $\tilde{H}\cap D$. The tricky part is
Question 2 How do we prove that
$$
\psi_{\tilde{\ell}}(\tilde{F}) \to \psi_{d\tilde{\ell}}\nu_D (\tilde{F})
$$
is an isomorphism on $\tilde{H}\cap D$, the only hypothesis being that $\tilde{H}$ is transverse to the strata of $D$?
(3) I have (almost) entirely checked that Question 2 cand be answered by using resolution of singularities and proper base change to reduce to the case where $\tilde{F}$ is constructible w/r to the stratification defined a normal crossing divisor, the strict transform of $H$ being one of its components and then using the explicit computation of the nearby cycles in terms of the nearby cycles relative to each component.
But it seems that this line of reasoning is overly convoluted and that there should be a simpler, more natural argument. My main evidence is that stating the computation of nearby cycles in the normal crossing case is already painful. The proof is even worse and it doesn't make things much clearer. Since we don't really need the full computation here, I'd like to avoid it. Plus, the idea that things shouldn't change under specialization if the characteristic directions are separated seems very natural. For example, I think this could be obvious to someone who understands (stratified) Morse theory if I was able to translate it in that topological language.
Question 3 I think Verdier's proof was based on a "standard" dévissage.
Is there a way not to use resolution of singularity and/or explicit computation?
Am I over-optimistic in thinking that there should be a proof as simple as the statement of the theorem?
(4) Any advice or reference (on what you think Verdier's proof is, general techniques of dévissage, the non-characteristic hypotheses etc...) would be truly appreciated. Thanks.
