\section[Cote 43 : polynômes additifs modulo $F - 1$ et perfection]{Cote 43 : polynômes additifs modulo $F - 1$ et perfection\protect\verifie{Folder43}}\label{sec:43}

La cote 43, \emph{Dualité des groupes. Jacobiennes généralisées etc}, réunit des liasses sur le corps de classes, les jacobiennes généralisées de Rosenlicht, la dualité de Cartier et les accouplements de Tate et de Lang ; la carte la date de 1964--1965. Aux pages~165 à~169, un lemme identifie $\mathrm{Ext}^1_{S\text{-gr}}(G, \Gamma)$ aux classes primitives de $H^1(G, \Gamma)$, puis la page~169 écrit, pour une base $S$ de caractéristique~$p$ (\lot{43}{9}{165}) :
\[
\mathrm{Ext}^1_{S\text{-gr}}(\mathbb G_a, \mathbb Z/p\mathbb Z) \simeq \Gamma(S, \mathcal O^{p^{-\infty}}), \qquad \mathcal O^{p^{-\infty}} = \varinjlim\bigl(\mathcal O \xrightarrow{x \mapsto x^p} \mathcal O \xrightarrow{x \mapsto x^p} \cdots\bigr).
\]
Pour voir d'où vient la perfection, on observe qu'une extension de $\mathbb G_a$ par $\mathbb Z/p\mathbb Z$ sur $S = \mathrm{Spec}\,R$ est un revêtement d'Artin--Schreier $x^p - x = f(t)$, et elle est compatible à l'addition quand $f$ est un \emph{polynôme additif}, $f(t) = \sum_i a_i t^{p^i}$ ; deux tels $f$ donnent la même classe quand ils diffèrent d'un $g^p - g$, $g$ additif. La lecture remarque que, modulo ces $g^p - g$, tout polynôme additif se ramène à un seul terme $a\,t$ avec $a$ dans la perfection. On démontre ici ce cœur algébrique, sur une base affine quelconque.

\noindent\emph{Notations.} Soient $p$ premier et $R$ un anneau commutatif de caractéristique~$p$. On note $R\{F\}$ le groupe des polynômes additifs $\sum_i a_i t^{p^i}$, suites presque nulles $(a_i)$ d'éléments de $R$. La composition à gauche par $F : t \mapsto t^p$ envoie $\sum a_i t^{p^i}$ sur $\sum a_i^p t^{p^{i+1}}$, qui est $(\sum a_i t^{p^i})^p$ en caractéristique~$p$ ; on pose $D = F - 1$, de sorte que $D(f) = f^p - f$. La perfection $R^{p^{-\infty}}$ est l'ensemble des classes de couples $(i, a)$, où $(i, a)$ représente $a^{p^{-i}}$ et $(i + 1, a^p)$ s'identifie à $(i, a)$ ; on note $[a]_i$ cette classe.

\begin{encadre}
\begin{theoreme*}[D'après la lecture des pages 165 à 169, $S$ affine\piste{43-ext-ga-zp-perfection}]
L'application $\Phi : R\{F\} \to R^{p^{-\infty}}$, $\sum_i a_i t^{p^i} \mapsto \sum_i [a_i]_i$, est un homomorphisme surjectif de groupes, de noyau exactement l'image de $D = F - 1$. Elle induit un isomorphisme de groupes
\[
R\{F\}/(F - 1)R\{F\} \;\simeq\; R^{p^{-\infty}}.
\]
De plus, modulo l'image de $D$, tout polynôme additif est égal à un seul terme $c\,t^{p^M}$, pour tout $M$ assez grand.
\end{theoreme*}
\end{encadre}

\begin{proof}
L'application $a \mapsto [a]_i$ est additive : $[a]_i + [b]_i = [a^{p^i} + b^{p^i}]_{2i} = [(a + b)^{p^i}]_{2i} = [a + b]_i$, par la règle de somme de la perfection et l'additivité de Frobenius. Donc $\Phi$ est additive. Elle tue l'image de $D$ : $\Phi(F(a\,t^{p^i})) = [a^p]_{i+1} = [a]_i$, d'où $\Phi \circ F = \Phi$ et $\Phi \circ D = 0$. Elle est surjective, puisque $[a]_n = \Phi(a\,t^{p^n})$.

Pour le noyau, on monte d'un cran : $a\,t^{p^N} - a^p\,t^{p^{N+1}} = -D(a\,t^{p^N})$, et par récurrence $a\,t^{p^N} \equiv a^{p^z}\,t^{p^{N+z}}$ modulo l'image de $D$ pour tout $z$. Un polynôme $\sum_{i \leq N} a_i t^{p^i}$ est donc congru à $c\,t^{p^M}$ pour tout $M \geq N$, avec $c = \sum_i a_i^{p^{M-i}}$ : c'est la dernière assertion. Si $\Phi(f) = 0$ et $f \equiv c\,t^{p^M}$, alors $[c]_M = 0$ dans la perfection, ce qui signifie $c^{p^z} = 0$ pour un $z$. Alors $c\,t^{p^M} \equiv c^{p^z} t^{p^{M+z}} = 0$, et $f$ est dans l'image de $D$. L'isomorphisme s'en déduit par passage au quotient.
\end{proof}

\begin{remarque}
Aucune hypothèse de réduction ni de noethérianité n'intervient : les éléments $x$ tels que $x^{p^z} = 0$, qui forment le noyau de $R \to R^{p^{-\infty}}$, sont absorbés par $F - 1$. La parenthèse de la page qui semble évoquer \q{l'hypothèse noethérienne} n'a donc pas lieu d'être pour ce cœur algébrique. En Lean, $R\{F\}$ est représenté par les suites presque nulles, et l'identification $D(f) = f^p - f$ avec le polynôme est vérifiée dans $R[t]$.
\end{remarque}

Ne sont pas démontrés ici les deux énoncés suivants de la cote. Le premier est la formule de la page~169 telle qu'elle est écrite : il y faut en outre le lemme des pages~166 à~168 sur les classes primitives, son invariance par homéomorphisme universel, le passage à une base non affine et la représentabilité par des pro-schémas parfaits.

\begin{encadre}
\begin{theoreme*}[Grothendieck, pages 165 à 169, $\mathrm{Ext}^1(\mathbf G_a, \mathbf Z/p\mathbf Z)$ et perfection\piste{43-ext-ga-zp-perfection}]\nonverifie
Sur une base quelconque $S$ de caractéristique~$p$, $\mathrm{Ext}^1_{S\text{-gr}}(\mathbf G_a, \mathbf Z/p\mathbf Z) \simeq \Gamma(S, \mathcal O^{p^{-\infty}})$, sections globales de la perfection $\varinjlim(\mathcal O \to \mathcal O \to \cdots)$ pour $x \mapsto x^p$. Le foncteur $\mathrm{Ext}^1(\mathbf G_a, \mathbf Z/p\mathbf Z)$ est donc représentable parmi les pro-schémas parfaits sur~$S$.
\end{theoreme*}
\end{encadre}
{\small Les feuillets en esquissent une démonstration incomplète (pages 166 à 168) : ils démontrent le lemme des classes primitives et son invariance par homéomorphisme universel, mais pas la formule elle-même, et le mot \q{parfaits} est incertain. Mathlib n'a pas les $\mathrm{Ext}$ de schémas en groupes. On se reportera aux notes de Grothendieck (\lot{43}{9}{165}).\par}

\begin{encadre}
\begin{theoreme*}[D'après les pages 70 à 74, forme corrigée par l'édition, concentration de la cohomologie locale\piste{43-local-cohomology-concentration}]\nonverifie
Soient $A$ un anneau local régulier de dimension $d$ contenant un corps algébriquement clos $k$, et $G$ un groupe algébrique commutatif sur $k$. La cohomologie locale de Zariski $H^i_{\mathfrak a}(\operatorname{Spec} A, G)$ au point fermé est nulle pour $i \neq d$ ; elle vaut $G(K)/G(A)$ pour $d = 1$ et $H^{d-1}(\operatorname{Spec} A - \mathfrak a, U)$ pour $d \geq 2$, où $U$ est la partie unipotente de $G$. Le foncteur $G \mapsto H^d_{\mathfrak a}(G)$ est donc exact sur les suites localement triviales ; cette exactitude sert à définir la jacobienne locale $J_{A/k}$ de la page~74.
\end{theoreme*}
\end{encadre}
{\small La clôture algébrique de $k$ est ajoutée par l'édition, et presque tous les mots de la prose sont de lecture incertaine. Mathlib n'a pas la cohomologie locale à valeurs dans un groupe algébrique. On se reportera aux notes de Grothendieck (\lot{43}{4}{70}).\par}

\section[Cote 101 : la dualité locale en dimension un pour tous les modules]{Cote 101 : la dualité locale en dimension un pour tous les modules\protect\verifie{Folder101}}\label{sec:101}

La cote 101, \emph{Cohomologie locale : notes manuscrites (s.d.)}, quarante-deux pages que l'inventaire date \q{[à partir de 1967-1968]}, énonce page~10, pour $A$ local régulier complet de dimension $n$, $X = \operatorname{Spec} A$ et $I = H^n_x(\mathcal O_X)$, que les applications de dualité $\varphi^i_F : \mathrm{Ext}^{n-i}(X; F, \mathcal O_X) \to \mathrm{Hom}(H^i_x(F), I)$ sont des isomorphismes pour tout $\mathcal O_X$-module $F$, \q{pas nécessairement quasi-cohérent} (\lot{101}{1}{10}). Pour $n = 1$, les pages~10 et~11 le démontrent. Un $\mathcal O_X$-module est un triplet $(M_0, M_1, u)$ : un $A$-module $M_0$, un $K$-espace vectoriel $M_1$ et une application $A$-linéaire $u : M_0 \to M_1$, avec $H^0_x(F) = \mathrm{Ker}\, u$ et $H^1_x(F) = \mathrm{Coker}\, u$. La résolution injective $\mathcal O_X \to \underline K_X \to \underline K_X/\mathcal O_X$ donne $\mathrm{Ext}^\bullet(X; F, \mathcal O_X)$ comme cohomologie du complexe $\mathrm{Hom}_K(M_1, K) \to \mathrm{Hom}_A(M_0, K/A)$, $g \mapsto g \circ u \bmod A$. La page conclut par trois faits : a) un homomorphisme d'un $K$-espace vectoriel dans $A$ est nul ; b) $\mathrm{Ext}^1_A(K, A) = 0$, parce que $A$ est complet ; c) $K/A$ est injectif.

\noindent\emph{Conventions.} On travaille dans le modèle de la page, dont on admet la réduction : l'équivalence entre $\mathcal O_X$-modules et triplets, et le calcul des $\mathrm{Ext}$ par la résolution. $\mathrm{Ext}^0$ est le noyau et $\mathrm{Ext}^1$ le conoyau de $g \mapsto g \circ u \bmod A$.

Le diagramme suivant montre le complexe et les deux applications de dualité du théorème ci-dessous ; la flèche horizontale du milieu est $g \mapsto g \circ u \bmod A$ :
\[
\begin{tikzcd}[column sep=small]
\mathrm{Ext}^0 \arrow[r, hook] \arrow[d] & \mathrm{Hom}_K(M_1, K) \arrow[r] & \mathrm{Hom}_A(M_0, K/A) \arrow[r, two heads] & \mathrm{Ext}^1 \arrow[d] \\
\mathrm{Hom}_A(\mathrm{Coker}\, u, K/A) & & & \mathrm{Hom}_A(\mathrm{Ker}\, u, K/A)
\end{tikzcd}
\]

\begin{theoreme}[Grothendieck, pages 10 et 11, dimension un\piste{101-sheaf-duality-dim-one}]\label{thm:101-dualite}
Soit $A$ un anneau de valuation discrète complet, de corps des fractions $K$. Pour tout triplet $(M_0, M_1, u)$, les applications $\mathrm{Ext}^0 \to \mathrm{Hom}_A(\mathrm{Coker}\, u, K/A)$, $g \mapsto (g \bmod A)$, et $\mathrm{Ext}^1 \to \mathrm{Hom}_A(\mathrm{Ker}\, u, K/A)$, restriction, sont bijectives.
\end{theoreme}

\begin{proof}
Soit $\varpi$ une uniformisante. Fait a) : si $g(m) = y \neq 0$, alors $g((\varpi y)^{-1} m) = \varpi^{-1} \in A$, absurde. Fait b) : soit $f : K \to K/A$ linéaire et $c_n \in K$ avec $f(\varpi^{-n}) = c_n \bmod A$. Comme $\varpi f(\varpi^{-n-1}) = f(\varpi^{-n})$, les $d_n = \varpi^n c_n$ vérifient $d_{n+1} - d_n \in \varpi^n A$ ; par complétude, $d_n - d_0$ converge vers $e \in A$, avec $d_0 + e - d_n \in \varpi^n A$. Pour $c = d_0 + e$, on a $c\,\varpi^{-n} - c_n \in A$ pour tout $n$, donc $f(x) = cx \bmod A$ pour tout $x = a \varpi^{-n}$. Sur une base de $M_1$, tout $h : M_1 \to K/A$ se relève ainsi en une application $K$-linéaire $M_1 \to K$. Fait c) : $A$ est principal et $K/A$ divisible, d'où le critère de Baer.

L'injectivité sur $\mathrm{Ext}^0$ est a) appliqué à une différence. Pour la surjectivité, un $\psi : \mathrm{Coker}\, u \to K/A$ donne $h : M_1 \to K/A$ nul sur $u(M_0)$, qui se relève par b) en $g$, et $g \circ u$ est à valeurs dans~$A$. La surjectivité sur $\mathrm{Ext}^1$ est c). Pour l'injectivité, un $h : M_0 \to K/A$ nul sur $\mathrm{Ker}\, u$ se factorise par $u(M_0) \subset M_1$, s'étend à $M_1$ par c), se relève par b) en $g : M_1 \to K$, et $h = g \circ u \bmod A$.
\end{proof}

\begin{remarque}
L'énoncé tient tel que la page le démontre ; la complétude ne sert qu'en b). La fin de l'argument d'injectivité, en partie illisible sur la page, est rétablie par la lecture dans cet ordre, et Lean la confirme. Les deux pages ne numérotent pas les applications de la même façon. La page~10 les indexe par le degré de cohomologie locale, si bien que $\varphi^1$ part de $\mathrm{Ext}^0$ ; la page~11 écrit au contraire $E^0 \xrightarrow{\varphi^0} \mathrm{Hom}(\mathrm{Coker}\, u, K/A)$. Les noms \texttt{phi0} et \texttt{phi1} du code Lean suivent la page~11.
\end{remarque}

La note de la lecture qui cite de mémoire l'équivalence entre $\mathrm{Ext}^1_A(K, A) = 0$ et la complétude est exacte ; c'est la réciproque de b).

\begin{enonce}[Réciproque du fait b), note de la lecture\piste{101-sheaf-duality-dim-one}]\label{thm:101-reciproque}
Soit $A$ un anneau de valuation discrète, de corps des fractions $K$. Alors $A$ est complet si et seulement si toute application $A$-linéaire $K \to K/A$ se relève en une application $A$-linéaire $K \to K$, autrement dit si et seulement si $\mathrm{Hom}_A(K, K) \to \mathrm{Hom}_A(K, K/A)$ est surjective, ce qui équivaut à $\mathrm{Ext}^1_A(K, A) = 0$ puisque $K$ est injectif.
\end{enonce}

\begin{proof}
Le sens direct est b). Réciproquement, $A$ est séparé pour la topologie $\mathfrak m$-adique (Krull). Soit $(e_n)$ une suite de Cauchy, $e_m - e_n \in \varpi^n A$ pour $n \leqslant m$. Pour $x \in K$ et $n$ tel que $\varpi^n x \in A$, la classe de $e_n x$ modulo $A$ ne dépend pas de $n$, car $(e_m - e_n) x \in \varpi^n x A \subset A$ ; elle définit une application $A$-linéaire $f : K \to K/A$. Un relèvement $g$ de $f$ vérifie $g(1) \equiv e_0 \bmod A$, donc $g(1) \in A$, et $g(1) - e_n = \varpi^n \bigl(g(\varpi^{-n}) - e_n \varpi^{-n}\bigr) \in \varpi^n A$ : la suite converge vers $g(1)$.
\end{proof}

Ne sont pas démontrés ici : l'équivalence entre $\mathcal O_X$-modules et triplets, et le calcul des $\mathrm{Ext}$ (et, en particulier, l'identification de $\mathrm{Ext}^1_A(K, A)$ au conoyau de $\mathrm{Hom}_A(K, K) \to \mathrm{Hom}_A(K, K/A)$, qui n'est pas formalisée) et des $H^i_x$ dans ce modèle. En dimension~$2$ la dualité échoue, et la page~14 le découvre (piste \texttt{101-sheaf-duality-dim-two-fails}, ci-dessous) :

\begin{encadre}
\begin{contrexemple*}[pages 10, 14 et 15, dualité locale en dimension deux\piste{101-sheaf-duality-dim-two-fails}]\nonverifie
La première phrase de la page~10 affirme les isomorphismes de dualité locale en toute dimension ; ils tombent en défaut en dimension~$2$. Soient $A$ un anneau local régulier complet de dimension~$2$, $f \in \mathfrak m$ non nul, $U = X_f$ et $F = j_!\mathcal O_U$ sur $X = \operatorname{Spec} A$. L'application $A_f = \mathrm{Ext}^0(X; F, \mathcal O_X) \to \mathrm{Hom}_A(H^2_x(F), E(k))$ est injective et non surjective : la dualité locale à duaux de Matlis algébriques ne vaut pas pour les $\mathcal O_X$-modules non quasi-cohérents.
\end{contrexemple*}
\end{encadre}
{\small La page~14 conclut \q{$\varphi$ n'est pas surjective}, souligné deux fois, sans démonstration, et une phrase commencée page~14, achevée page~15, dit qu'il faut des duaux topologiques. Mathlib n'a pas la cohomologie locale ni la dualité de Matlis.\par}
\section[Cote 125 : la carte des équivalences et le lemme du feuillet III-18]{Cote 125 : la carte des équivalences et le lemme du feuillet III-18\protect\verifie{Folder125}}\label{sec:125}

La cote 125, \emph{Dualité projective : notes manuscrites (s.d.)}, datée par l'inventaire \q{[avant 1970]}, compte huit feuillets, dont une chemise titrée de sa main \q{Dualité locale et dualité \dots\ projective}. Le feuillet~2 est une carte : six énoncés encadrés, reliés par des doubles flèches verticales, pour $\mathbf P^n \supset X^r \supset Y^m$, $r > m > 0$. Le premier énoncé est la suite exacte de cohomologie locale, marquée d'une astérisque ; la flèche du deuxième encadré au troisième porte le seul mot du feuillet, \q{dualité}, entouré (\lot{125}{1}{2}). Le feuillet~3 est une page de tapuscrit numérotée III-18, annotée d'une autre main. Elle établit qu'un homomorphisme $u : A^n \to B$ bijectif sur les germes en un point l'est sur un voisinage, avec en marge la justification \q{puisque $Y$ est noethérien et $B$ de type fini par hypothèse} (\lot{125}{1}{3}). La lecture modernisée donne les trois premiers étages de la carte et ce lemme, seules parties du dossier qui ne dépendent ni de la dualité de Serre ni du complété formel ; on les démontre ici.

\begin{enonce}[Feuillet 2, trois premiers étages\lie{6}\lie{9}]
Soient $X$ une variété projective de dimension $r$, $Y \subset X$ un fermé de dimension $m$, $F$ un faisceau cohérent sur $X$. Les énoncés suivants sont équivalents :
\begin{enumerate}
\item (premier étage) $H^p(X - Y, F) = 0$ pour $p \geqslant m$ ;
\item (deuxième étage) $H^p_Y(X, F) \to H^p(X, F)$ est bijectif pour $p > m$ et surjectif pour $p = m$ ;
\item (troisième étage) $\mathrm{Ext}^q_{\mathcal O_X}(F, \Omega^r_{X/k}) \to \mathrm{Ext}^q_{\mathcal O_{\widehat X}}(\widehat F, \widehat\Omega^r_{X/k})$ est bijectif pour $q < r - m$ et injectif pour $q = r - m$.
\end{enumerate}
Le deuxième étage est \q{le premier étage lu à travers la suite exacte} ; le troisième lui est équivalent par la dualité, qui met $H^p$ et $\mathrm{Ext}^{r-p}(-, \Omega^r)$ en accouplement parfait, et \q{les bornes se répondent comme il faut : $p \geqslant m$ d'un côté, $q < r - m$ de l'autre, et $p + q = r$}.
\end{enonce}

On démontre ici la forme abstraite de ces deux passages. Pour le premier, on se donne une suite exacte longue quelconque indexée par les entiers naturels,
\[
  \cdots \to L^p \xrightarrow{\ a_p\ } G^p \xrightarrow{\ b_p\ } C^p \xrightarrow{\ \delta_p\ } L^{p+1} \xrightarrow{\ a_{p+1}\ } \cdots
\]
de groupes abéliens, exacte en chaque terme ; $L^p$ tient lieu de $H^p_Y(X,F)$, $G^p$ de $H^p(X,F)$, $C^p$ de $H^p(X-Y,F)$. Pour le second, la dualité de Serre n'est pas démontrée : on l'admet sous la forme que lui prête la lecture : sur le corps $k$, la flèche de comparaison des $\mathrm{Ext}$ en degré $q = r - p$ s'identifie à la transposée ${}^t a_p : (G^p)^\vee \to (L^p)^\vee$ de $a_p$.

\begin{lemme}\label{lem:125-etage12}
Soit $m \in \mathbb N$. On a $C^p = 0$ pour tout $p \geqslant m$ si et seulement si $a_p$ est bijectif pour tout $p > m$ et $a_m$ est surjectif.
\end{lemme}

\begin{proof}
Supposons $C^p = 0$ pour $p \geqslant m$. Pour $p \geqslant m$, $b_p$ est nul, donc son noyau, qui est l'image de $a_p$ par exactitude en $G^p$, est $G^p$ tout entier : $a_p$ est surjectif, en particulier pour $p = m$. Soit $p > m$ ; écrivons $p = q + 1$ avec $q \geqslant m$. Par exactitude en $L^{q+1}$, le noyau de $a_{q+1}$ est l'image de $\delta_q$, qui est nulle puisque $C^q = 0$ : $a_p$ est injectif, donc bijectif.

Réciproquement, supposons $a_p$ bijectif pour $p > m$ et $a_m$ surjectif, et soient $p \geqslant m$ et $c \in C^p$. D'abord $a_p$ est surjectif : si $p > m$ parce qu'il est bijectif, si $p = m$ par hypothèse. Par exactitude en $L^{p+1}$, $a_{p+1}(\delta_p(c)) = 0$ ; comme $p + 1 > m$, $a_{p+1}$ est injectif et $\delta_p(c) = 0$. Par exactitude en $C^p$, il existe $y \in G^p$ avec $c = b_p(y)$, puis, $a_p$ étant surjectif, $x \in L^p$ avec $y = a_p(x)$. Alors $c = b_p(a_p(x)) = 0$ par exactitude en $G^p$.
\end{proof}

\begin{lemme}\label{lem:125-etage23}
Soient $k$ un corps, $(a_p : L^p \to G^p)_{p \in \mathbb N}$ des applications $k$-linéaires, et $m \leqslant r$ des entiers. Les conditions suivantes sont équivalentes :
\begin{enumerate}
\item $a_p$ est bijectif pour $m < p \leqslant r$ et $a_m$ est surjectif ;
\item ${}^t a_{r-q}$ est bijectif pour $q < r - m$ et ${}^t a_{m}$ est injectif.
\end{enumerate}
De plus, si $p + q = r$, on a $p \geqslant m \Leftrightarrow q \leqslant r - m$ et $p > m \Leftrightarrow q < r - m$.
\end{lemme}

\begin{proof}
On utilise deux faits classiques d'algèbre linéaire sur un corps, valables en dimension quelconque : une application linéaire $a$ est surjective si et seulement si sa transposée ${}^t a$ est injective, et elle est bijective si et seulement si ${}^t a$ l'est. (Le premier est immédiat dans un sens, et dans l'autre repose sur le fait qu'un sous-espace strict est contenu dans le noyau d'une forme linéaire non nulle ; le second en découle, avec l'énoncé dual : $a$ injective si et seulement si ${}^t a$ surjective, par prolongement des formes linéaires à partir d'un sous-espace.)

Les deux conditions sur $a_m$ se correspondent donc. Pour les autres : si $q < r - m$, l'entier $p = r - q$ vérifie $m < p \leqslant r$, et ${}^t a_{r-q}$ est bijectif puisque $a_p$ l'est ; si inversement $m < p \leqslant r$, l'entier $q = r - p$ vérifie $q < r - m$ et $r - q = p$, et $a_p$ est bijectif puisque ${}^t a_p$ l'est. L'assertion sur les bornes est de l'arithmétique : sous $p + q = r$, $p \geqslant m$ équivaut à $r - q \geqslant m$, soit $q \leqslant r - m$, et de même avec des inégalités strictes.
\end{proof}

Le lemme du feuillet~3 est démontré ici sous sa forme affine : $Y = \operatorname{Spec} R$ et le voisinage cherché est un ouvert $D(f)$.

\begin{enonce}[Feuillet 3, III-18, forme affine]
Soient $R$ un anneau noethérien, $\mathfrak p$ un idéal premier de $R$, $B$ un $R$-module de type fini et $u : R^n \to B$ une application $R$-linéaire telle que $u_{\mathfrak p} : R^n_{\mathfrak p} \to B_{\mathfrak p}$ soit bijective. Il existe $f \in R \setminus \mathfrak p$ tel que $u_f : R^n_f \to B_f$ soit bijective.
\end{enonce}

\begin{proof}
Le module $B$, de type fini sur un anneau noethérien, est de présentation finie : le noyau d'une surjection $R^s \to B$ est un sous-module de $R^s$, donc de type fini. Il suffit alors de démontrer l'énoncé classique suivant, où l'anneau commutatif $R$ est quelconque : \emph{si $M$ est de type fini, $B$ de présentation finie et $u : M \to B$ bijective en $\mathfrak p$, alors $u_f$ est bijective pour un $f \notin \mathfrak p$.}

Le conoyau $Q$ de $u$ est de type fini, quotient de $B$, et $Q_{\mathfrak p} = 0$ puisque la localisation est exacte. Chacun de ses générateurs $y_1, \dots, y_t$ est donc annulé par un $g_i \notin \mathfrak p$, et $g = g_1 \cdots g_t \notin \mathfrak p$ annule $Q$ : $Q_g = 0$, c'est-à-dire que $u_g : M_g \to B_g$ est surjective. Son noyau $K$ est de type fini : $M_g$ est de type fini sur $R_g$, $B_g$ de présentation finie, et le noyau d'une surjection d'un module de type fini sur un module de présentation finie est de type fini (fait classique : si $0 \to K \to M' \xrightarrow{\ \pi'\ } B' \to 0$ est exacte, avec $M'$ de type fini et $B'$ de présentation finie, choisissons une surjection $\pi : R^s \to B'$ de noyau $N$ de type fini et relevons-la en $\varphi : R^s \to M'$ avec $\pi' \varphi = \pi$ ; chaque générateur de $M'$ s'écrit $\varphi(x_j) + k_j$ avec $k_j \in K$, et tout $k \in K$ s'écrit $\varphi(x) + \sum c_j k_j$ où $\pi(x) = \pi'(k) = 0$, de sorte que $K = \varphi(N) + \sum_j R k_j$). Comme $K_{\mathfrak p}$ est le noyau de $u_{\mathfrak p}$, il est nul ; le même argument donne $h \notin \mathfrak p$ tel que $K_h = 0$. Avec $f = gh \notin \mathfrak p$, $u_f$ est surjective et injective.
\end{proof}

\begin{remarque}
Le passage du premier au deuxième étage vaut pour toute suite exacte longue, avec les bornes du feuillet ; il n'utilise rien de $X$, de $Y$ ni de $F$. La dualité étant admise sous la forme d'une transposition, les trois étages encadrés sont cohérents entre eux. La comparaison, sous une borne sur la dimension cohomologique de $X - Y$, de la cohomologie de $X$ à celle de son complété formel le long de $Y$, qui fait la suite de la carte, a été publiée par Hartshorne en 1970, au chapitre~III d'\emph{Ample Subvarieties of Algebraic Varieties} \cite{hartshorne1970} ; l'inventaire date le dossier \q{[avant 1970]}.
\end{remarque}

\begin{remarque}
Le commentaire de la lecture apparie $p \geqslant m$ avec $q < r - m$. Sous $p + q = r$, $p \geqslant m$ équivaut à $q \leqslant r - m$, de sorte que la plage $p \geqslant m$ répond à toute celle du troisième étage, cas limite injectif compris. L'écart est dans le commentaire ; la carte est juste.
\end{remarque}

\begin{remarque}
Le lemme III-18 est un fait classique : il vaut sur tout anneau commutatif pour une source de type fini et un but de présentation finie. La noethérianité de $Y$ et la finitude de $B$ qu'invoque la marge servent seulement à rendre $B$ de présentation finie.
\end{remarque}

Ne sont pas démontrés ici : la profondeur le long d'un fermé et le prolongement de type Hartogs ; la dualité de Serre, admise ; les étages~4 et~5 de la carte, qui passent par la complétion formelle ; les annulations pour $\mathcal O(n)$ ; la dimension cohomologique de $P - X$ ; les Ext des pages~4 et~5 ; le feuillet III-5 (Koszul) ; le lemme III-18 pour les faisceaux.

\begin{encadre}
\begin{theoreme*}[Grothendieck, pages 2, 4 et 7, dimension cohomologique du complémentaire ; voir aussi Hartshorne~\cite{hartshorne1970}\piste{125-cd-complement-formal-comparison}]\nonverifie
Soient $P \supset X \supset Y$ de dimensions $n$, $r$ et $m$, avec $r > m > 0$. L'annulation de $H^p(X - Y, F)$ pour $p \geq m$ et tout $F$ cohérent équivaut, par une dualité avec $\mathrm{Ext}^q(-, \Omega^r)$ sur $X$ et sur son complété formel $\hat X$ le long de $Y$, à ce que $H^q(X, F) \to H^q(\hat X, \hat F)$ soit bijectif pour $q < r - m$ et injectif pour $q = r - m$, pour tout $F$ localement libre.
\end{theoreme*}
\end{encadre}
\section[Cote 115 : la dualité d'Isbell par le calcul des noyaux]{Cote 115 : la dualité d'Isbell par le calcul des noyaux\protect\verifie{Folder115}}\label{sec:115}

La cote 115, \emph{\q{Correspondances} fonctorielles. Dualité des topos}, quatorze pages que l'inventaire date \q{[à partir de 1982]}, attache, aux pages~3 à~5, à un noyau $X \in (A \times B)^\wedge$, préfaisceau contravariant en ses deux variables sur deux petites catégories, deux transformées ${}^sX : \widehat A^{\mathrm{op}} \to \widehat B$ et ${}^dX : \widehat B^{\mathrm{op}} \to \widehat A$, reliées par $\mathrm{Hom}_{\widehat A}(L, {}^dX(M)) \simeq X(L, M) \simeq \mathrm{Hom}_{\widehat B}(M, {}^sX(L))$. La page~7 prend $B = A^{\mathrm{op}}$ et pour noyau le hom de $A$, que la marge de la page~3 désigne comme l'élément canonique de $(A \times A^{\mathrm{op}})^\wedge$ (\lot{115}{1}{3}). La lecture modernisée note $\mathcal O$ et $\mathrm{Spec}$ les foncteurs que le manuscrit écrit $\varphi_A$ et $\Psi_A$.

\begin{theoreme}[Grothendieck, pages 3 à 7, la dualité (dite d'Isbell) comme cas particulier\piste{115-isbell-duality-derived-from-kernels}]
Pour tout noyau $K$ sur $A \times B$, ${}^sK$, vu comme foncteur $\widehat A \to (\widehat B)^{\mathrm{op}}$, est adjoint à gauche de ${}^dK$. Pour $B = A^{\mathrm{op}}$ et $K = \mathrm{Hom}_A$, les deux transformées sont exactement $\mathcal O(\Phi)(a) = \mathrm{Hom}(\Phi, y a)$ et $\mathrm{Spec}(\Psi)(a) = \mathrm{Hom}(\Psi, \mathrm{Hom}_A(a, -))$, et l'adjonction est $\mathcal O \dashv \mathrm{Spec} : \widehat A \rightleftarrows (A^\vee)^{\mathrm{op}}$. On a $\mathcal O(y a) \simeq \mathrm{Hom}_A(a, -)$, $\mathrm{Spec}(\mathrm{Hom}_A(a, -)) \simeq y a$, et $\mathcal O$ transforme les colimites de $\widehat A$ en limites de $A^\vee$.
\end{theoreme}

Le diagramme montre l'adjonction et ses valeurs sur les représentables ; le triangle commute à isomorphisme près :
\[
\begin{tikzcd}[column sep=huge, row sep=large]
\widehat A \arrow[r, shift left=1.2ex, "\mathcal O"] & (A^\vee)^{\mathrm{op}} \arrow[l, shift left=1.2ex, "\mathrm{Spec}"] \\
A \arrow[u, "y"] \arrow[ur, "{a \,\mapsto\, \mathrm{Hom}_A(a, -)}"'] &
\end{tikzcd}
\qquad \mathcal O(ya) \simeq \mathrm{Hom}_A(a, -), \quad \mathrm{Spec}(\mathrm{Hom}_A(a, -)) \simeq ya.
\]

L'énoncé tient tel que la lecture le donne. En Lean, le noyau est un foncteur $K : A^{\mathrm{op}} \to [C, \mathbf{Ens}]$, le cas de la page étant $C = B^{\mathrm{op}}$ ; l'adjonction générale est \texttt{kernelAdj}, la dualité \texttt{isbell}, obtenue en posant $K$ égal au foncteur de co-Yoneda, et les deux formules de la page~7 valent par définition (\texttt{isbellO\_obj\_obj}, \texttt{isbellSpec\_obj\_obj}). La question de la piste, savoir si une démonstration publiée obtient ainsi la dualité, relève de la littérature et reste ouverte.

\begin{theoreme}[caractérisation de $\mathcal O$ et de $\mathrm{Spec}$ par leur restriction le long de $y$]
Le foncteur $\mathcal O$ est l'extension de Kan à gauche le long de $y$ du foncteur $a \mapsto \mathrm{Hom}_A(a, -)$ de $A$ dans $(A^\vee)^{\mathrm{op}}$ : tout foncteur $L : \widehat A \to (A^\vee)^{\mathrm{op}}$ qui transforme colimites en colimites, c'est-à-dire colimites de $\widehat A$ en limites de $A^\vee$, et tel que $L(ya) \simeq \mathrm{Hom}_A(a, -)$ naturellement en $a$, est isomorphe à $\mathcal O$. Dualement, tout foncteur $G : (A^\vee)^{\mathrm{op}} \to \widehat A$ qui commute aux limites et vérifie $G(\mathrm{Hom}_A(a, -)) \simeq ya$ naturellement en $a$ est isomorphe à $\mathrm{Spec}$.
\end{theoreme}

\begin{proof}[Esquisse]
Tout préfaisceau est colimite canonique de représentables, si bien qu'un foncteur commutant aux colimites est déterminé, à isomorphisme près, par sa restriction le long de $y$ ; c'est le théorème de densité de mathlib (\texttt{Presheaf.uniqueExtensionAlongULiftYoneda}), repris ici sous la forme \texttt{isoOfRestrict}. Il s'applique à $\mathcal O$, adjoint à gauche, dont la restriction est $a \mapsto \mathrm{Hom}_A(a, -)$ par le lemme de Yoneda (\texttt{isbellO\_restrict}, \texttt{isbellO\_isLeftKanExtension}, \texttt{isbellO\_unique}). Pour $\mathrm{Spec}$, on passe aux opposés : $G^{\mathrm{op}} : A^\vee \to \widehat A^{\mathrm{op}}$ commute aux colimites, $A^\vee$ est la catégorie des préfaisceaux sur $A^{\mathrm{op}}$, dont les représentables sont les $\mathrm{Hom}_A(a, -)$ (\texttt{yonedaOpIso}), et l'on conclut de même (\texttt{isbellSpec\_unique}).
\end{proof}

\begin{remarque}
L'adjonction $\mathcal O \dashv \mathrm{Spec}$ relève de la section~\ref{sec:161-1} : ses parties fixes $E_0 \subset \widehat A$ et $F_0 \subset (A^\vee)^{\mathrm{op}}$, où l'unité et la coünité sont inversibles, sont les objets réflexifs de la dualité d'Isbell, et l'énoncé sur les points fixes de la page~4 de la cote~161-1 les met en équivalence. Le lemme~\texttt{isbellO\_yoneda} et son dual disent que les représentables sont dans ces parties fixes. La page~7 demande si ce sont les seuls et répond \q{sans doute pas} ; la réponse est juste dès que $A$ n'est pas karoubienne : l'unité d'un rétracte est un rétracte de l'unité, donc un rétracte d'un représentable est réflexif, et un tel rétracte n'est pas toujours représentable. La lecture place de même l'enveloppe de Karoubi de $A$ parmi les objets réflexifs, comme inclusion et non comme égalité. Ces deux points sont de l'édition et ne sont pas vérifiés en Lean. La dualité entre topos et sites des pages suivantes rejoint les sections~\ref{sec:19}, \ref{sec:161-1} et~\ref{sec:161-2}.
\end{remarque}

Ne sont pas démontrés ici : la roue des onze catégories de foncteurs de la page~5, l'extension aux familles finies $(A_i)$ et la dualité des topos des pages suivantes.
\bigskip
\noindent Autres pistes de l'onglet Findings pour ce thème, dans des cotes qui n'ont pas de section ici :\par

\begin{encadre}
\begin{theoreme*}[Grothendieck, pages 10 et 11, noyau de l'image réciproque et indice\piste{32-pullback-kernel-index}]\nonverifie
Soient $f : X \to Y$ propre sur un corps $k$, $Y$ irréductible et lisse de point générique $\eta$, $X_\eta$ non vide, et $N$ le pgcd des degrés des $0$-cycles de $X_\eta$. Il existe une application $H^*(X, G_X) \to H^*(Y, G)$, fonctorielle en le complexe de coefficients étale $G$, dont le composé avec $f^*$ est $N \cdot \mathrm{id}$. Le noyau de $f^*$ est donc tué par l'indice de la fibre générique, sans hypothèse sur la dimension relative.
\end{theoreme*}
\end{encadre}
{\small Le calcul de la page~10 suppose le formalisme de Gysin du \S\,4 pour des $Z_i$ éventuellement singuliers, que le dossier énonce sans le démontrer. Mathlib n'a pas la cohomologie étale. On se reportera aux notes de Grothendieck (\lot{32}{1}{10}).\par}

\begin{encadre}
\begin{theoreme*}[Grothendieck, pages 40 à 43, permanence de la condition de Lefschetz\piste{58-lef-permanence-projective-flat}]\nonverifie
Soient $X$ quasi-projectif sur un anneau noethérien et $Y$ un fermé de $X$ tels que la paire $(X, Y)$ vérifie $(\mathrm{LG})_n$ : $H^i(X, F) \to H^i(X_{/Y}, F_{/Y})$ est bijectif pour $i \leq n$ et injectif pour $i = n+1$ pour tout $F$ localement libre. Alors pour tout $f : W \to X$ projectif et plat, la paire $(W, f^{-1}(Y))$ vérifie $(\mathrm{LG})_n$ ; de même pour la condition $\mathrm{Lef}$ de SGA~2, X. Rien n'est demandé aux fibres de~$f$.
\end{theoreme*}
\end{encadre}
{\small Démonstration donnée par l'édition, non vérifiée en Lean.\par}
{\small SGA~2 (exposés X et XII) obtient ces conditions par des hypothèses de profondeur sur les fibres. Mathlib n'a pas les complétions formelles ni leur cohomologie. On se reportera aux notes de Grothendieck (\lot{58}{2}{40}).\par}

\begin{encadre}
\begin{theoreme*}[Grothendieck, pages 45 à 51, comparaison des Hom hors de $Y$\piste{58-local-hom-comparison-depth-off-y}]\nonverifie
Soient $A$ un anneau local noethérien, quotient d'un anneau régulier et $t$-adiquement complet, $X'$ son spectre épointé et $Y' = V(t) \cap X'$. Pour $F$ et $G$ cohérents sur $X'$, $\mathrm{Hom}(F, G) \simeq \mathrm{Hom}(\hat F, \hat G)$ le long de $Y'$ dès que $G$ est de profondeur $\geq 2$ aux points fermés de $X' - Y'$. Aucune profondeur n'est demandée aux points de $Y'$, alors que SGA~2, X, exemple~2.1~(i), la demande en tout point fermé de~$X'$.
\end{theoreme*}
\end{encadre}
{\small Les feuillets en esquissent une démonstration incomplète (pages 45 à 51) : la page~47 marque d'un \q{?} le pas $t$-régulier et s'arrête. Mathlib n'a pas les faisceaux cohérents sur un spectre épointé ni leur complétion formelle. On se reportera aux notes de Grothendieck (\lot{58}{3}{45}).\par}