\domainevide{Les cotes de ce thème supposent les correspondances algébriques et une catégorie de motifs, que mathlib ne définit pas.}{12, 162-6}

\begin{encadre}
\begin{theoreme*}[Grothendieck, pages 115 à 119, poids et niveau d'une immersion\piste{12-immersion-level-bound}]\nonverifie
Soient $f : X \to Y$ une immersion de source régulière et $n$ la dimension de l'adhérence de $f(X)$. Les constituants de $R^i f_*\mathbb Q_\ell$ sont de poids $\leq 2\inf(i, n)$ et de niveau $\leq \inf(i, n-1)$. Le dossier tient l'énoncé sous réserve de la résolution, de la pureté et des conjectures de Weil.
\end{theoreme*}
\end{encadre}
{\small Les feuillets en esquissent une démonstration incomplète (pages 115, 117 et 119). Un constituant de poids $w$ est de niveau $\leq \nu$ quand ses valeurs propres de Frobenius sont divisibles par $q^{(w-\nu)/2}$, ou, côté Hodge, quand ses types $(p, q)$ vérifient $p, q \geq (w - \nu)/2$ ; la borne $\inf(i, n-1)$ est inférieure d'une unité au niveau $2n - i$ que permet $H^i$ d'une variété lisse de dimension~$n$ quand $i \geq n$. Les tableaux qui mènent à l'encadré sont écrits vite et surchargés, et l'énoncé repose sur l'encadré seul ; le passage des termes $E_2$ à l'aboutissement (proposition~4.2~a) de la page~112) n'est pas écrit. Les structures de Hodge et les périodes sont l'objet de la partie \q{Théorie de Hodge} (cotes~13 et~18). Mathlib n'a pas les poids des faisceaux $\ell$-adiques. On se reportera aux notes de Grothendieck (\lot{12}{6}{115}).\par}

{\small Sur $\mathbf C$, pour une immersion ouverte $j : X \to Y$, l'édition démontre l'énoncé, sous une forme plus précise, par un argument qui n'est pas sur les feuillets et que Lean ne vérifie pas. Soient $y \notin X$, $\pi : \tilde Y \to Y$ une résolution qui est un isomorphisme au-dessus de $X$, $D = \pi^{-1}(Y - X)$ à croisements normaux simples, $F = \pi^{-1}(y)$ et $F_q = F \cap D^{(q)}$ ; alors $\dim F_0 \leq n - 1$ et $\dim F_q \leq n - q$. La suite spectrale des poids, $E_1 = H^{k-q}(F_q)(-q) \Rightarrow H^k(X \cap B_y)$ (celle de Durfee \cite{durfee1983} quand $(Y - X) \cap B_y = \{y\}$ ; dans le cas général la structure de Hodge mixte vient des modules de Hodge mixtes de Saito \cite{saito1990}, et la forme de la suite spectrale n'est pas vérifiée ici), où $B_y$ est une petite boule autour de $y$, et le théorème~8.2.4 (i), (ii) de Hodge~III \cite{deligne1974} pour les $F_q$ compacts placent les types de Hodge de $(R^i j_*\mathbf Q)_y = H^i(X \cap B_y)$ dans la boîte $p, q \in [\max(0, i - n + 1), \min(i, n)]$. On retrouve les poids de la page, et le niveau est au plus $\min(i, 2n - 1 - i) \leq \min(i, n - 1)$ pour $i \leq 2n - 1$ (au-delà, $H^i$ est nul) ; c'est l'analogue local de 8.2.4 (ii). La majoration des termes $E_2$ des feuillets laisse passer le niveau $n$ en $E_2^{n,0} = H^n(\pi^{-1}(y))$, et c'est la dimension $n - 1$ de la fibre qui l'exclut. La borne est atteinte : le cône sur une variété projective lisse $V$ de dimension $n - 1$ telle que $h^{i,0}(V) \neq 0$ (une surface K3 pour $n = 3$) a le niveau $i$ pour $i \leq n - 1$ et le niveau $n - 1$ en $i = n$ ; pour $n = 2$ et $V$ une courbe de genre $\geq 1$, la fibre de $R^2 j_*$ au sommet est $H^1(V)(-1)$, de poids~$3$ et de niveau~$1$. Cette boîte n'a été trouvée imprimée que pour les singularités isolées, où elle découle de la semi-pureté et de la dualité (Friedman et Laza, théorème~2.6 et définition~2.7 \cite{friedmanlaza}). Pour un morphisme propre de fibres de dimension $d$, le gain d'une unité disparaît : une famille lisse de courbes a déjà un $H^1$ de niveau $1 = d$ ; la version relative que la page esquisse avec $n = d_y(f)$, suivie d'un point d'interrogation, ne peut donc pas garder $n - 1$ si $d_y(f)$ est la dimension de la fibre.\par}