\domainevide{Les cotes de ce thème supposent le site étale d'un schéma et sa cohomologie, que mathlib ne contient pas.}{31, 33, 60}
\begin{encadre}
\begin{exemple*}[Grothendieck, pages 38 à 58, moyenne sur l'inertie et dualité\piste{60-inertia-average-duality}]\nonverifie
Soit $E_\eta$ un faisceau $\ell$-adique au point générique d'une courbe sur $\mathbf F_p$. En remplaçant chaque fibre ramifiée $E^{I_x}$ par la moyenne de $E$ sur l'inertie modulo un sous-groupe ouvert qui agit de façon unipotente, on obtient un faisceau virtuel $E_\eta^\natural$ dont la fonction $L$ est additive et locale en $(E, x)$. Son dual de Verdier est $\check E_\eta^\natural(1)[2]$ augmenté des termes locaux $\mu_x(E) = \alpha_x(E_\eta)^\vee - \alpha_x(\check E_\eta)(1)$ ; la page~52 demande si $\delta^\natural(E_\eta)^2 = q^{\chi^\natural(E_\eta)}$ pour $E_\eta$ autodual de poids~$\rho$.
\end{exemple*}
\end{encadre}
{\small En termes actuels, la fibre moyennée $E^{\natural(x)}$ est l'espace des invariants de l'inertie dans la représentation de Weil--Deligne de $E$ restreinte au groupe de décomposition en $x$, l'opérateur de monodromie $N$ étant oublié, c'est-à-dire dans sa semi-simplifiée ; cette traduction est de la lecture. La lecture montre aussi, par le théorème de monodromie $\ell$-adique que la page suppose sans le nommer, que $\mu_x(E) = 0$ pour tout $E_\eta$ : les termes correctifs de la page s'annulent, et la question de la page~52 reçoit la réponse oui. Cet argument est de l'édition et n'est pas vérifié en Lean ; l'équation fonctionnelle de la fonction $L$ ainsi formée n'a pas été cherchée dans la littérature sur les constantes locales. Les connexions et la monodromie en caractéristique~$0$ sont l'objet de la section~\ref{sec:93} (connexions projectives) et des énoncés de la cote~162-5 (partie \q{Catégories et foncteurs}). Mathlib n'a pas les faisceaux $\ell$-adiques, leurs fonctions $L$ ni la dualité de Verdier. On se reportera aux notes de Grothendieck (\lot{60}{2}{38}).\par}

\begin{encadre}
\begin{theoreme*}[Grothendieck, pages 64 à 70, majoration de la dimension cohomologique ; voir M.~Artin, SGA~4, exposé~X, théorème~4.1 (1973)\pisteresolue{31-phi-specialisation-criterion}]\nonverifie
Soit $\varphi$ une fonction sur les points d'un schéma noethérien $X$ telle que $\varphi(x) \geq \mathrm{cd}_\ell(k(x))$ en tout point et $\varphi(y) < \varphi(x) - \mathrm{cd}_\ell(\mathcal O_{X,\bar y} \otimes k(x))$ pour toute spécialisation stricte $y$ de~$x$. Alors $H^i(X, F) = 0$ pour tout faisceau de $\ell$-torsion $F$ et tout $i$ supérieur au supremum de $\varphi$ sur le support de~$F$.
\end{theoreme*}
\end{encadre}
\begin{demopage}[pages 64 à 67]
Le résultat est publié par M.~Artin dans SGA~4, exposé~X, théorème~4.1 (1973) \cite{sga4-3} ; l'inventaire date la cote [1963--1973]. Par récurrence noethérienne sur $X$ (p.~66), une suite de composition par des faisceaux élémentaires (p.~64) ramène au cas $F = g_*(G)$, $g : \operatorname{Spec} k(x) \to X$, $G$ fini, où $\varphi(F) = \varphi(x)$ ; la prose de cette réduction est en grande partie illisible. La suite spectrale de Leray de $g$ et la fibre $(R^q g_*G)_{\bar y} = H^q(\mathcal O_{X,\bar y} \otimes k(x), G)$ donnent, par l'hypothèse sur les spécialisations, l'estimation encadrée $\varphi(R^q g_*G) \leq \varphi(x) - q$, et pour $q > 0$ l'hypothèse de récurrence tue $H^p(X, R^q g_*G)$ (p.~67). La page conclut sur un croquis du plan $(p, q)$, sans écrire le dernier pas.
\end{demopage}

\begin{encadre}
\begin{conjecture*}[Grothendieck, page 84, dimension cohomologique et degré d'imperfection\piste{31-imperfection-bound-conjectures}]
En la caractéristique résiduelle $\ell$, la borne de la dimension cohomologique d'un schéma affine est gouvernée par le degré d'imperfection $\nu(k)$, défini par $\ell^{\nu(k)} = [k : k^\ell]$, plutôt que par la dimension : $\mathrm{cd}_\ell(X) \leq \sup(\mathrm{cd}_\ell\, k(x), \nu(V(\ell)) + 3)$, et $\mathrm{cd}_\ell(U) \leq \dim A + \nu(k) + \mathrm{cd}_\ell(k)$ pour $U$ ouvert du spectre d'un anneau local hensélien intègre $A$ de caractéristique résiduelle $\ell$ dont le corps des fractions est de caractéristique~$0$.
\end{conjecture*}
\end{encadre}
{\small La seconde borne tient, sous une forme plus précise, pour $A$ hensélien, excellent et intègre, de corps résiduel de caractéristique~$\ell$ et de corps des fractions de caractéristique nulle, et $U$ ouvert affine non vide de $\operatorname{Spec} A[1/\ell]$ : Gabber et Orgogozo (2008, théorème~6.1) \cite{gabberorgogozo2008} montrent $\mathrm{cd}_\ell(U) = \dim A + \dim_\ell(k)$, où $\dim_\ell$ est la $\ell$-dimension de Kato, et $\dim_\ell(k) \leq \nu(k) + \mathrm{cd}_\ell(k)$ découle de leur définition~1.1 ; les mots qui entourent \q{ouvert} sont illisibles, et rien n'est connu ici pour un $U$ qui rencontre $V(\ell)$. Le rôle de $[k : k^\ell]$ est annoncé, sans borne, dans SGA~4, exposé~X, §~3.0 \cite{sga4-3}. La première borne, $\sup(\mathrm{cd}_\ell\, k(x), \nu(V(\ell)) + 3)$, n'a été trouvée dans aucune source lue. Les résultats les plus proches sont locaux ou relatifs : Mathew (2021, démonstration de la proposition~4.5) \cite{mathew2021} obtient la même forme, $\mathrm{cd}_\ell \leq d + 1$ pour les ouverts affines de $\operatorname{Spec} R[1/\ell]$ quand $\dim R_{\mathfrak p} + \log_\ell [\kappa(\mathfrak p) : \kappa(\mathfrak p)^\ell] \leq d$ le long de $V(\ell)$, mais pour $R$ intègre, normal et excellent, hensélien le long d'un idéal contenant~$\ell$ ; Gabber et Zavyalov (2026, théorème~1.7) \cite{gabberzavyalov2026} traitent les algèbres affinoïdes, où $\ell$ est inversible. Les bornes globales imprimées sont plus grossières : SGA~4 donne $\mathrm{cd}_\ell X \leq 2 \dim X + 1$ pour $X$ de type fini sur $\mathbf Z$ (exposé~X, 6.2 \cite{sga4-3}), et Clausen et Mathew $\mathrm{cd}_\ell(X) \leq \dim X + \sup_x \mathrm{cd}_\ell\, k(x)$ pour $X$ qcqs de dimension de Krull finie (corollaire~3.29 \cite{clausenmathew2021}), plus grossière d'un $\dim X$. Le $+2$ de la proposition~5.4.5 de Gabber et Orgogozo porte sur $\dim_\ell(k)$, qui vaut $\nu(k)$ ou $\nu(k) + 1$, et ne se compare pas au $+3$ de la page. La constante $3$ paraît être la bonne : pour $\operatorname{Spec}\mathbf Z$ et $\ell$ impair, $\nu(V(\ell)) = 0$ et $\mathrm{cd}_\ell\,\mathbf Q = 2$, tandis que $\mathrm{cd}_\ell(\operatorname{Spec}\mathbf Z) = 3$ (SGA~4, exposé~X, 6.1 \cite{sga4-3} ; la dualité d'Artin--Verdier donne $H^3(\operatorname{Spec}\mathbf Z, j_!\mu_\ell) \simeq \mathbf Z/\ell$, Milne, II.3.2 et 3.3 \cite{milne2006}) ; la comparaison avec la constante de la page est de l'édition. Mathlib n'a pas la dimension cohomologique étale. On se reportera aux notes de Grothendieck (\lot{31}{5}{84}).\par}

\begin{encadre}
\begin{theoreme*}[Grothendieck, page 22, minoration de la dimension cohomologique\piste{31-local-ring-cd-lower-bound}]\nonverifie
Soit $A$ un anneau local noethérien intègre, de corps des fractions $K$ et de corps résiduel $k$. Pour tout premier $r$, $\mathrm{cd}_r(K) \geq \mathrm{cd}_r(k) + \dim A$, sauf peut-être si $r$ est la caractéristique de $K$, ou si $r = 2$ et qu'un point $x$ de $\operatorname{Spec} A$ a un corps résiduel ordonnable avec $\mathrm{cd}_2\, k(x)(\sqrt{-1})$ fini ; la seconde exception disparaît quand $A$ est régulier.
\end{theoreme*}
\end{encadre}
{\small Quand $r$ est inversible dans $A$, l'inégalité est le corollaire~2.4 de SGA~4, exposé~X \cite{sga4-3}, avec l'exception plus grossière \q{un corps résiduel ordonnable} ; l'exemple de la marge, $\mathbf R[X,Y]/(X^2+Y^2)$ à l'origine, est celui qui suit le théorème~2.3 du même exposé ; quand $r$ est la caractéristique résiduelle et $K$ de caractéristique nulle, elle suit, pour $A$ excellent hensélien, du §~3 de Gabber et Orgogozo (2008) \cite{gabberorgogozo2008}. L'exception plus fine de la page et sa disparition pour $A$ régulier n'ont pas été trouvées ; le livre de Scheiderer \cite{scheiderer1994}, qui traite la dimension cohomologique en présence d'ordres, reste à lire ; la marge demande si la restriction est essentielle. Mathlib n'a pas la dimension cohomologique galoisienne. On se reportera aux notes de Grothendieck (\lot{31}{2}{22}).\par}