\section[Cote 128 : descente le long d'un conducteur nilpotent, idéaux d'équivalence de rang deux]{Cote 128 : descente le long d'un conducteur nilpotent, idéaux d'équivalence de rang deux\protect\verifie{Folder128}}\label{sec:128}

La cote 128, \emph{Descente non plate. Modules formels}, trente et une pages non datées, compare le complexe d'Amitsur d'une extension $A \subset A'$ à celui de sa réduction modulo un idéal nilpotent. Sept pages (12 à 18) y traitent de \q{résultats auxiliaires sur les relations d'équivalence}. La proposition~1 de la page~12 affirme que, si $A'/A$ est isomorphe au corps résiduel $k = A/\mathfrak m$, il n'y a sur $\operatorname{Spec} A'$, au-dessus de $\operatorname{Spec} A$, que deux relations d'équivalence : la plus fine et la moins fine (\lot{128}{1}{12}). La page~13 ramène l'énoncé au cas où $A = k$ est un corps et $A'$ une $k$-algèbre de rang~$2$, traite $k \times k$ et s'arrête sur \q{$A' \simeq k[\varepsilon]$} (\lot{128}{1}{13}). On démontre ici ce cas d'un corps et la réduction qui y ramène le cas local, puis, à la fin de la section, le résultat de descente des pages 4 à~9 : la descente plate effective se remonte le long d'un idéal nilpotent contenu dans le conducteur.

\noindent\emph{Idéaux d'équivalence.} Sur un ensemble $X$, une relation d'équivalence est une partie $R \subset X \times X$ qui contient la diagonale, est stable par l'échange $(x, y) \mapsto (y, x)$ et vérifie : si $(x, y)$ et $(y, z)$ sont dans $R$, $(x, z)$ aussi. Pour $X = \operatorname{Spec} A$ au-dessus d'un corps $k$, le produit $X \times_k X$ est $\operatorname{Spec}(A \otimes_k A)$, et un sous-schéma fermé de ce produit est donné par un idéal $J$ de $A \otimes_k A$, d'autant plus petit que le sous-schéma est gros. Les trois axiomes se traduisent alors ainsi (la lecture les énonce après la proposition~3 du n\textsuperscript{o}~1, pages 9 à~11) :
\begin{itemize}
\item réflexivité : $R$ contient la diagonale, c'est-à-dire $J \subset \Delta = \operatorname{Ker}(A \otimes_k A \to A, \ a \otimes b \mapsto ab)$ ;
\item symétrie : $J$ est stable par l'échange $a \otimes b \mapsto b \otimes a$ ;
\item transitivité : $p_{13}(J) \subset p_{12}(J) + p_{23}(J)$ dans $A \otimes_k A \otimes_k A$, où $p_{12}(a \otimes b) = a \otimes b \otimes 1$, $p_{13}(a \otimes b) = a \otimes 1 \otimes b$ et $p_{23}(a \otimes b) = 1 \otimes a \otimes b$ engendrent des idéaux.
\end{itemize}
La dernière condition dit que le sous-schéma de $X^3$ formé des $(x, y, z)$ avec $(x, y) \in R$ et $(y, z) \in R$ s'envoie dans $R$ par $(x, y, z) \mapsto (x, z)$. Les deux idéaux extrêmes sont $J = \Delta$, la diagonale, relation la plus fine, et $J = 0$, le produit tout entier, relation la moins fine.

\noindent\emph{L'intuition.} Une $k$-algèbre de rang~$2$ est un \q{schéma à deux points}, au sens géométrique : deux points distincts ($k \times k$), un point double ($k[\varepsilon]$, $\varepsilon^2 = 0$), ou un seul point de degré~$2$ (une extension quadratique de $k$). Pour deux points, la question est celle des relations d'équivalence sur un ensemble à deux éléments, et il y en a deux. Pour le point double, on pourrait craindre une relation intermédiaire, qui identifierait le point à lui-même \q{à l'ordre un} sans l'identifier à son vecteur tangent ; la transitivité l'interdit (figure~\ref{fig:128-rang-deux}).

\begin{figure}[htbp]
\centering
\begin{tikzpicture}[x=1cm, y=1cm, >=stealth, every node/.style={font=\small}]
% Spec(k x k) : deux points, le carré a quatre points
\draw[black!35] (0,-0.5) -- (2.6,-0.5) (-0.5,0) -- (-0.5,2.6);
\foreach \x/\l in {0.6/x, 2/y} { \fill (\x,-0.5) circle (1.6pt); \node[below] at (\x,-0.5) {$\l$}; \fill (-0.5,\x) circle (1.6pt); \node[left] at (-0.5,\x) {$\l$}; }
\draw[frise, thick, dashed] (0.2,0.2) -- (2.4,2.4) node[above right=-2pt] {$\Delta$};
\foreach \x in {0.6, 2} \foreach \y in {0.6, 2} \draw[fill=white] (\x,\y) circle (2.2pt);
\fill[frise] (0.6,0.6) circle (2.2pt) (2,2) circle (2.2pt);
\node[align=center] at (1.05,-1.55) {$\operatorname{Spec}(k \times k)$ : \\ $0$ garde les quatre points, \\ $\Delta$ les deux de la diagonale};
% Spec(k[eps]) : un point double ; trois sous-schémas du carré
\begin{scope}[xshift=5.2cm]
\foreach \c/\t/\col/\q/\ds/\dd in {0/{$J = 0$}/black/1/1/0, 3.2/{$J = k\,\varepsilon_1\varepsilon_2$}/piste/0/1/0, 6.4/{$J = \Delta$}/frise/0/0/1} {
  \begin{scope}[xshift=\c cm]
  \ifnum\q=1 \fill[black!15] (0,0) rectangle (1.1,1.1); \fi
  \ifnum\ds=1 \draw[->, thick, \col] (0,0) -- (1.5,0) node[below] {$\varepsilon_1$}; \draw[->, thick, \col] (0,0) -- (0,1.5) node[left] {$\varepsilon_2$}; \fi
  \ifnum\dd=1 \draw[->, thick, \col] (0,0) -- (1.2,1.2) node[above right=-2pt] {$\varepsilon_1 = \varepsilon_2$}; \fi
  \fill (0,0) circle (2pt);
  \node[\col] at (0.75,-0.75) {\t};
  \end{scope}
}
\node[align=center] at (4,-1.55) {$\operatorname{Spec}(k[\varepsilon] \otimes_k k[\varepsilon]) = \operatorname{Spec} k[\varepsilon_1, \varepsilon_2]/(\varepsilon_1^2, \varepsilon_2^2)$ : un seul point, \\ avec ses directions tangentes $\varepsilon_1$, $\varepsilon_2$ et le terme croisé $\varepsilon_1 \varepsilon_2$ (en gris)};
\end{scope}
\end{tikzpicture}
\caption{Les sous-schémas du carré $\operatorname{Spec}(A \otimes_k A)$ pour les deux modèles de rang~$2$. Pour $k \times k$, deux points, les relations $0$ et $\Delta$ sont le carré entier et sa diagonale. Pour $k[\varepsilon]$, un point double, le carré est un seul point épaissi ; $\Delta$ ne garde que la direction diagonale, et l'idéal intermédiaire $k\,\varepsilon_1\varepsilon_2$ ôte le seul terme croisé. Il n'est pas transitif : dans $A^{\otimes 3}$, placer le point du milieu à l'origine annule $\varepsilon_1\varepsilon_2$ et $\varepsilon_2\varepsilon_3$, mais pas $\varepsilon_1\varepsilon_3$.}
\label{fig:128-rang-deux}
\end{figure}

\begin{theoreme}[Grothendieck, page 12, proposition~1 (i), cas d'un corps]\label{thm:128-deux}
Soient $k$ un corps et $A$ une $k$-algèbre commutative de dimension~$2$. Les idéaux d'équivalence de $A \otimes_k A$ sont exactement $0$ et~$\Delta$.
\end{theoreme}

\begin{proof}
Les deux idéaux $0$ et $\Delta$ sont d'équivalence : pour $\Delta$, la symétrie vient de la commutativité de $A$, et la transitivité de l'identité $p_{13}(\delta s) = p_{12}(\delta s) + p_{23}(\delta s)$, où $\delta s = 1 \otimes s - s \otimes 1$, ces éléments engendrant~$\Delta$.

Réciproquement, soit $J$ un idéal d'équivalence. Pour $x \in A$ hors de $k$, $(1, x)$ est une base de $A$, et $\Delta = A \cdot \delta x$ : le $A$-module $\Delta$ est engendré par les $\delta s$, et $\delta(c + dx) = d\,\delta x$. Tout élément de $J$ s'écrit donc $a \cdot \delta x = a \otimes x - ax \otimes 1$, et il suffit de montrer que $J = 0$ ou que $\delta x \in J$ pour un tel~$x$.

Si tout élément non nul de $A$ est inversible, un élément non nul $a \cdot \delta x$ de $J$ donne $\delta x = a^{-1} \cdot (a \cdot \delta x) \in J$. Sinon, soit $e$ non nul et non inversible ; il n'est pas dans $k$, et $e^2 = s + re$ avec $s, r \in k$. Si $s \neq 0$, $e \cdot s^{-1}(e - r) = 1$ ; donc $s = 0$ et $e^2 = re$.

Si $r \neq 0$, $f = e/r$ est un idempotent hors de $k$ (c'est le cas $k \times k$). Un élément de $J$ s'écrit $t = c\,(1 \otimes f) + d\,(f \otimes f) - (c + d)(f \otimes 1)$. On calcule $(f \otimes 1)\,t = (c + d)\,w_1$ et $(1 \otimes 1 - f \otimes 1)\,t = c\,w_2$, avec $w_1 = f \otimes f - f \otimes 1$ et $w_2 = 1 \otimes f - f \otimes f$. Si $t \neq 0$, l'un des scalaires $c + d$, $c$ est non nul, donc $w_1$ ou $w_2$ est dans~$J$. Or $w - \sigma(w) = \delta f$ pour $w = w_1$ comme pour $w = w_2$, où $\sigma$ est l'échange, et la symétrie donne $\delta f \in J$.

Si $r = 0$, $e^2 = 0$ (c'est le cas $k[\varepsilon]$). Un élément de $J$ s'écrit $t = c\,\delta e + d\,(e \otimes e)$, et $(e \otimes 1)\,t = c\,(e \otimes e)$. Supposons $\delta e \notin J$. Si $c \neq 0$, $e \otimes e \in J$, puis $c\,\delta e = t - d\,(e \otimes e) \in J$, contradiction ; donc $J \subset k\,(e \otimes e)$. Si de plus $J \neq 0$, $e \otimes e \in J$. Soit $\chi : A \to k$ le caractère $c + de \mapsto c$, et $\varphi : A^{\otimes 3} \to A^{\otimes 2}$ le morphisme d'algèbres $a \otimes b \otimes c \mapsto \chi(b)\, a \otimes c$, qui \q{oublie le point du milieu}. Il annule $p_{12}(e \otimes e) = e \otimes e \otimes 1$ et $p_{23}(e \otimes e) = 1 \otimes e \otimes e$, donc les idéaux $p_{12}(J)$ et $p_{23}(J)$, mais envoie $p_{13}(e \otimes e) = e \otimes 1 \otimes e$ sur $e \otimes e \neq 0$. La transitivité est en défaut ; donc $J = 0$.

Dans tous les cas, $J = 0$ ou $\delta x \in J$ pour un $x \notin k$, et alors $\Delta = A \cdot \delta x \subset J \subset \Delta$.
\end{proof}

\begin{remarque}
La démonstration n'utilise ni la clôture algébrique de $k$, que la page s'accorde en interligne, ni la classification des algèbres de rang~$2$ : elle couvre d'un coup les extensions quadratiques, séparables ou non. Le cas $k[\varepsilon]$, que la page laisse après \q{$\varepsilon^2 = 0$}, est celui de la lecture : l'idéal $k\,\varepsilon_1\varepsilon_2$ est réflexif et symétrique, mais pas transitif. Le cas $k \times k$ se règle, lui, par la seule symétrie : les idéaux $k\,(f \otimes (1 - f))$ et $k\,((1 - f) \otimes f)$, réflexifs et transitifs, correspondent aux deux relations non symétriques d'un ensemble à deux éléments.
\end{remarque}

\noindent\emph{Portée de la vérification.} Lean formalise la définition des idéaux d'équivalence par les trois conditions ci-dessus, pour $A$ commutative de dimension~$2$ sur un corps quelconque, et démontre le théorème~\ref{thm:128-deux} dans les deux sens. L'idéal $\Delta$ y est le noyau de la multiplication \texttt{Algebra.\allowbreak{}TensorProduct.\allowbreak{}lmul'}, et les $\delta s$ l'engendrent comme $A$-module par un résultat de mathlib qui sert à définir les différentielles de Kähler.

La partie difficile de la proposition~1 (i) est la réduction du cas général au cas d'un corps. Elle passe par la proposition~3 du n\textsuperscript{o}~1 et son corollaire~2 (pages 9 à~11) : la réduction modulo $\mathfrak m$ induit une bijection entre les idéaux d'équivalence de $A' \otimes_A A'$ et ceux de $A'_0 \otimes_k A'_0$, parce que l'idéal d'augmentation se réduit isomorphiquement (lemme du serpent). Cette réduction est démontrée plus bas, pour $I = \mathfrak m$ et dans le sens qui sert (théorème~\ref{thm:128-prop1}) ; ni la traduction entre idéaux et sous-schémas fermés, ni les points (ii) et (iii) de la proposition ne sont formalisés.

\noindent\emph{Le critère sur un corps.} Prenons $A = k$ et notons, comme dans le théorème~\ref{thm:128-deux}, $A$ l'algèbre finie (le $A'$ de la page). L'hypothèse \q{$\delta(x)$ engendre l'idéal $\Delta$ de $A'' = (A \otimes_k A)/J$} se lit dans $A \otimes_k A$ : $\Delta \subset (\delta x) + J$. L'exactitude de $k \to A \rightrightarrows A''$ dit que $\delta x \in J$ seulement pour $x \in k$. Les feuillets distinguent deux cas : $A$ non radiciel, ramené à $k^n$ où un décompte donne $n = 2$, et $A$ radiciel, ramené à $k \oplus V$ avec $V^2 = 0$, où la page~18 s'arrête sur \q{il faut prouver} $\dim V = 1$. La démonstration ci-dessous évite cette distinction : elle regarde $J$ point par point.

\begin{theoreme}[Grothendieck, pages 14 à 18, proposition~2, cas d'un corps]\label{thm:128-colongueur}
Soient $k$ un corps, $A$ une $k$-algèbre commutative de dimension finie dont tous les corps résiduels sont $k$, et $J \subset \Delta$ un idéal de $A \otimes_k A$. On suppose que $\delta x \in J$ entraîne $x \in k$, et que $\Delta \subset (\delta x) + J$ pour tout $x \notin k$. Alors $\dim_k A \leq 2$, c'est-à-dire $\mathrm{long}(A/k) \leq 1$. Si de plus $J$ est un idéal d'équivalence et $\dim_k A = 2$, alors $J = 0$, c'est-à-dire $A'' = A \otimes_k A$.
\end{theoreme}

\begin{proof}
Un point $\chi : A \to k$ (un morphisme de $k$-algèbres, d'idéal $\mathfrak m_\chi = \operatorname{Ker} \chi$) donne le morphisme $\varphi_\chi : A \otimes_k A \to A$, $a \otimes b \mapsto \chi(a)\, b$, qui \q{fixe le premier point en $\chi$}. Il envoie $\delta x$ sur $x - \chi(x)$, et $\Delta$ dans $\mathfrak m_\chi$. Pour $0 \neq z \in \mathfrak m_\chi$ (donc $z \notin k$) et $y \in \mathfrak m_\chi$, écrivons $\delta y = u\, \delta z + j$ avec $j \in J$ ; en appliquant $\varphi_\chi$, $y = \varphi_\chi(u)\, z + \varphi_\chi(j)$. Ainsi $\mathfrak m_\chi \subset A z + \varphi_\chi(J)$.

Premier cas : $\varphi_\chi(J) = 0$ pour un point $\chi$. Alors tout $z \neq 0$ de $\mathfrak m_\chi$ l'engendre. Si $\mathfrak m_\chi = 0$, $A = k$. Sinon, soit $z \neq 0$ dans $\mathfrak m_\chi$ et $\mathfrak n$ un idéal maximal contenant l'annulateur de $z$ ; c'est le noyau d'un point $\chi'$. Pour $w \in \mathfrak n$, si $wz \neq 0$, il engendre $\mathfrak m_\chi$ : $z = bwz$, donc $1 - bw$ annule $z$ et serait dans $\mathfrak n$ avec $bw$, absurde. Donc $\mathfrak n z = 0$, et $bz = \chi'(b)\, z$ pour tout $b$ : $\mathfrak m_\chi = kz$ et $A = k \oplus kz$.

Second cas : $\mathfrak m_\chi \subset \varphi_\chi(J)$ pour tout $\chi$ (si $\varphi_\chi(J)$ contient $y_0 \neq 0$, on prend $z = y_0$ ci-dessus). Pour $f \in \Delta$, $f \equiv \delta(\varphi_\chi f)$ modulo $\mathfrak m_\chi \Delta$ (où $A$ agit sur le premier facteur) : c'est vrai pour $f = \delta s$, car $\delta$ s'annule sur $k$, et le passage à $a \cdot f$ ajoute $(a - \chi(a)) \cdot f \in \mathfrak m_\chi \Delta$. Pour $x \in A$, choisissons $f \in J$ avec $\varphi_\chi(f) = x - \chi(x)$ ; alors $\delta x = \delta(\varphi_\chi f) \in J + \mathfrak m_\chi \Delta$. Ainsi $\Delta \subset J + \mathfrak m \Delta$ pour tout idéal maximal $\mathfrak m$, puisque tous sont des $\mathfrak m_\chi$. Par le lemme de Nakayama, appliqué en chaque idéal maximal au $A$-module de type fini $(\Delta + J)/J$, $\Delta \subset J$ ; l'exactitude donne alors $x \in k$ pour tout $x$, soit $A = k$.

Enfin, si $\dim_k A = 2$ et si $J$ est un idéal d'équivalence, le théorème~\ref{thm:128-deux} donne $J = 0$ ou $J = \Delta$, et $J = \Delta$ contredirait l'exactitude.
\end{proof}

\begin{remarque}
La première assertion n'utilise de $J$ que l'inclusion $J \subset \Delta$ : ni la symétrie, ni la transitivité, ni la nilpotence de $J$ que la page souligne sans la justifier. Le décompte \q{$2(n-1) = n^2 - n$} du cas non radiciel et le calcul de $\dim V$ de la page~18 sont deux instances du premier cas, $\varphi_\chi(J) = 0$ ; le second cas est celui où la relation ne relie $\chi$ à aucun autre point, ni infinitésimalement.
\end{remarque}

\noindent\emph{Portée de la vérification.} Lean démontre le théorème~\ref{thm:128-colongueur} sous ces hypothèses (\texttt{Colength.\allowbreak{}finrank\_le\_two}, \texttt{Colength.\allowbreak{}eq\_bot\_of\_finrank\_eq\_two}, réunis dans \texttt{Colength.\allowbreak{}prop2}) ; l'hypothèse sur les corps résiduels y est écrite \q{tout idéal maximal est le noyau d'un morphisme $A \to k$}, et le lemme de Nakayama en tout idéal maximal y est \texttt{Colength.\allowbreak{}le\_of\_forall\_le\_sup\_smul}. La réduction du cas local au cas d'un corps fait l'objet du théorème suivant.

\noindent\emph{Du cas local au cas d'un corps.} Revenons à l'énoncé de la page~14 : $A$ local artinien d'idéal maximal $\mathfrak m$, $k = A/\mathfrak m$, et $A'$ une $A$-algèbre finie. Les idéaux d'équivalence de $A' \otimes_A A'$ se définissent comme plus haut, $\otimes_k$ devenant $\otimes_A$, et $\delta x = 1 \otimes x - x \otimes 1$. La page obtient $\mathfrak m A' = \mathfrak m$ par sa distinction radiciel / non radiciel, en s'appuyant sur la nilpotence de $J$, puis réduit modulo $\mathfrak m$ par la proposition~3 du n\textsuperscript{o}~1 et son corollaire~2 (pages 9 à~11), qui identifient l'idéal d'augmentation $\Delta$ à celui de $A'_0 = A'/\mathfrak m A'$ et transportent les idéaux d'équivalence. On suit ici la même réduction, mais $\mathfrak m A' = \mathfrak m$ se lit directement sur l'hypothèse, et l'argument point par point du théorème~\ref{thm:128-colongueur} se fait dans $A'_0$ sans passer par $A'_0 \otimes_k A'_0$.

\begin{theoreme}[Grothendieck, pages 14 à 18, proposition~2\piste{128-colength-one-equivalence-criterion}]\label{thm:128-local}
Soient $A$ un anneau noethérien, $\mathfrak m$ un idéal maximal de $A$, $k = A/\mathfrak m$, et $A'$ une $A$-algèbre finie dont tout idéal maximal est le noyau d'un morphisme de $A$-algèbres $A' \to k$ (c'est le cas si $A$ est local artinien d'idéal maximal $\mathfrak m$ et si les extensions résiduelles de $A'$ sont triviales). Soit $J \subset \Delta$ un idéal de $A' \otimes_A A'$ ; on suppose que $\delta x \in J$ entraîne $x \in A$ (exactitude de $A \to A' \rightrightarrows (A' \otimes_A A')/J$), et que $\Delta \subset (\delta x) + J$ pour tout $x \notin A$. Alors :
\begin{enumerate}
\item $\mathfrak m A'$ est contenu dans l'image de $A$ ; si $A \to A'$ est injectif, $\mathfrak m A' = \mathfrak m$ ;
\item $A'/A$ est de longueur au plus~$1$ ;
\item si de plus $J$ est un idéal d'équivalence et si $A'/A$ est de longueur~$1$, alors $J = 0$, c'est-à-dire $(A' \otimes_A A')/J = A' \otimes_A A'$.
\end{enumerate}
\end{theoreme}

\begin{proof}[Esquisse]
Point~1. Tout idéal maximal $\mathfrak n$ de $A'$ est le noyau d'un point $\chi : A' \to k$, donc contient $\mathfrak m A'$. Si $x \in \mathfrak m A'$ n'était pas dans $A$, on aurait $\delta x \in \mathfrak m \Delta \subset \mathfrak n \Delta$ (car $\delta$ est $A$-linéaire et nul sur $A$), où $A'$ agit sur le premier facteur ; l'hypothèse donnerait $\Delta \subset (\delta x) + J \subset J + \mathfrak n \Delta$ pour tout $\mathfrak n$, donc $\Delta \subset J$ par le lemme de Nakayama en chaque idéal maximal de $A'$ ($\Delta$ est de type fini, $A'$ étant noethérien), et l'exactitude mettrait $x$ dans $A$.

Point~2. Pour un point $\chi$, le morphisme $\varphi_\chi : A' \otimes_A A' \to A'_0$, $a \otimes b \mapsto \chi(a)\, \bar b$, envoie $\delta x$ sur $\bar x - \chi(x)$, et l'on refait la démonstration du théorème~\ref{thm:128-colongueur} dans la $k$-algèbre finie $A'_0$, dont les corps résiduels sont $k$. Ou bien $\varphi_\chi(J) = 0$ pour un $\chi$, et l'idéal maximal de $\chi$ dans $A'_0$ est simple, d'où $\dim_k A'_0 \leq 2$. Ou bien, pour tout $\chi$, cet idéal est contenu dans $\varphi_\chi(J)$ ; la congruence $f \equiv \delta(\varphi_\chi f)$ du cas d'un corps est remplacée par : tout $t \in \Delta$ est congru à un $\delta s$ modulo $\mathfrak n_\chi \Delta$ (on écrit $a = \lambda + (a - \lambda)$ avec $\lambda \in A$ relevant $\chi(a)$). Pour $x \in A'$, prenons $f \in J$ avec $\varphi_\chi(f) = \bar x - \chi(x)$ et $s$ avec $f \equiv \delta s$ ; comme $\varphi_\chi$ annule $\mathfrak n_\chi \Delta$, $\bar x - \bar s \in k$, donc $x - s \in A + \mathfrak m A'$ et $\delta x \equiv \delta s \equiv f$ modulo $\mathfrak n_\chi \Delta$. Ainsi $\Delta \subset J + \mathfrak n \Delta$ pour tout $\mathfrak n$, puis $\Delta \subset J$ et $A' = A$. Dans le premier cas, soit $z \notin A$ : par le point~1, $1$ et $\bar z$ sont libres dans $A'_0$, donc en forment une base, et $A' = A + Az + \mathfrak m A' = A + Az$ ; tout élément non nul de $A'/A$ l'engendre, et la longueur vaut au plus~$1$.

Point~3. Soit $\Theta : A' \otimes_A A' \to A'_0 \otimes_k A'_0$ la réduction modulo $\mathfrak m$. Son noyau est contenu dans $\mathfrak m (A' \otimes_A A')$ (exactitude à droite du produit tensoriel) ; et comme $\mathfrak m A' \subset A$, $\mu (a \otimes b) = (\mu a) \otimes b = 1 \otimes \mu a b$ pour $\mu \in \mathfrak m$, de sorte que tout élément $t$ de $\mathfrak m(A' \otimes_A A')$ vaut $1 \otimes t'$ où $t'$ est son image par la multiplication : il est nul s'il est dans $\Delta$. Ainsi $\Theta$ est injectif sur $\Delta$ ; c'est la proposition~3 du n\textsuperscript{o}~1 pour $I = \mathfrak m$. Comme $\Theta$ commute à l'échange, à la multiplication et aux $p_{ij}$, $\Theta(J)$ est un idéal d'équivalence (corollaire~2, dans le sens qui sert). La longueur~$1$ fournit $z \notin A$, et le point~2 donne $\dim_k A'_0 = 2$. Par le théorème~\ref{thm:128-deux}, $\Theta(J) = 0$, d'où $J = 0$ par injectivité, ou $\Theta(J) = \Delta_0$ ; dans ce cas $\Theta(\delta z) = \Theta(j)$ pour un $j \in J$, donc $\delta z = j \in J$, contre l'exactitude.
\end{proof}

\begin{theoreme}[Grothendieck, pages 12 et 13, proposition~1 (i)\piste{128-colength-one-equivalence-criterion}]\label{thm:128-prop1}
Soient $A$ un anneau, $\mathfrak m$ un idéal maximal, $k = A/\mathfrak m$, et $A \subset A'$ une $A$-algèbre telle que $A'/A \simeq k$ comme $A$-modules. Les idéaux d'équivalence de $A' \otimes_A A'$ sont exactement $0$ et $\Delta$.
\end{theoreme}

\begin{proof}[Esquisse]
Comme $\mathfrak m$ annule $A'/A$, $\mathfrak m A' \subset A$. Soit $z$ relevant $1 \in k$ : tout $y$ s'écrit $\lambda + \nu z$ avec $\lambda, \nu \in A$, donc $1, \bar z$ engendrent $A'_0$, et ils sont libres puisque $z \notin A + \mathfrak m A'$ ; $\dim_k A'_0 = 2$. Pour un idéal d'équivalence $J$, $\Theta(J)$ est un idéal d'équivalence de $A'_0 \otimes_k A'_0$, donc $0$ ou $\Delta_0$ (théorème~\ref{thm:128-deux}). Dans le premier cas $J = 0$ par injectivité de $\Theta$ sur $\Delta$. Dans le second, tout $d \in \Delta$ a son image dans $\Delta_0 = \Theta(J)$, donc $d - j \in \Delta$ est d'image nulle pour un $j \in J$, et $d = j$ : $J = \Delta$. Réciproquement $0$ et $\Delta$ sont des idéaux d'équivalence, comme sur un corps.
\end{proof}

\begin{remarque}
Ni la nilpotence de $J$, que la page souligne sans la justifier, ni la distinction radiciel / non radiciel, ni la différentielle $d : A' \to \Delta/\Delta^2$ ne servent ; les points~1 et~2 n'utilisent de $J$ que l'inclusion $J \subset \Delta$. L'anneau de base n'a pas à être local ni artinien : il suffit qu'il soit noethérien et que tous les points de $A'$ soient rationnels au-dessus d'un même idéal maximal. La proposition~1 (i) vaut sur un anneau quelconque, sans finitude ; c'est l'énoncé de la page~12, que la page~13 ramène au cas d'un corps sans plus de détail.
\end{remarque}

\noindent\emph{Portée de la vérification.} Lean démontre le théorème~\ref{thm:128-local} sous ces hypothèses (\texttt{ColengthLocal.\allowbreak{}map\_le\_range} pour le point~1, \texttt{ColengthLocal.\allowbreak{}colength\_le\_one} pour les points 1 et~2, \texttt{ColengthLocal.\allowbreak{}eq\_bot\_of\_length\_eq\_one} pour le point~3, réunis pour $A$ local noethérien dans \texttt{ColengthLocal.\allowbreak{}prop2}), la longueur étant \texttt{Module.\allowbreak{}length} ; l'alternative du point~2 est \texttt{ColengthLocal.\allowbreak{}finrank\_le\_two\_or}, la congruence modulo $\mathfrak n \Delta$ \texttt{ColengthLocal.\allowbreak{}exists\_sub\_dl\_mem}, la réduction $\Theta$ \texttt{ColengthLocal.\allowbreak{}theta}, son injectivité sur $\Delta$ \texttt{ColengthLocal.\allowbreak{}eq\_zero\_of\_theta}, et le transport des idéaux d'équivalence \texttt{ColengthLocal.\allowbreak{}isEquivalenceIdeal\_map}. Il démontre le théorème~\ref{thm:128-prop1} (\texttt{ColengthLocal.\allowbreak{}prop1\_i}, avec \texttt{ColengthLocal.\allowbreak{}isEquivIdeal\_bot} et \texttt{ColengthLocal.\allowbreak{}isEquivIdeal\_diag}). Ne sont pas formalisés : la proposition~3 du n\textsuperscript{o}~1 et son corollaire~2 pour un idéal nilpotent $I$ quelconque du conducteur (seul le cas $I = \mathfrak m$, $\mathfrak m A' \subset A$, et le sens de $A'$ vers $A'_0$ le sont), les points (ii) et (iii) de la proposition~1, et la traduction entre idéaux et sous-schémas fermés.


\noindent\emph{Descente le long d'un conducteur nilpotent.} Revenons aux pages 4 à~9 (\lot{128}{1}{4}). Soient $A \to A'$ un morphisme d'anneaux commutatifs et $I$ un idéal de $A$ que $\lambda \mapsto \lambda \cdot 1$ envoie injectivement sur un idéal de $A'$ : $I$ est contenu dans le conducteur, et le carré formé de $A$, $A'$, $A_0 = A/I$, $A'_0 = A'/IA'$ est cartésien (un carré de Milnor). Une \emph{donnée de descente} sur un $A'$-module $E'$ relativement à $A \to A'$ est un isomorphisme $\varphi : A' \otimes_A E' \to E' \otimes_A A'$ satisfaisant la condition de cocycle ; on l'écrit ici par la coaction $\psi(e) = \varphi(1 \otimes e) = \sum b_i \otimes e_i$, application $A'$-linéaire $E' \to A' \otimes_A E'$ soumise à deux conditions : la counité $\sum b_i e_i = e$ et le cocycle $\sum b_i \otimes \psi(e_i) = \sum b_i \otimes 1 \otimes e_i$. Les invariants $E = \{e \mid \psi(e) = 1 \otimes e\}$ forment le $H^0$ du complexe de descente, et la donnée est \emph{effective} si $E$ est plat sur $A$ et si $A' \otimes_A E \to E'$ est bijectif : elle est alors celle de $A' \otimes_A E$. Un morphisme $\operatorname{Spec} A' \to \operatorname{Spec} A$ est de \emph{descente effective pour les modules plats} si $M \to H^0(A'/A, M)$ est bijectif pour tout $A$-module plat $M$ et si toute donnée de descente sur un $A'$-module plat est effective. Une donnée sur $E'$ en induit une sur $E'_0 = A'_0 \otimes_{A'} E'$ relativement à $A_0 \to A'_0$, sa réduction.

\begin{theoreme}[Grothendieck, pages 4 à 7, proposition~2 et corollaire~1\piste{128-nilpotent-conductor-flat-descent}]\label{thm:128-descente}
Soient $A \to A'$ et $I$ comme ci-dessus, avec $I$ nilpotent.
\begin{enumerate}
\item Si $E'$ est un $A'$-module plat muni d'une donnée de descente dont la réduction modulo $I$ est effective, la donnée est effective.
\item Si $\operatorname{Spec} A'_0 \to \operatorname{Spec} A_0$ est un morphisme de descente effective pour les modules plats, $\operatorname{Spec} A' \to \operatorname{Spec} A$ l'est aussi.
\end{enumerate}
\end{theoreme}

\begin{proof}
On note $\pi : E' \to E'_0$ la réduction, $E$ et $E_0$ les invariants de $E'$ et de $E'_0$. Le fait de base est que, $IA'$ étant égal à l'image de $I$, on a dans $A' \otimes_A N$, pour tout $A$-module $N$, $\lambda b \otimes n = 1 \otimes \lambda_b n$ avec $\lambda_b \in I$ : tout élément de $IA' \cdot (A' \otimes_A N)$ s'écrit $1 \otimes y$ avec $y \in IN$.

Étape 1 : $e$ est invariant si et seulement si $\pi(e)$ l'est. Si $\pi(e)$ est invariant, $\psi(e) - 1 \otimes e$ s'annule modulo $I$, donc vaut $1 \otimes y$ ; en appliquant la counité, $e - e = y$, d'où $y = 0$. C'est le calcul de la page~5, qui n'utilise ni $I^2 = 0$ ni la platitude. Ainsi $E \to E_0$ est surjectif, de noyau $IE'$.

Étape 2 : par l'effectivité modulo $I$, $E'_0$ est engendré par $E_0$, donc $E' = A' E + IE'$, et $E' = A'E$ par le lemme de Nakayama pour l'idéal nilpotent $IA'$ ; on en tire aussi $IE' = IE$. L'application $A' \otimes_A E \to E'$ est donc surjective.

Étape 3 : elle est injective. Un élément $t$ de son noyau a une réduction dans $A'_0 \otimes_{A_0} E_0$ qui s'envoie sur $\pi(0) = 0$, donc est nulle par l'effectivité modulo $I$ ; $t$ est alors dans $IA' \cdot (A' \otimes_A E)$, de la forme $1 \otimes y$, et son image $y$ est nulle.

Étape 4 : $E$ est plat. D'une part $E/IE \simeq E_0$ est plat sur $A_0$. D'autre part $I \otimes_A E \simeq I \otimes_{A'} (A' \otimes_A E) \simeq I \otimes_{A'} E' \to E'$ est injectif, $E'$ étant plat sur $A'$ ; c'est le seul usage de cette platitude. Le critère local de platitude pour un idéal nilpotent conclut : si $M/IM$ est plat sur $A/I$ et $I \otimes_A M \to M$ injectif, $M$ est plat. On le démontre sans hypothèse noethérienne, en remontant une filtration $J \subset J + I^{n-1} \subset \cdots \subset A$ de chaque idéal $J$ et en ramenant chaque cran, tué par $I$, à un module libre.

Pour le point 2, l'effectivité se déduit du point 1 appliqué à la réduction de la donnée. Pour $M$ plat sur $A$, on applique l'hypothèse à $M_0 = A_0 \otimes_A M$ : si $1 \otimes m = 0$ dans $A' \otimes_A M$, alors $m \in IM$, provient de $I \otimes_A M$, qui s'injecte dans $A' \otimes_A M$ par platitude, d'où $m = 0$ ; et un invariant $x$ de $A' \otimes_A M$ a une réduction de la forme $1 \otimes m_0$, d'où $x - 1 \otimes m = 1 \otimes y$ par l'étape~1 et $x = 1 \otimes (m + y)$.
\end{proof}

\begin{remarque}
La page procède autrement : elle traite le cas $I^2 = 0$ par la suite exacte de cohomologie de $0 \to I\,C^\bullet_D \to C^\bullet_D(A'/A, E') \to C^\bullet_D(A'_0/A_0, E'_0) \to 0$, puis raisonne par récurrence sur l'ordre de nilpotence. L'étape~1 montre que cette récurrence n'est pas nécessaire. Comme le note la lecture, les hypothèses $A \simeq H^0(A'/A)$ et $H^1(A'/A) = 0$ de l'énoncé ne servent pas au point~1. Le dernier pas de la page~6, l'isomorphisme $E \otimes_A A' \to E'$, presque illisible, est ici l'étape~3, qui ne demande pas la platitude de $E'$.
\end{remarque}

\begin{theoreme}[Grothendieck, page 7, exemple du corollaire~1\piste{128-nilpotent-conductor-flat-descent}]\label{thm:128-fid-plat}
\begin{enumerate}
\item Si $A \to A'$ est plat, $A' \otimes_A E \to E'$ est bijectif pour toute donnée de descente sur un $A'$-module $E'$, $E$ désignant ses invariants.
\item Si $A \to A'$ est fidèlement plat, $\operatorname{Spec} A' \to \operatorname{Spec} A$ est un morphisme de descente effective pour les modules plats.
\item Soient $A \to A'$ et $I$ comme au théorème~\ref{thm:128-descente}, $I$ nilpotent. Si $A'_0$ est fidèlement plat sur $A_0$, $\operatorname{Spec} A' \to \operatorname{Spec} A$ est un morphisme de descente effective pour les modules plats.
\end{enumerate}
\end{theoreme}

\begin{proof}
Point 1. Soit $f = \psi - (1 \otimes \cdot) : E' \to A' \otimes_A E'$, $A$-linéaire, de noyau $E$. Le cocycle dit que $\psi(e)$ est annulé par $A' \otimes f$ ; $A'$ étant plat, le noyau de $A' \otimes f$ est l'image de $A' \otimes_A E$, qui s'injecte dans $A' \otimes_A E'$. On écrit donc $\psi(e) = j(t)$, avec $j : A' \otimes_A E \hookrightarrow A' \otimes_A E'$, et la counité donne $\theta(t) = e$ pour $\theta : A' \otimes_A E \to E'$ : $\theta$ est surjectif. Pour $x$ invariant, $\psi(\theta(b \otimes x)) = b \psi(x) = b \otimes x = j(b \otimes x)$, donc $j = \psi \circ \theta$, et $\theta$ est injectif puisque $j$ l'est.

Point 2. Pour $M$ un $A$-module, $M \to A' \otimes_A M$ est injectif par fidèle platitude. Si $E'$ est plat sur $A'$, $A' \otimes_A E \simeq E'$ est plat sur $A'$, donc $E$ est plat sur $A$ (la platitude descend le long d'un morphisme fidèlement plat) : la donnée est effective. Enfin, pour la donnée canonique sur $A' \otimes_A M$, d'invariants $N$, l'application $\iota : M \to N$, $m \mapsto 1 \otimes m$, vérifie $\theta \circ (A' \otimes \iota) = \mathrm{id}$ ; $\theta$ étant bijectif par le point~1, $A' \otimes \iota$ est surjectif, donc $\iota$ aussi par fidèle platitude : $M \simeq H^0(A'/A, M)$.

Point 3. C'est le point~2 du théorème~\ref{thm:128-descente}, dont l'hypothèse est donnée par le point~2 appliqué à $A_0 \to A'_0$.
\end{proof}

La démonstration est la descente fidèlement plate classique, écrite directement sur les coactions : elle n'utilise pas la comonadicité de l'extension des scalaires.

\noindent\emph{Portée de la vérification.} Lean définit les données de descente par la coaction (\texttt{Descent.\allowbreak{}DescentDatum}), leurs invariants, l'effectivité (\texttt{DescentDatum.\allowbreak{}IsEffective}), la réduction (\texttt{DescentDatum.\allowbreak{}reduce}) et les morphismes de descente effective pour les modules plats (\texttt{IsEffectiveDescentFlat}), et démontre le point~1 (\texttt{DescentDatum.\allowbreak{}isEffective\_of\_reduce}), le point~2 (\texttt{isEffectiveDescentFlat\_of\_quotient}) et le critère local de platitude (\texttt{flat\_of\_isNilpotent}), pour des anneaux commutatifs quelconques. L'hypothèse sur $I$ y est \texttt{IsConductorIdeal}. Il démontre aussi le théorème~\ref{thm:128-fid-plat} : le point~1 (\texttt{DescentDatum.\allowbreak{}bijective\_of\_flat}), le point~2 (\texttt{isEffectiveDescentFlat\_of\_faithfullyFlat}, avec \texttt{surjective\_of\_section} et la descente de la platitude \texttt{Module.\allowbreak{}Flat.\allowbreak{}of\_flat\_tensorProduct} de mathlib) et le point~3 (\texttt{isEffectiveDescentFlat\_of\_quotient\_faithfullyFlat}). Ne sont pas formalisés les corollaires 2 et~3 (énoncé ci-dessous).

Ne sont pas démontrés ici, de la même cote :

\begin{encadre}
\begin{theoreme*}[Grothendieck, pages 8 et 9, corollaires 2 et 3\piste{128-nilpotent-conductor-flat-descent}]\nonverifie
Soient $X$ un préschéma, $\mathcal I$ un idéal quasi-cohérent nilpotent de $\mathcal O_X$ et $X' = \operatorname{Spec} \mathcal A' \to X$ affine, $\mathcal I$ s'envoyant isomorphiquement sur un idéal de $\mathcal A'$ et $X'_0$ étant fidèlement plat sur $X_0 = V(\mathcal I)$. Alors $X' \to X$ est un morphisme de descente effective pour les modules quasi-cohérents plats, et le reste après tout changement de base plat $Y \to X$.
\end{theoreme*}
\end{encadre}
{\small Le cas affine, avec l'hypothèse plus faible que $\operatorname{Spec} A'_0 \to \operatorname{Spec} A_0$ soit de descente effective pour les modules plats, est le théorème~\ref{thm:128-descente}, et le cas affine tel qu'énoncé, avec $A'_0$ fidèlement plat sur $A_0$, est le point~3 du théorème~\ref{thm:128-fid-plat}. Restent non vérifiés le recollement sur un préschéma et la stabilité par changement de base plat.\par}

\begin{encadre}
\begin{theoreme*}[Grothendieck, pages 19 à 29, descente infinitésimale\piste{128-infinitesimal-descent-theorem}]\nonverifie
Soient $A$ un anneau semi-local noethérien de radical $\mathfrak m$, $A'$ une $A$-algèbre finie, $A_n = A/\mathfrak m^{n+1}$ et $A'_n = A' \otimes_A A_n$. Les trois conditions suivantes, imposées pour tout $n$, sont équivalentes : $H^1(A'_n/A_n) = 0$ ; $H^1(A'_n/A_n, \mathrm{GL}_r)$ est trivial ; la descente des modules quasi-cohérents plats le long de $\operatorname{Spec} A'_n \to \operatorname{Spec} H^0(A'_n/A_n)$ est effective. Elles entraînent la descente effective des modules plats de type fini le long de $\operatorname{Spec} A' \to \operatorname{Spec} H^0(A'/A)$.
\end{theoreme*}
\end{encadre}
{\small Le théorème lui-même reste non vérifié : mathlib n'a ni la cohomologie d'Amitsur $H^1(A'/A)$ ni le $H^1$ non abélien $H^1(A'/A, \mathrm{GL}_r)$, et sa démonstration (pages 26 à~29) repose sur le lemme~1 et ses corollaires 2 et~3, que la lecture trouve non démontrés : le cobord multiplicatif d'une unité $u$ est $u^{-1}\partial(u)$, non $\partial(u)$, et le carré de la page~20 ne commute pas. On vérifie ci-dessous les morceaux de la démonstration qui tiennent tels quels (\lot{128}{1}{19}).\par}

\noindent\emph{Rendre une matrice inversible.} Le lemme~2 fournit l'hypothèse du corollaire~2 dans la récurrence de la partie~a) : toute matrice sur $\widetilde B_0 = H^0(A'_0/A_0)$ devient inversible quand on lui ajoute une matrice venue de $B$. La page le démontre sous deux hypothèses, (i) corps résiduels infinis et (ii) extensions résiduelles radicielles ; la lecture observe que (i) est superflue sous (ii).

\begin{theoreme}[Grothendieck, page 23, lemme~2, sans l'hypothèse (i)\piste{128-infinitesimal-descent-theorem}]\label{thm:128-lemme2}
Soient $B$ un anneau et $C$ une $B$-algèbre entière n'ayant qu'un nombre fini d'idéaux maximaux. On suppose que deux idéaux maximaux distincts de $C$ induisent des idéaux distincts de $B$ et que chaque extension résiduelle $k(\mathfrak n)/k(\mathfrak m)$ est radicielle. Alors pour tout $n \geq 1$ et toute $u \in \mathbb M_n(C)$, il existe $v \in \mathbb M_n(B)$ telle que $u + \varphi(v)$ soit inversible. En particulier ($n = 1$, N.B. du lemme~1, page~19) $C = C^* + \varphi(B)$.
\end{theoreme}

\begin{proof}
Une matrice carrée sur $C$ est inversible si et seulement si son déterminant n'est dans aucun idéal maximal $\mathfrak n$ ; il suffit donc de trouver $v$ telle que $\det(u + v)$ soit non nul dans chaque corps $k(\mathfrak n) = C/\mathfrak n$. Les idéaux $\mathfrak m = \mathfrak n \cap B$ sont maximaux ($C$ est entière sur $B$) et deux à deux distincts, donc deux à deux étrangers : par le lemme chinois, appliqué coefficient par coefficient, on peut prescrire $v$ modulo chacun d'eux. On se ramène ainsi à un seul $\mathfrak n$, et à trouver $w \in \mathbb M_n(B)$ avec $\det(\bar u + \bar w) \neq 0$ dans $k(\mathfrak n)$.

Si $k(\mathfrak m)$ est infini, on prend $w = t$ scalaire : $\det(t + \bar u)$ est la valeur en $t$ du polynôme caractéristique de $-\bar u$, unitaire, donc non nul, qui n'a qu'un nombre fini de racines dans $k(\mathfrak n)$, alors que $k(\mathfrak m) \to k(\mathfrak n)$ est injectif. Si $k(\mathfrak m)$ est fini, il est parfait ; l'extension $k(\mathfrak n)/k(\mathfrak m)$, radicielle et algébrique, est alors séparable, donc triviale : $B \to k(\mathfrak n)$ est surjectif, et on relève $1 - \bar u$ en $w$, de sorte que $\bar u + \bar w = 1$.
\end{proof}

\begin{remarque}
Sur un corps résiduel infini, l'hypothèse radicielle ne sert pas, ni la finitude de $C$ : le Lean énonce aussi le lemme sous la forme \q{à chaque $\mathfrak n$, $k(\mathfrak m)$ est infini ou $B \to k(\mathfrak n)$ est surjectif}. Pour le N.B. du lemme~1, avec $C = \widetilde B_0$ et $B = \overline B$, il reste à savoir que $\operatorname{Spec} \widetilde B_0 \to \operatorname{Spec} \overline B$ est radiciel, ce que la page affirme sans le démontrer.
\end{remarque}

\noindent\emph{Descendre relativement à $A'/A$ ou à $A'/H^0$.} Les pages 26 et~27 identifient, entre crochets, la donnée de descente relativement à $A'_n/A_n$ à celle relativement à $A'_n/B^{(n)}$. C'est exact : pour $b \in H^0(A'/A)$, $b \otimes 1 = 1 \otimes b$ dans $A' \otimes_A A'$, et en multipliant par $s \otimes 1$ puis en faisant agir $A' \otimes_A A'$ sur $A' \otimes_A E$, on obtient $bs \otimes e = s \otimes be$ ; l'application canonique $A' \otimes_A E \to A' \otimes_B E$ a donc un inverse, pour tout $A'$-module $E$ et tout $B$ entre $A$ et $H^0(A'/A)$. Les complexes d'Amitsur et les données de descente relatives à $A'/A$ et à $A'/B$ coïncident, et $H^0(A'/B) = H^0(A'/A)$.

\noindent\emph{Portée de la vérification.} Lean démontre le lemme~2 sans l'hypothèse (i) (\texttt{Infinitesimal.\allowbreak{}lemme2}, sous la forme générale \texttt{Infinitesimal.\allowbreak{}exists\_isUnit\_add\_map}), le cas $n = 1$ (\texttt{Infinitesimal.\allowbreak{}exists\_isUnit\_add}), l'identification des produits tensoriels (\texttt{Infinitesimal.\allowbreak{}tensorEquiv}, \texttt{Infinitesimal.\allowbreak{}bijective\_mapOfCompatibleSMul}, \texttt{Infinitesimal.\allowbreak{}mem\_H0\_iff}, avec $H^0(A'/A)$ défini comme égaliseur, \texttt{Infinitesimal.\allowbreak{}H0}), et l'identité $p_2(u)\,p_1(u)^{-1} = 1 + p_1(u)^{-1}\,(p_2(u) - p_1(u))$ qui fait du cobord multiplicatif une dérivée logarithmique (\texttt{Infinitesimal.\allowbreak{}coboundary\_mul\_eq}). Ne sont pas formalisés : les $H^1$ d'Amitsur, additif et non abélien, le lemme~1 et ses corollaires, la récurrence sur $n$ de la partie~a), le passage à la limite de la partie~b) (Mittag-Leffler, Artin--Rees) et la partie~c) ; le théorème encadré ci-dessus reste donc non vérifié.
\section[La question de Buffalo : une relation d'équivalence finie non effective (Venken, 1971)]{La question de Buffalo : une relation d'équivalence finie non effective (Venken, 1971)\protect\verifie[\leanblobmain]{EffectiveVenken}}\label{sec:venken}

Cette section ne porte pas sur une cote du fonds. Elle répond à une question que Grothendieck a laissée ouverte deux fois. En 1961, dans le troisième exposé sur la construction des schémas, il écrit qu'il ne sait pas si une relation d'équivalence finie, sans hypothèse de platitude, est toujours effective, même sur un corps \cite{fga3}. Le 11 juillet 1973, à la fin d'une séance de son cours de Buffalo, il la donne encore comme problème ouvert, en ajoutant qu'il attend une réponse négative et que la question est \q{très élémentaire}. La réponse était imprimée depuis deux ans : c'est le corollaire~3.1 d'une note de Jacques Venken aux \emph{Comptes rendus} \cite{venken}, dont le titre parle de descente des modules plats et qui, de ce fait, semble être passée inaperçue.

\emph{L'idée.} On reprend le vocabulaire de la section~\ref{sec:128}. Soit $A$ une algèbre de dimension finie sur un anneau $k$ et $J \subset A \otimes_k A$ un idéal d'équivalence : il est contenu dans le noyau de la multiplication, stable par l'échange des facteurs, et vérifie la condition de transitivité. Le quotient de $\operatorname{Spec} A$ par la relation est le spectre de l'anneau des invariants
\[
  A^J = \{\, a \in A : a \otimes 1 - 1 \otimes a \in J \,\}.
\]
Les éléments $b \otimes 1 - 1 \otimes b$, pour $b$ invariant, engendrent un idéal $J_{A^J} \subset J$, celui de la relation \q{avoir la même image dans le quotient}. La relation est \emph{effective} quand les deux coïncident, c'est-à-dire quand elle est exactement la relation définie par son propre quotient. Pour une relation finie et plate, c'est toujours le cas (SGA~3, exposé~V \cite{sga3-1}). La question est de savoir si la platitude est nécessaire. Comme tout est de dimension finie, la réponse est une affaire d'algèbre linéaire : il suffit d'exhiber un élément de $J$ qui n'est pas dans $J_{A^J}$, et pour le montrer, une forme linéaire qui s'annule sur $J_{A^J}$ et pas sur cet élément.

\emph{L'exemple de Venken.} Soit $B$ le quotient de $k[M, N, X, Y, Z, W]$ par l'idéal engendré par
\[
  M^2,\ MN,\ N^2,\ X^3,\ Y^3,\ Z^3,\ W^3,\ YZ,\ NY,\ MZ,\ NXY,\ MYW
\]
et par tous les monômes de degré~$3$ en $X, Y, Z, W$ ; on note les classes en minuscules. C'est une algèbre locale, de base les $33$ monômes qui échappent à ces relations, tous de degré au plus~$3$. Venken considère la sous-algèbre engendrée par $m$, $n$, $mx$, $nw$ et $my - nz$, et la relation d'équivalence sur $\operatorname{Spec} B$ dont l'idéal est
\[
  I_V = \bigl(a \otimes 1 - 1 \otimes a : a = m, n, mx, nw, my - nz\bigr) + (mxy \otimes w) \subset B \otimes_k B .
\]
Les premiers générateurs disent que deux points ont les mêmes valeurs de $m, n, mx, nw, my - nz$ ; le dernier ajoute une condition qui n'est pas de cette forme.

\begin{encadre}
\begin{enonce}[Venken 1971, corollaire~3.1, sous la forme démontrée en Lean]
Soit $k$ un anneau commutatif non nul, et $B$, $I_V$ comme ci-dessus.
\begin{enumerate}
\item $I_V$ est un idéal d'équivalence : il est contenu dans le noyau de la multiplication $B \otimes_k B \to B$, il est stable par l'échange des facteurs, et $p_{13}(I_V) \subset p_{12}(I_V) + p_{23}(I_V)$ dans $B \otimes_k (B \otimes_k B)$.
\item Ses invariants forment le sous-module engendré par les dix éléments
\[
  1,\ m,\ n,\ mx,\ nz - my,\ nw,\ mx^2,\ my^2,\ nz^2,\ nw^2 .
\]
\item $mxy \otimes w$ appartient à $I_V$ mais pas à l'idéal engendré par les $b \otimes 1 - 1 \otimes b$, $b$ invariant. La relation n'est donc pas effective.
\end{enumerate}
\end{enonce}
\end{encadre}

\noindent Le point~2 contient une petite surprise : la sous-algèbre de Venken a pour base les six éléments $1$, $m$, $n$, $mx$, $nw$ et $my - nz$, et les invariants de la relation sont plus nombreux. Les quatre éléments de degré~$3$, $mx^2$, $my^2$, $nz^2$ et $nw^2$, sont invariants sans appartenir à cette sous-algèbre. Cela ne change pas la conclusion, mais il faut les connaître pour la démontrer, puisque l'idéal $J_{A^J}$ dépend de tous les invariants.

\begin{proof}
Tout se ramène à des identités entre éléments de $B \otimes_k B$, et l'on travaille dans la base des $33 \times 33$ produits $u \otimes v$ de monômes de base. La table de multiplication de $B$ est calculée une fois, et Lean la vérifie terme à terme.

\emph{Réflexivité.} Chaque générateur de $I_V$ s'envoie sur $0$ par la multiplication : $a \cdot 1 - 1 \cdot a = 0$, et $mxy \cdot w = mxyw = 0$ puisque $MYW$ est dans l'idéal.

\emph{Symétrie et transitivité.} L'échange envoie $a \otimes 1 - 1 \otimes a$ sur son opposé, qui est dans $I_V$ ; pour l'image $w \otimes mxy$ du dernier générateur, on exhibe une combinaison explicite des générateurs de $I_V$ à coefficients dans $B \otimes_k B$ qui lui est égale (neuf termes). De même, chaque image par $p_{13}$ d'un générateur est écrite comme combinaison explicite d'images par $p_{12}$ et $p_{23}$ (vingt termes en tout). Ce sont des certificats : trouver la combinaison demande un calcul, la vérifier n'est qu'un développement.

\emph{Les invariants.} Que les dix éléments soient invariants se vérifie de la même façon, par des combinaisons explicites. L'inclusion inverse est la partie délicate : il faut montrer qu'aucun autre élément de $B$ n'est invariant. On utilise vingt-trois formes linéaires $\psi_p$ sur $B \otimes_k B$, à coefficients entiers, qui s'annulent sur $I_V$. Si $b = \sum_s c_s\, s$ est invariant, alors $\psi_p(b \otimes 1 - 1 \otimes b) = 0$ pour tout $p$, et ces vingt-trois équations linéaires en les coefficients $c_s$ forcent $b$ à être une combinaison des dix éléments. Les formes et les combinaisons sont à coefficients entiers et l'argument ne divise jamais : c'est pourquoi l'énoncé vaut sur tout anneau commutatif non nul.

\emph{La non-effectivité.} Soit $\varphi$ la forme linéaire sur $B \otimes_k B$, à seize coefficients non nuls, tous entiers, que fournit le calcul. On vérifie qu'elle s'annule sur tous les produits $(u \otimes v)(b \otimes 1 - 1 \otimes b)$, pour $u, v$ monômes de base et $b$ l'un des dix invariants ; elle s'annule donc sur l'idéal $J_{A^J}$ qu'ils engendrent. Et $\varphi(mxy \otimes w) = 1$. Donc $mxy \otimes w \notin J_{A^J}$, alors que $mxy \otimes w \in I_V$ par définition.
\end{proof}

\emph{Comment la preuve a été trouvée, et ce qu'elle vérifie.} Les combinaisons et les formes linéaires ont été obtenues par une élimination de Gauss sur $\mathbf Q$, dans la base des monômes, dont tous les pivots valent $\pm 1$ ; c'est ce qui permet des certificats à coefficients entiers, valables sur tout anneau. Lean ne refait pas l'élimination : il vérifie les certificats, chacun par un calcul sur des listes d'entiers que le noyau évalue (\texttt{decide +kernel}, sans \texttt{native\_decide}). Découpées par degré, ces vérifications prennent une à deux minutes. La démonstration n'utilise que les trois axiomes standard de Lean. Venken, lui, démontre la non-effectivité par la cohomologie d'Amitsur : $mxy \otimes w$ définit une classe non nulle dans $H^1(B/A, \mathbb G_a)$. Le certificat $\varphi$ joue ici le rôle de cette classe.

\emph{Ce qui n'est pas formalisé.} Les dimensions des deux idéaux en degré~$4$ ($269$ et $268$ sur un corps) ne sont pas démontrées en Lean ; seule la forme qui les sépare l'est. Les énoncés de Venken sur la descente des modules plats, et la traduction entre idéaux d'équivalence et relations d'équivalence dans la catégorie des schémas, ne le sont pas non plus. Un second exemple, de longueur~$15$ (ou $16$ en caractéristique~$2$) en deux variables, obtenu en restreignant la relation de Raicu sur le plan à un sous-schéma fini, est démontré à la main dans la note \href{https://github.com/Commutator-IO/grothendieck-project/blob/main/docs/effective/article.pdf}{\texttt{grothendieck-effective.pdf}} ; il n'est pas formalisé.
\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 17 à 23, factorisation radicielle-étale\piste{126-radicial-etale-factorisation}]\nonverifie
Soit $f : X \to Y$ fini et universellement ouvert, $Y$ localement noethérien, dont toutes les fibres ont le même nombre de points géométriques. Alors $f$ se factorise en un morphisme radiciel fini surjectif $X \to X^{\text{ét}}$ suivi d'un revêtement étale fini $X^{\text{ét}} \to Y$, universel parmi les $Y$-morphismes de $X$ vers les $Y$-schémas étales.
\end{theoreme*}
\end{encadre}
{\small Les feuillets en esquissent une démonstration incomplète : la section ouverte et fermée de la page~19 est marquée \q{[vérif]}, la prose des lemmes des pages 18, 20, 21 et~22 est illisible, et la page~23 s'arrête sur \q{À formuler}.\par}

\begin{encadre}
\begin{theoreme*}[D'après les pages 4 à 7, forme complétée par l'édition, quotient d'une déformation nilpotente\piste{126-nilpotent-deformation-quotient}]\nonverifie
Soit $R \rightrightarrows X$ une relation d'équivalence plate dont la réduction $R_0 \rightrightarrows X_0$ modulo un idéal nilpotent est effective, de quotient fpqc quasi-séparé $X_0 \to Y_0$. Alors $R$ est effective, son quotient $Y$ est un épaississement nilpotent de $Y_0$ et $X \to Y$ est plat.
\end{theoreme*}
\end{encadre}
{\small La page porte la conclusion et la méthode, le relèvement par l'annulation de $\check H^0(X_0/Y_0, \mathcal H^1)$ ; les hypothèses, en grande partie illisibles, sont reconstituées par l'édition, de même que la réduction au cas $\mathcal J^2 = 0$ et la platitude.\par}

\begin{encadre}
\begin{theoreme*}[Grothendieck, pages 26 à 29, descente générique\piste{126-generic-descent}]\nonverifie
Soient $S$ noethérien, $T \to S$ plat de type fini et $F$ une catégorie fibrée sur les $S$-schémas de type fini pour laquelle les morphismes plats surjectifs sont de $F$-descente (pleine fidélité seulement). Un isomorphisme $\varphi : p_1^*X \simeq p_2^*X$ défini sur un ouvert dense de $T \times_S T$ et vérifiant la condition de cocycle sur un ouvert dense de $T \times_S T \times_S T$ se prolonge, après restriction de $T$ à un ouvert dense, en une donnée de descente qui coïncide avec $\varphi$ là où les deux sont définies.
\end{theoreme*}
\end{encadre}
\begin{demopage}[pages 26 à 29]
On réduit $\mathcal U$ et $V$ à des ouverts, et $T$ à un ouvert dense au-dessus duquel les fibres de $\mathcal U$ et de $V$ sont denses (p.~26). Sur $W = p_{12}^{-1}(\mathcal U) \cap p_{23}^{-1}(\mathcal U)$, la page définit $\psi : \pi^*X_1 \simeq \pi^*X_2$, $\pi = p_{13}$, en composant $\varphi$ par un point médian (p.~27). Sa compatibilité avec $\pi$ se lit sur une partie $W'$ de $T^5$ par le cocycle ; elle demande que $W' \to W \times_{T \times_S T} W$ soit surjectif, et la page l'admet \q{sauf erreur} (p.~28). $W \to T \times_S T$ étant plat et surjectif, $\psi$ descend en $\varphi'$, dont le cocycle se vérifie sur une partie $W'''$ de $T^6$ (pp.~28--29), et $\varphi' = \varphi$ sur $\mathcal U$ car $V \to \mathcal U$ est surjectif (p.~29). La lecture réordonne les restrictions.
\end{demopage}