\section[Cote 10 : les indécomposables de $\mathbb G_a \rtimes \mathbb G_m$]{Cote 10 : les indécomposables de $\mathbb G_a \rtimes \mathbb G_m$\protect\verifie{Folder10}}\label{sec:10} La cote 10, \emph{Catégories tensorielles}, que l'inventaire date \q{[à partir de 1958]}, finit sur sept feuillets consacrés au groupe $G = k \rtimes k^*$, $k^*$ opérant sur $k$ par $\lambda \mapsto \lambda^p$, en caractéristique nulle (\lot{10}{10}{191}). La page~191 passe à l'algèbre de Lie, engendrée par $X$ (de $\mathbb G_a$) et $Y$ (de $\mathbb G_m$) avec $[Y, X] = pX$ ; les pages~192 à~194 classent les représentations indécomposables ; les pages~195 à~197 calculent l'anneau des classes. L'hypothèse $p \geq 1$ est de l'édition. \noindent\emph{Conventions.} Une représentation est un espace vectoriel muni de deux endomorphismes $X$ et $Y$, et un morphisme une application linéaire qui commute aux deux. La chaîne $e_{n,k}$ est $k^k$, de base $z_0, \ldots, z_{k-1}$, avec $X z_j = z_{j+1}$ ($z_k = 0$) et $Y z_j = (n + pj)\, z_j$ ; c'est le $k[Z]/(Z^k)$ de la page, de poids $n, n + p, \ldots, n + p(k-1)$. Le produit tensoriel est muni de $X \otimes 1 + 1 \otimes X$ et de $Y \otimes 1 + 1 \otimes Y$, le dual de $-{}^tX$ et $-{}^tY$, et l'on pose $\xi = e_{0,2}$. \begin{enonce}[Grothendieck, page 194, les chaînes\piste{10-split-ring-ga-rtimes-gm}] En caractéristique nulle et pour $p \geq 1$, tout endomorphisme de $e_{n,k}$ est scalaire, de sorte que $e_{n,k}$ est indécomposable ; $e_{n,k} \simeq e_{n',k'}$ avec $k \geq 1$ entraîne $n = n'$ et $k = k'$ ; et le dual de $e_{n,k}$ est $e_{-n-p(k-1),k}$. \end{enonce} L'énoncé tient tel que la lecture le donne (\texttt{string\_end\_scalar}, \texttt{string\_indecomposable}, \texttt{string\_iso\_imp}, \texttt{string\_dual}). La formule du dual vaut sur tout corps et pour tout $p$. \begin{enonce}[Énoncé de l'édition, d'après les pages 196 et 197, le terme dominant de $\xi^n$] Sur un corps $K$ quelconque et pour tout $p$, si $k \geq 2$ est inversible dans $K$, on a $\xi \otimes e_{n,k} \simeq e_{n,k+1} \oplus e_{n+p,k-1}$. \end{enonce} \begin{proof} Soient $a$, $b$ la base de $\xi$, de poids $0$ et $p$, avec $Xa = b$ et $Xb = 0$. Comme $X^2 = 0$ sur $\xi$, on a $X^c(a \otimes y) = a \otimes X^c y + c\, b \otimes X^{c-1} y$. Posons $v_j = X^j(a \otimes z_0)$, $0 \leq j \leq k$, et $w_i = X^i w_0$, $0 \leq i \leq k - 2$, avec $w_0 = a \otimes z_1 - (k-1)\, b \otimes z_0$. Alors $v_j = a \otimes z_j + j\, b \otimes z_{j-1}$ et $w_i = a \otimes z_{i+1} + (i - k + 1)\, b \otimes z_i$, d'où $X v_k = 0$ et $X w_{k-2} = 0$. La relation $[Y, X] = pX$ passe au produit tensoriel, et $a \otimes z_0$, $w_0$ sont propres pour $Y$, de valeurs $n$ et $n + p$ : les $v_j$ et les $w_i$ forment deux chaînes, de types $e_{n,k+1}$ et $e_{n+p,k-1}$. Enfin $v_{i+1} - w_i = k\, b \otimes z_i$ et $v_k = k\, b \otimes z_{k-1}$ ; comme $k$ est inversible, les $b \otimes z_i$, puis les $a \otimes z_j = v_j - j\, b \otimes z_{j-1}$, sont dans l'espace engendré. Les $2k$ vecteurs $v_j$, $w_i$ engendrent un espace de dimension $2k$ : ils en forment une base, et l'application qui envoie les bases des deux chaînes sur eux est un isomorphisme de représentations. \end{proof} \begin{remarque} Cet isomorphisme rend triangulaire, à coefficient dominant $1$, l'écriture de $\xi^n$ sur les $e_{0,i}$ : $\xi \cdot e_{0,k} = e_{0,k+1} + \sigma_p\, e_{0,k-1}$ donne par récurrence $\xi^n = e_{0,n+1} + \sum_{i \leq n} c_{ni}\, e_{0,i}$, soit le $\alpha = 0$ que la page~197 obtient par les poids. La preuve n'utilise que l'inversibilité de $k$, ni la caractéristique nulle ni $p \geq 1$ : l'énoncé est plus général que celui dont la page a besoin (\texttt{xi\_tensor\_string}). \end{remarque} \begin{enonce}[Grothendieck, pages 192 à 194, lemmes 1 et 2\piste{10-split-ring-ga-rtimes-gm}] En caractéristique nulle et pour $p \geq 1$, soit $V$ une représentation de dimension finie non nulle, avec $[Y, X] = pX$, sur laquelle $Y$ est diagonalisable à valeurs propres entières, $V = \bigoplus_{n \in \mathbf Z} \operatorname{Ker}(Y - n)$. Si $V$ est indécomposable, c'est-à-dire si ses seuls endomorphismes idempotents sont $0$ et $1$, alors $V \simeq e_{n,k}$ pour un $n \in \mathbf Z$ et un $k \geq 1$. \end{enonce} \begin{proof} Comme $X$ envoie le poids $c$ sur le poids $c + p$ et que les poids de $V$ sont en nombre fini, $X$ est nilpotent ; soit $m$ tel que $X^{m+1} = 0 \neq X^m$. Prenons un vecteur propre $v$ de $Y$, de poids $n$, avec $X^m v \neq 0$, et une coordonnée $\psi$ dans une base propre de $Y$ telle que $\psi(X^m v) = 1$ : on a $\psi \circ Y = \mu\, \psi$, et $\mu = n + pm$ est le poids de $X^m v$. Comme $X^a v$ est de poids $n + pa$, on obtient $\psi(X^a v) = 0$ pour $a \neq m$, la caractéristique étant nulle et $p \neq 0$. Posons $P(x) = \sum_{l=0}^{m} \psi(X^{m-l} x)\, X^l v$. Alors $P$ commute à $X$ (car $X^{m+1} = 0$) et à $Y$ (car $X^{a} Y = (Y - pa) X^{a}$), et $P(X^l v) = X^l v$, de sorte que $P$ est un idempotent non nul : $P = 1$. Les $X^l v$, $0 \leq l \leq m$, engendrent donc $V$ ; ils sont libres, puisque $\psi(X^{m-l'} X^l v) = \delta_{l l'}$, et forment une chaîne de type $e_{n,m+1}$. \end{proof} \noindent Lean : \href{\leanblobmain/Folder10.lean}{\texttt{indecomposable\_is\_string}} (avec une base propre de $Y$) et \href{\leanblobmain/Folder10.lean}{\texttt{indecomposable\_is\_string'}} (avec $\sum_n \operatorname{Ker}(Y - n) = V$). \begin{remarque} La preuve ne suit pas celle de la page, qui construit la suite $E_0 \to E_1 \to \cdots$ et montre par récurrence que les $u_i$ sont injectifs, puis bijectifs : elle scinde directement la plus longue chaîne par un supplémentaire stable. L'hypothèse que $Y$ soit semi-simple est celle que la lecture tire du cas~II pour une représentation rationnelle de $G$ ; on ne peut l'omettre au niveau de l'algèbre de Lie, puisque $X = 0$ et $Y$ un bloc de Jordan de taille $2$ donnent une représentation indécomposable qui n'est pas une chaîne. Il en va de même de $p \geq 1$ : pour $p = 0$, $X$ n'est plus forcément nilpotent. \end{remarque} Ne sont pas démontrés ici : le passage d'une représentation rationnelle du groupe algébrique $G$ à la représentation $(V, X, Y)$ de son algèbre de Lie, avec $Y$ semi-simple à poids entiers, et l'anneau $R(G) = \mathbf Z[\mathbf Z][\xi]$ lui-même, qui demande encore le théorème de Krull--Schmidt, absent de mathlib. \subsection*{Page 65 : le $H^2$ d'un tore de norme un} L'Exemple~1 de la page~65 traite d'une catégorie tannakienne de lien un tore $G$ de dimension~$1$, déployé par une extension quadratique $Z/k$. La suite exacte $0 \to G \to Z^* \to \mathbf G_m \to 0$, où $Z^* = R_{Z/k}\mathbf G_m$ et la flèche de droite est la norme, donne \q{par Hilbert 90} que le noyau de $H^2(k, G) \to H^2(k, Z^*) = \mathrm{Br}(Z)$ est nul. La page en conclut que le caractère numérique détermine la catégorie. Lean démontre le pas cohomologique, à un niveau galoisien fini. Il ne démontre ni le passage à la cohomologie galoisienne de $k$, ni la conclusion tannakienne (finding \texttt{10-numerical-character-rank-one-torus}). \noindent\emph{Conventions.} Soient $L/K$ une extension galoisienne finie, $\Gamma = \mathrm{Gal}(L/K)$ et $\chi \colon \Gamma \to \{\pm 1\}$ un caractère, le signe d'une sous-extension quadratique $Z \subset L$ (\texttt{quadChar}). Pour un $\Gamma$-module $M$ (ici $M = L^\times$, noté additivement), on note $M_\chi$ le module $M$ tordu par $\chi$, soit $\gamma \star x = \chi(\gamma)\,\gamma x$, c'est-à-dire $\gamma(x)^{\chi(\gamma)}$ sur $L^\times$. On note $\mathrm{Ind}\,M$ le module $M \times M$, sur lequel $\gamma$ agit par $(\gamma x, \gamma y)$ si $\chi(\gamma) = 1$ et par $(\gamma y, \gamma x)$ sinon. Sur $L^\times$, ce sont les $L$-points de $G$ et de $Z^*$ : $(Z \otimes_K L)^\times$ s'écrit dans la base des deux idempotents. \begin{encadre} \begin{enonce}[Grothendieck, page 65, Exemple 1, à un niveau fini\piste{10-numerical-character-rank-one-torus}]\verifie[\leanblobmain]{Folder10} \begin{enumerate} \item[(a)] Pour tout $\Gamma$-module $M$, la suite $0 \to M_\chi \xrightarrow{x \mapsto (x, -x)} \mathrm{Ind}\,M \xrightarrow{(x,y) \mapsto x + y} M \to 0$ est exacte. Si $H^1(\Gamma, M) = 0$, l'application $H^2(\Gamma, M_\chi) \to H^2(\Gamma, \mathrm{Ind}\,M)$ est injective. \item[(b)] Pour $M = L^\times$, la suite est $1 \to G(L) \to (Z \otimes_K L)^\times \xrightarrow{N} L^\times \to 1$, et $H^2(\Gamma, G(L)) \to H^2(\Gamma, (Z \otimes_K L)^\times)$ est injective. \item[(c)] Si $\chi$ est le signe d'une sous-extension quadratique $Z$, on a $H^2(\Gamma, \mathrm{Ind}\,L^\times) \simeq H^2(\mathrm{Gal}(L/Z), L^\times)$, et le composé $H^2(\Gamma, G(L)) \to H^2(\mathrm{Gal}(L/Z), L^\times)$ est injectif. \end{enumerate} \end{enonce} \end{encadre} \begin{proof} (a) Le noyau de $(x, y) \mapsto x + y$ est formé des $(x, -x)$, et $(x, 0)$ est un antécédent de $x$. Les deux flèches sont équivariantes : si $\chi(\gamma) = -1$, l'échange des facteurs envoie $(\gamma x, -\gamma x)$ sur $(-\gamma x, \gamma x)$, image de $\gamma \star x = -\gamma x$, et ne change pas la somme. La suite exacte longue donne l'exactitude de $H^1(\Gamma, M) \xrightarrow{\delta} H^2(\Gamma, M_\chi) \to H^2(\Gamma, \mathrm{Ind}\,M)$, et le noyau est l'image d'un groupe nul. (b) La forme de Noether du théorème~90 de Hilbert donne $H^1(\mathrm{Gal}(L/K), L^\times) = 0$. (c) Soit $\tau$ hors de $\mathrm{Ker}\,\chi = \mathrm{Gal}(L/Z)$. L'application qui envoie $(x, y)$ sur la fonction $h \mapsto h x$ si $\chi(h) = 1$ et $h \mapsto h y$ sinon est un isomorphisme de $\mathrm{Ind}\,M$ sur le coinduit de $M|_{\mathrm{Ker}\,\chi}$, d'inverse $f \mapsto (f(1), \tau^{-1} f(\tau))$. On conclut par le lemme de Shapiro. Un tel $\tau$ existe, puisque $Z \neq K$. \end{proof} \noindent Lean : \href{\leanblobmain/Folder10.lean}{\texttt{torusSeq\_shortExact}} et \href{\leanblobmain/Folder10.lean}{\texttt{torus\_H2\_injective}} pour (a), \href{\leanblobmain/Folder10.lean}{\texttt{norm\_one\_torus\_H2\_injective}}, \href{\leanblobmain/Folder10.lean}{\texttt{torusIncl\_units}} et \href{\leanblobmain/Folder10.lean}{\texttt{normMap\_units}} pour (b), \href{\leanblobmain/Folder10.lean}{\texttt{indShapiro}} et \href{\leanblobmain/Folder10.lean}{\texttt{norm\_one\_torus\_H2\_injective\_quadratic}} pour (c). \begin{remarque} L'énoncé (a) vaut pour tout caractère $\chi$, y compris le caractère trivial, cas où $Z = K \times K$ est déployée et où $G = \mathbf G_m$. Lean n'identifie pas le module $\mathrm{Ind}\,L^\times$ à $(Z \otimes_K L)^\times$ : il prend le modèle des deux idempotents comme définition. Il n'identifie pas non plus $H^2(\mathrm{Gal}(L/Z), L^\times)$ au groupe de Brauer relatif $\mathrm{Br}(L/Z)$. Restent hors de portée le passage à la limite sur $L$, qui donne $H^2(k, G) \to \mathrm{Br}(Z)$, et l'énoncé tannakien que la page en tire : que le caractère numérique détermine $\mathcal M$ à équivalence près. Ce dernier demande les catégories tannakiennes, leurs gerbes et leurs liens, absents de mathlib. \end{remarque} \section[Cote 90 : un groupe plat irréductible dont un saturé n'est pas de type fini]{Cote 90 : un groupe plat irréductible dont un saturé n'est pas de type fini\protect\verifie{Folder90}}\label{sec:90} La cote 90, \emph{KG (X)}, est datée par l'inventaire \q{à partir de 1964} ; ses notes sont écrites au dos de feuillets dactylographiés d'EGA~IV, §\,18. Elles préparent l'existence de résolutions équivariantes. La page~1 pose, sur un anneau de Dedekind $A$, la notion de \emph{saturé} : pour un sous-module $N$ d'un module sans torsion $M$, le saturé $\widetilde N$ est l'ensemble des $y \in M$ dont un multiple non nul est dans $N$. Le lemme~1 donne des conditions équivalentes pour que le saturé de tout sous-module de type fini soit de type fini (\lot{90}{1}{1}). La page~9 applique ces conditions à l'algèbre $B$ d'un groupe affine et plat $G$ sur $A$, et dit dans une parenthèse (\lot{90}{1}{9}) : \begin{quote} \emph{cela signifie que pour les composantes irréd.\ de G, leurs fibres sont non vides} \end{quote} \noindent Pour un groupe de type fini, la parenthèse est raisonnable. Sans cette hypothèse, que la proposition ne pose pas, elle tombe en défaut. \noindent\emph{Le contre-exemple.} Soient $R$ un anneau de valuation discrète, $K$ son corps des fractions, $\varpi$ une uniformisante et $k = R/\varpi R$ le corps résiduel. On pose \[ B = \{ f \in K[T] \;:\; f(0) \in R \}, \] les polynômes à coefficients dans $K$ dont le terme constant est entier. C'est la réunion des dilatations successives $R[T/\varpi^n]$ du groupe additif en l'origine : on autorise des dénominateurs arbitraires partout, sauf au point $T = 0$ de la fibre spéciale. Cet exemple figure déjà dans SGA~3 (exposé~VI\textsubscript{B}, 13.3), où l'anneau est décrit comme $R \oplus K \oplus K \oplus \cdots$, non projectif ; Duong, Hai et dos Santos le rappellent (arXiv:1701.06518, exemple~1.1). La page de la cote~90, qui ne suppose pas $G$ de type fini, le contredit donc dans le séminaire même de Grothendieck. \begin{encadre} \begin{contrexemple}[SGA~3, exposé~VI\textsubscript{B}, 13.3, contre la parenthèse de la page 9 \cite{sga3-1}] L'anneau $B$ est intègre, de sorte que $\mathrm{Spec}\,B$ est irréductible ; il est plat sur $R$ ; l'application $f \mapsto f(0) \bmod \varpi$ est surjective de $B$ sur $k$, de noyau $\varpi B$, de sorte que $B/\varpi B \simeq k$ ; et $K \otimes_R B \neq 0$. Les deux fibres sont donc non vides. Pour tout $f \in B$, il existe $b_i, c_i \in B$ en nombre fini tels que $f(x + y) = \sum_i b_i(x)\,c_i(y)$ pour tous $x, y \in K$ : la comultiplication du groupe additif préserve $B$. Pourtant le saturé de $R \cdot T$ dans $B$ est $K \cdot T$, qui n'est pas un $R$-module de type fini. \end{contrexemple} \end{encadre} \begin{proof} $B$ est un sous-anneau de $K[T]$, donc intègre. Il est sans torsion : si $r \neq 0$ et $r f = 0$ dans $K[T]$, alors $f = 0$, puisque $r$ est inversible dans $K$. Sur un anneau principal, un module sans torsion est plat. Soit $f \in B$ avec $f(0) \in \varpi R$, disons $f(0) = a\varpi$. Alors $g = \varpi^{-1} f$ a pour terme constant $a \in R$, donc $g \in B$ et $f = \varpi g \in \varpi B$. Réciproquement, un élément de $\varpi B$ a un terme constant dans $\varpi R$. Le noyau de $f \mapsto f(0) \bmod \varpi$ est donc $\varpi B$, et l'application est surjective puisque les constantes de $R$ sont dans $B$. Pour la fibre générique, l'application $K \otimes_R B \to K[T]$, $\lambda \otimes f \mapsto \lambda f$, envoie $1 \otimes 1$ sur $1 \neq 0$. Pour la comultiplication, écrivons $f = \sum_{k \leq d} f_k T^k$ avec $f_0 \in R$. La formule du binôme donne $f(x + y) = \sum_k \sum_{j \leq k} \binom{k}{j} f_k\, x^j y^{k-j}$. On répartit chaque terme en un produit de deux éléments de $B$ : pour $k = j = 0$, $f_0 \cdot 1$ ; pour $j = 0 < k$, le facteur $1$ en $x$ et $f_k y^k$ en $y$, de terme constant nul ; pour $j \geq 1$, le facteur $\binom{k}{j} f_k x^j$, de terme constant nul, et $y^{k-j}$. Tous ces facteurs sont dans $B$. Le saturé. Si $r \neq 0$ et $r f = a T$ avec $a \in R$, alors $f = (a/r) T \in K \cdot T$. Inversement, pour $c \in K$, écrivons $c = a/s$ avec $a, s \in R$, $s \neq 0$ ; alors $s \cdot cT = aT \in R \cdot T$. Le saturé est donc $K \cdot T$, contenu dans $B$ puisque $cT$ s'annule en~$0$. L'application $cT \mapsto c$ est un isomorphisme de $R$-modules de $K \cdot T$ sur $K$. Si $K$ était de type fini sur $R$, il serait entier sur $R$ ; or $R$ est intégralement clos, donc $\varpi^{-1}$ serait dans $R$, et $\varpi$ serait inversible, ce qui n'est pas. \end{proof} \begin{remarque} Le lemme~1 de la page~1 dit que, pour un module sans torsion sur un anneau de Dedekind, les saturés des sous-modules de type fini sont de type fini si et seulement si le module est réunion filtrante de sous-modules de type fini saturés. Ici $R \cdot T$ est de type fini et son saturé ne l'est pas : $B$ ne satisfait pas les conditions du lemme~1, alors que $\mathrm{Spec}\,B$, qui n'a qu'une composante irréductible, a ses deux fibres non vides. Que $B$ soit une algèbre de Hopf n'est vérifié que par l'identité de comultiplication, point par point sur $K$ ; comme $K$ est infini, c'est une identité de polynômes. L'antipode, $f(T) \mapsto f(-T)$, et la counité, $f \mapsto f(0)$, préservent visiblement $B$, mais ne sont pas écrites en Lean. \end{remarque} \noindent\emph{Le cas de type fini et réduit.} Pour un groupe de type fini, la parenthèse se ramène à une question d'algèbre commutative sur l'idéal $d(A) = \bigcap_n \pi^n A$ des éléments infiniment divisibles par l'uniformisante. On en démontre ici le cœur, valable pour tout élément $\pi$ d'un anneau commutatif. \begin{encadre} \begin{enonce}[Composantes et éléments infiniment divisibles, énoncé de l'édition]\verifie[\leanblobmain]{Folder90} Soient $A$ un anneau commutatif, $\pi \in A$ et $d(A) = \bigcap_{n} \pi^n A$. \begin{enumerate} \item[(a)] Si un idéal premier minimal $\mathfrak p$ de $A$ vérifie $\mathfrak p + \pi A = A$, autrement dit si la composante irréductible $V(\mathfrak p)$ de $\mathrm{Spec}\,A$ ne rencontre pas la fibre spéciale $V(\pi)$, alors $d(A) \neq 0$. \item[(b)] Si $A$ est noethérien et réduit et si tout premier minimal $\mathfrak p$ vérifie $\mathfrak p + \pi A \neq A$, alors $d(A) = 0$. \end{enumerate} Pour $A$ noethérien et réduit, $d(A) = 0$ si et seulement si toutes les composantes irréductibles de $\mathrm{Spec}\,A$ rencontrent la fibre spéciale. \end{enonce} \end{encadre} \begin{proof} (a) Comme $\mathfrak p + \pi A = A$, il existe $c \in A$ tel que $1 - c\pi \in \mathfrak p$. Dans un anneau commutatif, tout élément d'un premier minimal est diviseur de zéro : il existe $a \neq 0$ tel que $a(1 - c\pi) = 0$. Alors $a = ac\pi$ et, par récurrence, $a = a(c\pi)^n = (ac^n)\,\pi^n$ pour tout $n$ : $a$ est un élément non nul de $d(A)$. L'idée : sur une composante qui évite la fibre spéciale, $\pi$ est inversible, et une fonction portée par cette composante est divisible par toutes les puissances de $\pi$. Cette partie n'utilise ni l'hypothèse noethérienne ni le théorème de Krull. (b) Soit $\mathfrak p$ un premier minimal. L'anneau $A/\mathfrak p$ est intègre et noethérien, et l'image de $\pi$ y engendre un idéal propre, puisque $\mathfrak p + \pi A \neq A$. Le théorème d'intersection de Krull donne $\bigcap_n \bar\pi^n (A/\mathfrak p) = 0$ ; l'image de $d(A)$ dans $A/\mathfrak p$ est donc nulle, et $d(A) \subseteq \mathfrak p$. L'intersection des premiers minimaux est le nilradical, nul puisque $A$ est réduit : $d(A) = 0$. \end{proof} \noindent Lean : \href{\leanblobmain/Folder90.lean}{\texttt{iInf\_pow\_ne\_bot\_of\_minimalPrime}} pour (a), \href{\leanblobmain/Folder90.lean}{\texttt{iInf\_pow\_eq\_bot\_of\_minimalPrimes}} pour (b) et \href{\leanblobmain/Folder90.lean}{\texttt{iInf\_pow\_eq\_bot\_iff}} pour l'équivalence. \begin{remarque} Pour $A = R[G]$, algèbre d'un groupe affine et plat de type fini sur un anneau de valuation discrète complet $R$ d'uniformisante $\pi$, la proposition~6.19 de Hai et dos Santos \cite{haidossantos2018} et le théorème de Kaplansky sur les modules projectifs traduisent $d(A) = 0$ en deux propriétés : $G$ est \emph{spécialement localement fini}, et $R[G]$ est un $R$-module libre. Avec l'énoncé ci-dessus, on obtient le critère de la page~9 quand $R[G]$ est réduit, ce qui est toujours le cas en caractéristique générique nulle. Ces deux résultats sont cités, non formalisés. Le cas non réduit, en caractéristique générique $p$, reste ouvert. \end{remarque} Ne sont pas démontrés ici : le lemme~1 lui-même, et l'énoncé suivant de la cote. \begin{encadre} \begin{theoreme*}[D'après les pages 13 à 23, sous-modules équivariants sur une base quelconque, forme précisée par la lecture\piste{90-equivariant-resolution-general-base}]\nonverifie Soient $S$ un schéma et $G$ un $S$-schéma en groupes plat et affine, dont l'algèbre est réunion filtrante de sous-cogèbres localement libres de rang fini à quotients plats, opérant sur un $S$-schéma $X$ quasi-compact et quasi-séparé muni d'un faisceau ample relatif $G$-linéarisé. Tout sous-module quasi-cohérent d'un $G$-module quasi-cohérent $E$ sur $X$ est contenu dans un plus petit sous-module quasi-cohérent $G$-stable, compatible au changement de base plat sur $S$ et de type fini quand le premier l'est. \end{theoreme*} \end{encadre} {\small Les feuillets en esquissent une démonstration incomplète (pages 19 à 23). L'argument s'arrête sur \q{Rédiger mieux ce début}. Mathlib n'a pas les modules quasi-cohérents équivariants. On se reportera aux notes de Grothendieck (\lot{90}{1}{13}).\par} \subsection*{Le plus petit sous-comodule, sur $\mathrm{Spec}\,A$ (pages 7--9 et 13--15)\protect\verifie{Folder90Comodules}}\label{sec:90-comodules} La page~13 (\lot{90}{1}{13}) énonce, pour un groupe affine sur une base quelconque dont l'algèbre $B$ est réunion filtrante de sous-modules $B_i$ avec 1)~$B/B_i$ plat, 2)~$\Delta B_i \subset B_i \otimes B_i$, 3)~$B_i$ localement libre de type fini, et pour un $G$-module quasi-cohérent $E$ à action triviale : \begin{quote} \emph{1) tout sous-module quasi-cohérent $F$ de $E$ est contenu dans un plus petit sous-module quasi-cohérent $F'$ stable par $G$ ; sa formation commute à tout changement de base plat ; si $F$ est de type fini, $F'$ aussi ; 2) si $X$ est quasi-compact et quasi-séparé, $E$ est réunion filtrante de sous-modules quasi-cohérents de type fini stables par $G$.} \end{quote} \noindent La page n'en donne pas de démonstration ; la lecture propose la formule $F' = \sum_i U_i \cdot (F \cap E_i)$, $U_i = \check B_i$, tirée de la description des pages~7 et~9. On démontre ici le cas de l'anneau, $X = S = \mathrm{Spec}\,A$, que la page énonce et argumente. Mathlib a les cogèbres mais pas les comodules : un comodule est un $A$-module $E$ muni d'une coaction $\delta \colon E \to B \otimes E$ counitaire et coassociative, et $N \subset E$ est un sous-comodule si $\delta N$ est contenu dans l'image de $B \otimes N$. \begin{encadre} \begin{enonce}[Pages 13--15, cas affine]\verifie[\leanblobmain]{Folder90Comodules} Soient $A$ un anneau commutatif et $B$ une $A$-cogèbre, réunion filtrante de sous-modules $B_i$ projectifs de type fini, avec $B/B_i$ plat et $\Delta B_i \subset \mathrm{Im}(B_i \otimes B_i \to B \otimes B)$. Soit $E$ un $B$-comodule. \begin{enumerate} \item Tout sous-module $F$ de $E$ est contenu dans un plus petit sous-comodule $F'$, à savoir le sous-module engendré par les $(u \otimes \mathrm{id})(y)$, où $y \in B_i \otimes E$ relève $\delta f$, $f \in F$ et $u \in U_i = \mathrm{Hom}_A(B_i, A)$. \item Si $F$ est de type fini, $F'$ l'est, et $F' = U_i \cdot F$ pour un seul indice $i$. \item Tout élément de $E$ est dans un sous-comodule de type fini ; ceux-ci sont stables par somme, et $E$ en est la réunion filtrante. \item Pour tout morphisme de comodules $\varphi$, $\varphi(F') = (\varphi F)'$. \item Pour toute $A$-algèbre $A'$, $A' \otimes E$ est un comodule sur la $A'$-cogèbre $A' \otimes B$, et l'image de $A' \otimes F'$ dans $A' \otimes E$ est le plus petit sous-comodule contenant l'image de $A' \otimes F$. Si $A'$ est plat sur $A$, cette image est $A' \otimes F'$. \end{enumerate} \end{enonce} \end{encadre} \begin{proof} \emph{L'étape de platitude.} Comme $B/B_i$ est plat, $B_i \otimes M \to B \otimes M$ est injectif pour tout $M$ (suite exacte $0 \to B_i \to B \to B/B_i \to 0$, lemme du serpent sur une présentation de $M$). Il en découle l'égalité de la lecture, $(B_i \otimes E) \cap (B \otimes N) = B_i \otimes N$ : si $y \in B_i \otimes E$ a son image dans $B \otimes N$, son image dans $B_i \otimes (E/N)$ s'envoie sur $0$ dans $B \otimes (E/N)$, donc est nulle, et $y$ provient de $B_i \otimes N$ par exactitude à droite. \emph{$F'$ contient $F$.} Pour $f \in F$, $\delta f$ est une somme finie, donc dans un $B_i \otimes E$ ; la coünité restreinte à $B_i$ donne $(\varepsilon \otimes \mathrm{id})(y) = (\varepsilon \otimes \mathrm{id})\,\delta f = f$. \emph{Minimalité.} Si $N \supset F$ est un sous-comodule et $y \in B_i \otimes E$ relève $\delta f$, $f \in F$, l'image de $y$ est dans $B \otimes N$, donc $y \in B_i \otimes N$ par l'étape de platitude, et $(u \otimes \mathrm{id})(y) \in N$. \emph{Stabilité.} Le module projectif de type fini $B_i$ a une base duale finie $(b_k, b_k^*)$, et $\Delta$ se relève en $\Delta_i \colon B_i \to B_i \otimes B_i$ par projectivité. La coassociativité et l'injectivité de $B_i \otimes (B \otimes E) \to B \otimes (B \otimes E)$ donnent $(\mathrm{id} \otimes \delta)(y) = (\Delta_i \otimes \mathrm{id})(y)$ dans $B_i \otimes B \otimes E$, d'où \[ \delta\big((u \otimes \mathrm{id})\,y\big) = \sum_k b_k \otimes \big((u * b_k^*) \otimes \mathrm{id}\big)(y), \qquad u * v = (u \otimes v) \circ \Delta_i , \] et les coefficients sont encore des générateurs de $F'$. \emph{Finitude.} Si $F$ est engendré par $f_1, \dots, f_m$, on choisit un $i$ commun (la famille est filtrante) et des relèvements $y_j$ de $\delta f_j$. Le sous-module $G$ engendré par les $(b_k^* \otimes \mathrm{id})(y_j)$ contient tous les $(u \otimes \mathrm{id})(y_j)$, puisque $u = \sum_k u(b_k)\, b_k^*$ ; il est stable par la formule précédente et contient $F$ ; donc $F' \subset G \subset F'$, et $F'$ est de type fini. Le point~3 s'en déduit avec $F = A e$. \emph{Morphismes et changement de base.} Un morphisme $\varphi$ envoie les générateurs de $F'$ sur des générateurs de $(\varphi F)'$, et $\varphi(F')$ est un sous-comodule contenant $\varphi F$. Pour $A'$, l'application $e \mapsto 1 \otimes e$ est un morphisme de $B$-comodules $E \to A' \otimes E$ ; un sous-comodule de $A' \otimes E$ sur $A' \otimes B$ en est un sur $B$, par $(a \otimes b) \otimes n \mapsto b \otimes a n$ ; et l'image de $A' \otimes F'$ est le $A'$-module engendré par $1 \otimes F'$. Si $A'$ est plat, $A' \otimes F' \to A' \otimes E$ est injectif. \end{proof} \begin{remarque} L'énoncé~1 tient sur tout anneau commutatif tel que la lecture le complète, et la compatibilité au changement de base tient pour toute $A$-algèbre $A'$ dès qu'on l'énonce avec des images ; la platitude de $A'$ ne sert qu'à identifier l'image à $A' \otimes F'$. La platitude de $B/B_i$ n'intervient que par l'injectivité de $B_i \otimes M \to B \otimes M$. Ne sont pas formalisés : les modules quasi-cohérents sur un schéma $X$ au-dessus d'une base $S$ quelconque (recollement, hypothèse « quasi-compact et quasi-séparé » de 2)), les énoncés~3) et~4), l'équivalence de la page~7 entre comodules $i$-admissibles et $U_i$-modules, et l'action de $G$ sur $X$ des pages~17 à~23, qui est l'objet de la trouvaille. Noms Lean : \texttt{Comodule}, \texttt{IsSubcomodule}, \texttt{Exhaustion}, \texttt{Exhaustion.\allowbreak{}closure}, \texttt{Exhaustion.\allowbreak{}isLeast\_closure}, \texttt{Exhaustion.\allowbreak{}closure\_fg}, \texttt{Exhaustion.\allowbreak{}exists\_fg\_isSubcomodule}, \texttt{IsSubcomodule.\allowbreak{}sup}, \texttt{Exhaustion.\allowbreak{}map\_closure}, \texttt{Exhaustion.\allowbreak{}coact\_coeff}, \texttt{Exhaustion.\allowbreak{}mem\_range\_lTensor\_of\_rTensor\_mem}, \texttt{comoduleBaseChange}, \texttt{isLeast\_closure\_baseChange}, \texttt{baseChange\_closure\_injective}. \end{remarque} \section[Cote 40 : la régularité des torseurs sous α\_p ne passe pas à la somme]{Cote 40 : la régularité des torseurs sous $\alpha_p$ ne passe pas à la somme\protect\verifie{Folder40}}\label{sec:40} La cote 40, \emph{Calculs [affines sur des] fibrés principaux affines : notes manuscrites (s.d.)}, que l'inventaire date \q{[années 1960-1970]}, compte vingt-sept pages de notes rapides, toutes de sa main. Elle traite des schémas en groupes affines comme algèbres de Hopf commutatives, de leurs actions et des espaces principaux homogènes (pages~1 à~15), puis du noyau $\alpha_p$ du Frobenius en caractéristique~$p$ (pages~16 à~18), de la classification $H^1(A, \alpha_p) = A/A^p$ (pages~18 à~23) et d'une version globale par la suite de Frobenius (pages~24 à~27). La remarque des pages~26 et~27 prend $A = k[[X]]$, $k$ algébriquement clos, et les revêtements obtenus en extrayant une racine $p$-ième : au changement d'uniformisante près, ce sont les $A[T]/(T^p - X^n)$, et \q{si $n = 1$, c'est un anneau local régulier. Sinon, il ne l'est pas, comme on voit facilement} (\lot{40}{2}{26}). Pour $p = 3$ et $n = 2$, la page décrit le cusp. La page~27 ajoute que, pour la structure de revêtement sous $\alpha_p$, ce revêtement est la somme de deux revêtements réguliers, ceux des racines $p$-ièmes de $X$ et de $-X + X^2$, et que le produit fibré de ces deux anneaux $C_1$, $C_2$ sur $A$ est \q{déjà un anneau non régulier [car isomorphe à $C_1[T]/(T^p)$, qui a des éléments nilpotents]} (\lot{40}{2}{27}). La phrase de la page~26 qui introduit la somme comporte des mots illisibles ou incertains ; l'énoncé de la page~27 est lu. \noindent\emph{Conventions.} Un anneau local noethérien de dimension un est régulier si et seulement s'il est de valuation discrète ; c'est ce dernier énoncé qui est démontré. Un anneau local régulier est intègre, donc un anneau non intègre n'est pas régulier. Pour un polynôme unitaire $g$ sur un anneau $R$, $R[T]/(g)$ est libre de base $1, T, \ldots, T^{\deg g - 1}$ ; en particulier la classe d'un polynôme non nul de degré $< \deg g$ n'y est pas nulle. \begin{lemme}\label{lem:40-dvr} Soient $A$ un anneau de valuation discrète, $\varpi$ une uniformisante, $u \in A^\times$ et $n \geq 1$. L'anneau $C = A[T]/(T^n - \varpi u)$ est de valuation discrète, d'idéal maximal $(t)$, où $t$ est la classe de $T$. \end{lemme} \begin{proof} Le polynôme $T^n - \varpi u$ est unitaire et d'Eisenstein pour l'idéal $(\varpi)$ : ses coefficients non dominants sont dans $(\varpi)$, et son terme constant $-\varpi u$ n'est pas dans $(\varpi^2)$. Il est donc irréductible dans $A[T]$, qui est factoriel, donc premier, et $C$ est intègre. L'anneau $C$ est fini sur $A$, donc entier, et tout idéal maximal $M$ de $C$ se contracte en un idéal maximal de $A$, c'est-à-dire en $(\varpi)$. Alors $\varpi \in M$, puis $t^n = \varpi u \in M$ et $t \in M$, puisque $M$ est premier. Inversement, tout $x \in M$ s'écrit $x = a + t y$ avec $a \in A$ et $y \in C$ ; comme $a = x - ty \in M \cap A = (\varpi)$ et $\varpi = t^n u^{-1}$, on a $x \in (t)$. Ainsi $M = (t)$ pour tout idéal maximal $M$ : $C$ est local d'idéal maximal $(t)$. Il est noethérien comme quotient de $A[T]$, et $t \neq 0$, puisque $t^n = \varpi u \neq 0$ et que $A \to C$ est injective. Un anneau local noethérien intègre dont l'idéal maximal est principal et non nul est de valuation discrète. \end{proof} \begin{enonce}[Page 26, le cusp $T^n = X^2$]\label{prop:40-cusp} Soient $k$ un corps quelconque, $n \geq 2$, $S = k[[X]][T]/(T^n - X^2)$ et $y$ la classe de $T$. \begin{enumerate} \item Si $n$ est impair, ni $X$ ne divise $y$, ni $y$ ne divise $X$ dans $S$ ; $S$ n'est donc pas un anneau de valuation, ni a fortiori de valuation discrète. \item Si $n = 2m$ est pair, $(y^m - X)(y^m + X) = 0$ et les deux facteurs sont non nuls ; $S$ n'est pas intègre. \item Si $n = 2$ et si $k$ est de caractéristique~$2$, $(y - X)^2 = 0$ et $y - X \neq 0$. \end{enumerate} \end{enonce} \begin{proof} 1) L'homomorphisme $A = k[[X]] \to k[[Z]]$, $f(X) \mapsto f(Z^n)$, se prolonge en $\varphi : S \to k[[Z]]$ par $y \mapsto Z^2$, puisque $(Z^2)^n = (Z^n)^2$. Soit $B \subset k[[Z]]$ l'ensemble des séries dont les coefficients d'exposant impair $< n$ sont nuls. C'est un sous-anneau : dans le coefficient d'exposant $m$ impair $< n$ d'un produit, chaque terme $a_i b_{m-i}$ a un indice impair $< n$. Il contient $f(Z^n)$, qui n'a que des exposants multiples de $n$, et $Z^2$ ; il contient donc $\varphi(S)$. Si $Xc = y$, alors $Z^n \varphi(c) = Z^2$, donc $Z^{n-2}\varphi(c) = 1$, égalité que le terme constant interdit, puisque $n \geq 3$. Si $yc = X$, alors $Z^2 \varphi(c) = Z^n$ et $\varphi(c) = Z^{n-2}$, qui n'est pas dans $B$ puisque $n - 2$ est impair et $< n$. Or, dans un anneau de valuation, de deux éléments l'un divise l'autre. 2) Le produit des polynômes unitaires $T^m - X$ et $T^m + X$ est $T^{2m} - X^2$, et leurs classes sont non nulles, étant de degré $m < 2m$. 3) $(T - X)^2 - (T^2 - X^2) = 2X(X - T)$ est nul en caractéristique~$2$, et $T - X$ est de degré $1 < 2$. \end{proof} \begin{theoreme}[Grothendieck, pages 26 et 27, la régularité ne passe pas à la somme des torseurs sous $\alpha_p$\piste{40-alpha-p-regular-sum}] Soient $k$ un corps de caractéristique $p > 0$, $A = k[[X]]$, $C_1 = A[T]/(T^p - X)$ et $C_2 = A[T]/(T^p + X - X^2)$, de racines $s$ et $t$. \begin{enumerate} \item $C_1$ et $C_2$ sont des anneaux locaux réguliers. \item Leur somme dans $H^1(A, \alpha_p) = A/A^p$, l'anneau $A[T]/(T^p - X^2)$ de la classe de $X + (-X + X^2) = X^2$, n'est pas régulière. \item Le produit fibré $C_1 \otimes_A C_2$ n'est pas réduit : $z = 1 \otimes t + (s - s^2) \otimes 1$ est non nul et $z^p = 0$. Dans $C_1$, on a $-X + X^2 = (-s + s^2)^p$. \item Il y a un isomorphisme de $C_1$-algèbres $C_1 \otimes_A C_2 \simeq C_1[T]/(T^p)$ qui envoie $z$ sur la classe de $T$. \end{enumerate} \end{theoreme} \begin{proof} 1) C'est le lemme~\ref{lem:40-dvr} pour $\varpi = X$, avec $u = 1$, puis avec $u = X - 1$, qui est inversible de terme constant $-1$ et vérifie $-X + X^2 = X(X - 1)$. 2) Si $p$ est impair, c'est l'énoncé~\ref{prop:40-cusp}, 1). Si $p = 2$, l'anneau a un nilpotent non nul par l'énoncé~\ref{prop:40-cusp}, 3) ; il n'est donc pas intègre. 3) L'anneau $C_1$ est non nul et $p = 0$ dedans, donc de caractéristique~$p$, et le Frobenius y est additif : $(-s + s^2)^p = (s^2 - s)^p = s^{2p} - s^p = X^2 - X$, puisque $s^p = X$. Le produit fibré est non nul (voir plus bas) et de caractéristique~$p$ pour la même raison, et $z = 1 \otimes t - (-s + s^2) \otimes 1$. Donc \[ z^p = 1 \otimes t^p - (-s + s^2)^p \otimes 1 = 1 \otimes a - a \otimes 1 = 0, \qquad a = -X + X^2 \in A, \] car $a \otimes 1 = 1 \otimes a$ pour $a \in A$. Pour voir que $z \neq 0$, soit $D = C_1[T]/(T^p + X - X^2)$, l'extension des scalaires de $C_2$ à $C_1$. L'homomorphisme de $A$-algèbres $C_2 \to D$, $t \mapsto T$, et l'inclusion $C_1 \to D$ définissent $\psi : C_1 \otimes_A C_2 \to D$, $x \otimes y \mapsto x\,\psi_2(y)$. Alors $\psi(z) = T - (-s + s^2)$ est la classe d'un polynôme unitaire de degré $1 < p$, donc non nulle. 4) Soit $E = C_1[T]/(T^p)$, de racine $\tau$, et $b = -s + s^2$. L'anneau $E$ est non nul et de caractéristique~$p$, donc $(\tau + b)^p = \tau^p + b^p = b^p = -X + X^2$ par~3) : l'homomorphisme de $A$-algèbres $\varphi_2 : C_2 \to E$, $t \mapsto \tau + b$, est bien défini, et avec l'inclusion $C_1 \to E$ il définit $\varphi : C_1 \otimes_A C_2 \to E$, $x \otimes y \mapsto x\,\varphi_2(y)$, qui est $C_1$-linéaire. Inversement, $z^p = 0$ par~3), donc $\tau \mapsto z$ définit un homomorphisme de $C_1$-algèbres $\chi : E \to C_1 \otimes_A C_2$. On a $\varphi(z) = (\tau + b) - b = \tau$, donc $\varphi \circ \chi$ fixe le générateur $\tau$ et est l'identité. De même $\chi \circ \varphi$ est $C_1$-linéaire et $\chi(\varphi(1 \otimes t)) = \chi(\tau + b) = z + b \otimes 1 = 1 \otimes t$ ; il est l'identité sur $C_1 \otimes 1$ et sur $1 \otimes C_2$, donc partout. \end{proof} \noindent Voir \texttt{root\_add\_pow\_E}, \texttt{C$_2$toE}, \texttt{fibreToE}, \texttt{EtoFibre}, \texttt{fibreEquiv} et \texttt{fibreEquiv\_z} dans \href{\leanblob/Folder40.lean}{\texttt{Folder40.\allowbreak{}lean}}. \begin{remarque} Le théorème tient tel que la lecture l'énonce, et plus généralement. Le lemme~\ref{lem:40-dvr} n'utilise ni la complétude de $A$, ni la caractéristique, ni $k$ algébriquement clos, et vaut pour tout $n \geq 1$. L'énoncé~\ref{prop:40-cusp} vaut sur tout corps et pour tout $n \geq 2$. Le calcul de $\psi(z)$ est celui de la lecture : dans $D$, $T^p = -X + X^2 = (-s + s^2)^p$, donc $(T - (-s + s^2))^p = 0$, et le changement de variable $T \mapsto T - (-s + s^2)$ donne $D \simeq C_1[T]/(T^p)$, l'anneau de la page. La lecture en déduit $C_1 \otimes_A C_2 \simeq C_1[T]/(T^p)$ ; le point~4) le démontre directement, sans passer par $D$ ni par le changement de variable : on envoie $t$ sur $\tau + (-s + s^2)$ et, en sens inverse, $\tau$ sur $z$. La piste demande si cet échec de la régularité sous la loi de groupe de $H^1(A, \alpha_p)$ est consigné dans la littérature sur les modèles de torseurs sous $\alpha_p$. \end{remarque} Ne sont pas démontrés ici : les algèbres de Hopf, les actions et les deux critères des pages~1 à~15 ; la classification $H^1(A, \alpha_p) = A/A^p$ (pages~18 à~23), et donc l'identification de la loi de groupe de $H^1$ avec l'addition de $A/A^p$, que la page~22 dit ne pas avoir prouvée ; la suite de Frobenius (pages~24 à~26) ; la réduction de tout torseur de $k[[X]]$ à $A[T]/(T^p - X^n)$ par changement d'uniformisante ; la non-régularité de $A[T]/(T^p - X^n)$ pour $n \geq 2$ autre que $n = 2$. \section[Cote 46 : relever un cocycle à travers la réduction modulo $\mathfrak m$]{Cote 46 : relever un cocycle à travers la réduction modulo $\mathfrak m$\protect\verifie{Folder46}}\label{sec:46} La cote 46, \emph{Schémas en groupes et fibrés principaux (Divers)}, quatre-vingt-quatorze pages sans pagination de sa main, réunit des liasses sur le Frobenius, les schémas de Brauer--Severi, la restriction des scalaires et, aux pages 71 à 92, des \q{Petits fourbis cohomologiques} : théorème~90 tordu, théorème de Lang, torsion des cocycles, version semi-locale. Les pages 90 à 92 en sont la dernière étape (\lot{46}{5}{90}). Soient $\mathcal O$ un anneau local, d'idéal maximal $\mathfrak m$ et de corps résiduel $k$ de caractéristique $p$, $\Gamma$ un groupe fini et $A$ une $(\mathcal O, \Gamma)$-algèbre finie, non nécessairement commutative : la marge de la page~90 cite $A = \mathrm M_n(\mathcal O)$. La page affirme que $H^1(\Gamma, A^*) \to H^1(\Gamma, (A/\mathfrak mA)^*) \times H^1(\Lambda, A^*)$ est injective, $\Lambda$ un $p$-sous-groupe de Sylow, et \q{en particulier}, quand $p$ ne divise pas l'ordre de $\Gamma$, que la réduction $H^1(\Gamma, A^*) \to H^1(\Gamma, (A/\mathfrak mA)^*)$ l'est. La lecture modernisée n'en retient que la forme \q{noyau trivial}. On démontre ici ce cas particulier, par une autre voie que la page, et montre qu'il se passe des deux hypothèses que la page discute ; puis l'injectivité elle-même, que la page affirme, et enfin la forme de Sylow, sous la forme \q{noyau trivial}. \noindent\emph{Cocycles et cobords.} Le groupe $\Gamma$ opère sur l'anneau $A$ par automorphismes d'anneau, et donc sur le groupe $A^*$ de ses inversibles. Un $1$-cocycle est une application $c : \Gamma \to A^*$ telle que $c(gh) = c(g)\, g(c(h))$ ; c'est un homomorphisme quand l'action est triviale, et en général un homomorphisme \q{tordu} par l'action. Il est cohomologue au cocycle trivial, ou est un cobord, s'il existe $u \in A^*$ avec $c(g) = u^{-1} g(u)$ pour tout $g$. L'ensemble $H^1(\Gamma, A^*)$ des classes n'est pas un groupe quand $A^*$ n'est pas commutatif, seulement un ensemble pointé, et \q{noyau trivial} y est plus faible qu'\q{injectif}. Dire que la classe de $c$ meurt dans $H^1(\Gamma, (A/\mathfrak mA)^*)$, c'est dire que l'image $\bar c$ de $c$ modulo $\mathfrak mA$ est un cobord : $\bar c(g) = \bar v^{-1} g(\bar v)$ pour un inversible $\bar v$ de $A/\mathfrak mA$. La question est de relever ce cobord. \noindent\emph{La voie de la page : dévisser par les puissances de $\mathfrak m$.} Supposons d'abord $\mathfrak m^N A = 0$. La page corrige le cocycle couche par couche. Si $c$ est déjà trivial modulo $\mathfrak m^n A$, on peut l'écrire $c(g) = 1 + a(g)$ avec $a(g) \in \mathfrak m^n A$. Modulo $\mathfrak m^{n+1}A$, le produit $a(g)\,g(a(h))$ disparaît, et la relation de cocycle devient additive : $a(gh) = a(g) + g(a(h))$. La couche $\mathfrak m^n A/\mathfrak m^{n+1}A$ est un groupe abélien, et même un espace vectoriel sur $k$. Sur un tel module, quand $|\Gamma|$ est inversible, tout cocycle additif est un cobord : on pose $w = -\frac{1}{|\Gamma|}\sum_{\sigma} a(\sigma)$, et la relation de cocycle donne $a(g) = g(w) - w$. Alors $1 + w$ est inversible, et $(1+w)^{-1}g(1+w) = 1 + a(g)$ modulo $\mathfrak m^{n+1}A$ : le cocycle est trivial une couche plus bas. Après $N$ couches, il est trivial. L'inversibilité de $|\Gamma|$ est là où sert \q{$p$ ne divise pas $|\Gamma|$} : dans un espace vectoriel sur $k$, diviser par $|\Gamma|$ demande que $|\Gamma| \neq 0$ dans $k$. Pour le cas général, $A$ fini sur $\mathcal O$ sans $\mathfrak m$ nilpotent, la lecture passe à la limite par Artin--Rees. \noindent\emph{La voie suivie ici : une seule moyenne.} La démonstration du théorème~90 de Hilbert fournit un raccourci. Pour un cocycle $c$ et un élément quelconque $w$ de $A$, posons $b = \sum_{\sigma \in \Gamma} c(\sigma)\,\sigma(w)$. Alors \[ c(g)\, g(b) = \sum_\sigma c(g)\, g(c(\sigma))\, g\sigma(w) = \sum_\sigma c(g\sigma)\, (g\sigma)(w) = b, \] puisque $\sigma \mapsto g\sigma$ permute $\Gamma$. Si $b$ est inversible, cela s'écrit $c(g) = b\, g(b)^{-1}$, et $c$ est un cobord, avec $u = b^{-1}$. Tout revient à choisir $w$ pour que $b$ soit inversible. Si $c$ est trivial modulo $\mathfrak mA$, on prend $w = 1$ : $b = \sum_\sigma c(\sigma)$ est congru à $|\Gamma|$, donc s'écrit $|\Gamma|(1 + x)$ avec $x \in \mathfrak mA$, et il est inversible dès que $|\Gamma|$ l'est et que les éléments $1 + x$, $x \in \mathfrak mA$, le sont. Dans le cas général, on relève $\bar v^{-1}$ en un $w \in A$ ; alors $b \equiv \sum_\sigma \bar v^{-1}\sigma(\bar v)\,\sigma(\bar v^{-1}) = |\Gamma|\, \bar v^{-1}$, et $b = |\Gamma| w (1 + x)$ avec $x \in \mathfrak mA$. Les couches de la page sont ainsi traitées d'un coup : la moyenne se fait dans $A^*$ et non dans chaque quotient abélien. Reste à voir que $1 + \mathfrak mA$ est fait d'inversibles, et que $w$ l'est. Quand $\mathfrak m^NA = 0$, un élément $x$ de $\mathfrak mA$ vérifie $x^N = 0$, et $1 + x$ a pour inverse $1 - x + x^2 - \cdots \pm x^{N-1}$. Quand $A$ est fini sur $\mathcal O$, c'est le lemme de Nakayama : la multiplication à gauche par $1 + x$ est une application $\mathcal O$-linéaire de $A$ dans lui-même, surjective modulo $\mathfrak mA$ puisqu'elle y est l'identité, donc surjective ; $1 + x$ a un inverse à droite, de même un inverse à gauche, et il est inversible. Un élément $w$ inversible modulo $\mathfrak mA$, avec $ww' = 1 + x$ et $w'w = 1 + y$, $x, y \in \mathfrak mA$, est alors inversible des deux côtés. \begin{encadre} \begin{enonce}[D'après les pages 90 à 92, forme reconstituée par l'édition, cas où $p$ ne divise pas l'ordre de $\Gamma$\piste{46-sylow-reduction-criterion}] Soient $\mathcal O$ un anneau local commutatif, de corps résiduel de caractéristique $p$, $\Gamma$ un groupe fini d'ordre premier à $p$, et $A$ une $\mathcal O$-algèbre, non nécessairement commutative, sur laquelle $\Gamma$ opère par automorphismes d'anneau. On suppose $\mathfrak m^N A = 0$ pour un entier $N$, ou $A$ fini sur $\mathcal O$. Alors le noyau de $H^1(\Gamma, A^*) \to H^1(\Gamma, (A/\mathfrak mA)^*)$ est trivial : un cocycle dont la réduction modulo $\mathfrak mA$ est un cobord est un cobord. Plus généralement, il en est ainsi de $H^1(\Gamma, A^*) \to H^1(\Gamma, B^*)$ pour tout morphisme d'anneaux surjectif $A \to B$ compatible à $\Gamma$ et de noyau contenu dans $\mathfrak mA$. \end{enonce} \end{encadre} \begin{proof} Soit $c$ un cocycle et $\bar v$ un inversible de $B$ avec $\bar c(g) = \bar v^{-1} g(\bar v)$. Comme $|\Gamma|$ n'est pas divisible par $p$, son image dans le corps résiduel n'est pas nulle, et $|\Gamma|$ est inversible dans $\mathcal O$, donc dans $A$. Les éléments $1 + x$, $x \in \mathfrak mA$, sont inversibles, par nilpotence ou par Nakayama. Relevons $\bar v^{-1}$ et $\bar v$ en $w$ et $w'$ ; $ww'$ et $w'w$ sont de la forme $1 + x$, donc $w$ est inversible. L'élément $b = \sum_\sigma c(\sigma)\,\sigma(w)$ a pour image $\sum_\sigma \bar v^{-1}\,\sigma(\bar v)\,\sigma(\bar v^{-1}) = |\Gamma|\,\bar v^{-1}$, la même que $|\Gamma|\, w$. Donc $b = m(1 + m^{-1}x)$, avec $m = |\Gamma|\,w$ inversible et $x$ dans le noyau, et $b$ est inversible. L'identité $c(g)\,g(b) = b$ donne $c(g) = u^{-1} g(u)$ avec $u = b^{-1}$. \end{proof} \begin{contrexemple*}[De l'édition : l'hypothèse sur $p$ est nécessaire] Soit $\Gamma = \mathbb Z/2$, opérant trivialement sur $A = \mathcal O = \mathbb Z/4$, où $\mathfrak m = (2)$, $\mathfrak m^2 = 0$ et $p = 2 = |\Gamma|$. L'application $c$ qui envoie l'élément non trivial de $\Gamma$ sur $-1$ est un cocycle, trivial modulo $\mathfrak m$, puisque $-1 \equiv 1 \pmod 2$. Ce n'est pas un cobord : l'action étant triviale et $A$ commutatif, $u^{-1}g(u) = 1$ pour tout $u$, et $-1 \neq 1$ dans $\mathbb Z/4$. \end{contrexemple*} \begin{remarque} La démonstration n'utilise que deux choses : $|\Gamma|$ inversible dans $A$, et $1 + x$ inversible pour $x$ dans le noyau de $A \to B$. Elle ne se sert ni de l'hypothèse du texte, que $\Gamma$ opère trivialement sur $A/\mathfrak mA$, ni de celle de la marge, que $A^\Gamma \to A/\mathfrak mA$ est surjectif, ni d'une action de $\Gamma$ sur $\mathcal O$, ni de la noethérianité, et le cas fini se passe d'Artin--Rees. La page en a besoin parce qu'elle vise la forme de Sylow : la restriction $H^1(\Gamma, A) \to H^1(\Lambda, A)$, injective puisque $[\Gamma : \Lambda]$ est inversible, fournit un $w \in A$ quelconque avec $a(g) = g(w) - w$, et la surjectivité de $A^\Gamma \to A/\mathfrak mA$ sert à corriger ce $w$ par un invariant pour que $\varepsilon(w) = 1$, donc pour que $w$ soit inversible. Quand $\Lambda$ est trivial, la moyenne donne directement un $w$ dans $\mathfrak m^nA$, et la correction n'a pas lieu d'être. \end{remarque} \begin{remarque} La marge qui porte la surjectivité de $A^\Gamma \to A/\mathfrak mA$ est écrite en huit lignes obliques dans la marge gauche de la page~90, reliée par un double trait à \q{Supposons de plus que} ; la transcription y relève une douzaine de mots illisibles et lit \q{plus généralement supposons} avec doute, \q{surjectif} étant souligné deux fois. L'hypothèse dont la forme de Sylow dépend repose donc sur une lecture fragile, que seul le fac-similé peut confirmer. Le cas démontré ici n'en dépend pas. \end{remarque} \begin{remarque} Pour $A$ commutatif, l'énoncé découle du lemme du §\,3.6 de Lorenz \cite{lorenz1999}, lu dans sa prépublication (arXiv:math/9808032) ; la version publiée n'a pas été consultée, et sa numérotation peut différer. Lorenz suppose $S$ commutatif et la trace $S \to S^G$ surjective, ce qu'entraîne $|G|$ inversible, et montre que $H^1(G, \mathrm{GL}_n(S)) \to H^1(G, \mathrm{GL}_n(S/\mathrm{rad}\, S))$ est de noyau trivial, par les modules projectifs et Nakayama. Comme $\mathfrak mA$ est contenu dans le radical de Jacobson de $A$ quand $A$ est fini sur $\mathcal O$, le cas $n = 1$ donne le cas commutatif de l'énoncé encadré. Le cas d'une algèbre non commutative à action quelconque, celui de la marge ($A = \mathrm M_n(\mathcal O)$ avec une action qui n'est pas forcément coefficient par coefficient), n'y est pas sous cette forme ; l'argument de moyenne est classique, et l'énoncé n'est pas présenté comme nouveau. \end{remarque} \noindent\emph{De noyau trivial à injectif.} Dans un ensemble pointé, un noyau trivial ne dit pas que deux classes de même image sont égales. Les pages~86 à~89 passent de l'un à l'autre en \emph{tordant} l'action par un cocycle $c'$ : on fait opérer $\Gamma$ sur $A$ par $\gamma \star a = c'(\gamma)\,\gamma(a)\,c'(\gamma)^{-1}$, et dire que $c$ et $c'$ sont cohomologues revient à dire qu'un cocycle de l'action tordue est un cobord. On peut éviter de changer d'action en faisant la moyenne directement avec les deux cocycles. \begin{encadre} \begin{enonce}[Grothendieck, page 90, injectivité, cas où $p$ ne divise pas l'ordre de $\Gamma$\piste{46-semilocal-hilbert90-inertia}] Sous les hypothèses de l'énoncé précédent, avec $A$ fini sur $\mathcal O$, l'application $H^1(\Gamma, A^*) \to H^1(\Gamma, B^*)$ est injective : si deux cocycles $c, c' : \Gamma \to A^*$ ont des réductions cohomologues dans $B^*$, ils sont cohomologues, c'est-à-dire que $c(g) = u^{-1}\,c'(g)\,g(u)$ pour un $u \in A^*$. \end{enonce} \end{encadre} \begin{proof} Pour $w \in A$, posons $u = \sum_\sigma c'(\sigma)\,\sigma(w)\,c(\sigma)^{-1}$. La relation de cocycle donne $g(c(\sigma))^{-1} = c(g\sigma)^{-1} c(g)$, d'où \[ c'(g)\,g(u) = \sum_\sigma c'(g)\,g(c'(\sigma))\,(g\sigma)(w)\,g(c(\sigma))^{-1} = \sum_\sigma c'(g\sigma)\,(g\sigma)(w)\,c(g\sigma)^{-1}\,c(g) = u\,c(g). \] Si $u$ est inversible, cela s'écrit $c(g) = u^{-1} c'(g)\,g(u)$. Soit $v \in B^*$ avec $\bar c(g) = v^{-1}\,\bar c'(g)\,g(v)$ ; relevons $v$ en $w$, inversible comme plus haut. Alors $\bar c'(\sigma)\,\sigma(v)\,\bar c(\sigma)^{-1} = v$ pour tout $\sigma$, de sorte que $u$ a la même image que $|\Gamma|\,w$, et $u = |\Gamma| w (1 + x)$ avec $x$ dans le noyau : $u$ est inversible. \end{proof} \noindent Avec $c' = 1$, on retrouve la moyenne de l'énoncé précédent. La moyenne $u$ est celle du théorème~90 pour l'action tordue par $c'$, écrite sans changer d'action. \noindent\emph{La forme de Sylow.} Reste le facteur $H^1(\Lambda, A^*)$ de la page~90. Quand $p$ divise l'ordre de $\Gamma$, la moyenne sur $\Gamma$ n'est plus possible, mais la moyenne sur les classes à gauche $g\Lambda$ l'est encore, puisque leur nombre $[\Gamma : \Lambda]$ est premier à $p$. Il faut pour cela que le terme $c(g)\,g(z)$ ne dépende que de la classe $g\Lambda$, c'est-à-dire que $c(\lambda)\,\lambda(z) = z$ pour $\lambda \in \Lambda$ : la relation de cocycle donne alors $c(g\lambda)\,(g\lambda)(z) = c(g)\,g\bigl(c(\lambda)\,\lambda(z)\bigr) = c(g)\,g(z)$. C'est là que servent les deux hypothèses de la page. Que $c$ soit un cobord sur $\Lambda$, $c(\lambda) = u^{-1}\lambda(u)$, permet de prendre $z = u^{-1}w$ avec $w$ invariant par $\Lambda$ ; que $w$ puisse être choisi de réduction prescrite modulo $\mathfrak mA$, c'est la surjectivité de la marge. \begin{encadre} \begin{enonce}[D'après la page 90 et sa marge, forme \q{noyau trivial}\piste{46-sylow-reduction-criterion}] Soient $\mathcal O$ un anneau local commutatif, de corps résiduel de caractéristique $p$, $\Gamma$ un groupe fini, $\Lambda$ un sous-groupe d'indice premier à $p$, par exemple un $p$-sous-groupe de Sylow, et $A$ une $\mathcal O$-algèbre finie, non nécessairement commutative, sur laquelle $\Gamma$ opère par automorphismes d'anneau. On suppose que $A^\Lambda \to A/\mathfrak mA$ est surjectif, ce qu'entraîne la surjectivité de $A^\Gamma \to A/\mathfrak mA$ demandée par la marge. Alors une classe de $H^1(\Gamma, A^*)$ triviale dans $H^1(\Gamma, (A/\mathfrak mA)^*)$ et dans $H^1(\Lambda, A^*)$ est triviale. Il en est de même pour tout morphisme d'anneaux surjectif $\pi : A \to B$ compatible à $\Gamma$, de noyau contenu dans $\mathfrak mA$, tel que $A^\Lambda \to B$ soit surjectif. \end{enonce} \end{encadre} \begin{proof} Soient $u \in A^*$ avec $c(\lambda) = u^{-1}\lambda(u)$ pour $\lambda \in \Lambda$, et $\bar v \in B^*$ avec $\bar c(g) = \bar v^{-1} g(\bar v)$. Choisissons $w \in A^\Lambda$ de réduction $\pi(u)\,\bar v^{-1}$, et posons $z = u^{-1}w$. Pour $\lambda \in \Lambda$, \[ c(\lambda)\,\lambda(z) = u^{-1}\lambda(u)\,\lambda(u^{-1})\,\lambda(w) = u^{-1} w = z , \] de sorte que $b = \sum_{g\Lambda \in \Gamma/\Lambda} c(g)\,g(z)$ est bien défini. Comme plus haut, $c(\gamma)\,\gamma(b)$ est la même somme, réindexée par $g\Lambda \mapsto \gamma g\Lambda$, d'où $c(\gamma)\,\gamma(b) = b$. La réduction de $z$ est $\bar v^{-1}$, celle de chaque terme est $\bar v^{-1}g(\bar v)\,g(\bar v^{-1}) = \bar v^{-1}$, et celle de $b$ est $[\Gamma : \Lambda]\,\bar v^{-1}$. L'indice est inversible dans $A$, $z$ l'est puisque sa réduction l'est, et $b = m(1 + m^{-1}x)$ avec $m = [\Gamma : \Lambda]\,z$ et $x$ dans le noyau : $b$ est inversible, et $c(g) = b\,g(b)^{-1}$. \end{proof} Pour $\Lambda = \Gamma$, l'hypothèse sur $\Lambda$ dit déjà que $c$ est un cobord, et l'énoncé est vide ; pour $\Lambda$ trivial, $A^\Lambda = A$ se surjecte toujours sur $A/\mathfrak mA$, et l'on retrouve le premier énoncé. La démonstration n'utilise pas l'hypothèse du texte que $\Gamma$ opère trivialement sur le corps résiduel. Elle donne le noyau trivial et non l'injectivité : pour comparer deux cocycles $c$ et $c'$ égaux sur $\Lambda$, il faudrait un $w$ qui commute aux $c(\lambda)$, ce que l'invariance par $\Lambda$ ne fournit pas quand $A$ n'est pas commutatif. Pour $A$ commutatif, $H^1(\Gamma, A^*)$ est un groupe et le noyau trivial suffit. \noindent\emph{L'injectivité dans la forme de Sylow.} Pour comparer deux cocycles $c$ et $c'$, on tord la moyenne comme plus haut : $b = \sum_{g\Lambda} c'(g)\,g(z)\,c(g)^{-1}$. La relation de cocycle donne \[ c'(g)\,g\bigl(c'(h)\,h(z)\,c(h)^{-1}\bigr) = c'(gh)\,(gh)(z)\,c(gh)^{-1}\,c(g), \] de sorte que le terme ne dépend que de la classe $g\Lambda$ dès que $c'(\lambda)\,\lambda(z)\,c(\lambda)^{-1} = z$ pour $\lambda \in \Lambda$, et qu'alors $c'(\gamma)\,\gamma(b) = b\,c(\gamma)$. Si $c(\lambda) = u^{-1}c'(\lambda)\,\lambda(u)$ sur $\Lambda$, on prend $z = wu$, et la condition devient $c'(\lambda)\,\lambda(w)\,c'(\lambda)^{-1} = w$ : $w$ doit être invariant par $\Lambda$ pour l'action tordue par $c'$, et non pour l'action donnée. C'est le point que la page ne vérifie pas en ramenant l'injectivité au noyau par torsion : l'hypothèse de la marge doit survivre à la torsion. Elle y survit dans deux cas : quand $c'$ est un cobord $t^{-1}\lambda(t)$ sur $\Lambda$, les invariants tordus sont les $t^{-1}wt$, $w \in A^\Lambda$, ce qui contient le noyau ($c' = 1$) ; quand $A$ est commutatif, l'action tordue est l'action donnée. \begin{encadre} \begin{enonce}[D'après la page 90 et sa marge, injectivité, forme reconstituée par l'édition\piste{46-sylow-reduction-criterion}] Soient $\mathcal O$, $\Gamma$, $\Lambda$, $A$ et $\pi : A \to B$ comme dans l'énoncé précédent, sans supposer $A$ commutatif, et $c$, $c'$ deux cocycles $\Gamma \to A^*$ dont les images dans $H^1(\Gamma, B^*)$ et dans $H^1(\Lambda, A^*)$ coïncident. On suppose que tout élément de $B$ se relève en un $w \in A$ tel que $c'(\lambda)\,\lambda(w)\,c'(\lambda)^{-1} = w$ pour $\lambda \in \Lambda$. Alors $c$ et $c'$ sont cohomologues. L'hypothèse est celle de la marge, $A^\Lambda \to B$ surjectif, quand $c'$ est un cobord sur $\Lambda$ ou quand $A$ est commutatif ; dans ce dernier cas, $H^1(\Gamma, A^*) \to H^1(\Gamma, B^*) \times H^1(\Lambda, A^*)$ est injective. \end{enonce} \end{encadre} \begin{proof} Soient $u \in A^*$ avec $c(\lambda) = u^{-1}c'(\lambda)\,\lambda(u)$ sur $\Lambda$, $\bar v \in B^*$ avec $\bar c(g) = \bar v^{-1}\,\bar c'(g)\,g(\bar v)$, et $w$ un relèvement tordu-invariant de $\bar v\,\pi(u)^{-1}$. Alors $z = wu$ vérifie $c'(\lambda)\,\lambda(z)\,c(\lambda)^{-1} = z$ : multiplié à droite par $c(\lambda) = u^{-1}c'(\lambda)\lambda(u)$, c'est $c'(\lambda)\lambda(w)\lambda(u) = w\,c'(\lambda)\,\lambda(u)$. La réduction de $z$ est $\bar v$, celle de chaque terme $c'(g)\,g(z)\,c(g)^{-1}$ est $\bar v$, celle de $b$ est $[\Gamma:\Lambda]\,\bar v$, et $b$ est inversible comme dans la démonstration précédente ; $c'(\gamma)\,\gamma(b) = b\,c(\gamma)$ s'écrit $c(\gamma) = b^{-1}c'(\gamma)\,\gamma(b)$. Si $c'(\lambda) = t^{-1}\lambda(t)$ et $w_0 \in A^\Lambda$ relève $\pi(t)\,y\,\pi(t)^{-1}$, l'élément $t^{-1}w_0t$ relève $y$ et est invariant pour l'action tordue ; si $A$ est commutatif, $c'(\lambda)\,\lambda(w)\,c'(\lambda)^{-1} = \lambda(w)$. \end{proof} On ne sait pas si l'hypothèse non tordue de la marge suffit en général quand $A$ n'est pas commutatif ; la démonstration par la moyenne ne le donne pas, et l'on n'a pas cherché de contre-exemple. \begin{sloppypar} \noindent\emph{Portée de la vérification.} Lean définit les cocycles et les cobords à valeurs dans $A^*$ pour un anneau quelconque muni d'une action par automorphismes (\texttt{IsCocycle}, \texttt{IsCoboundary}), sans recourir à la cohomologie des groupes de mathlib, qui est abélienne. Il démontre l'identité de moyenne (\texttt{mul\_smul\_sum}), sa conséquence (\texttt{isCoboundary\_of\_isUnit\_sum}), le noyau trivial pour un morphisme surjectif compatible à $\Gamma$ quand $1 + \mathrm{Ker}$ est fait d'inversibles (\texttt{isCoboundary\_of\_map\_isCoboundary}), la nilpotence de $\mathfrak mA$ quand $\mathfrak m^NA = 0$ et l'inversibilité de $1 + \mathfrak mA$ pour $A$ fini, par Nakayama (\texttt{isNilpotent\_of\_mem\_smul\_top}, \texttt{isUnit\_one\_add\_of\_mem\_smul\_top}), puis les deux formes de l'énoncé encadré (\texttt{ker\_trivial\_of\_pow\_smul\_eq\_bot}, \texttt{ker\_trivial}), l'injectivité (\texttt{mul\_smul\_sum\_twist}, \texttt{isCohomologous\_of\_map}, \texttt{injective}) et le contre-exemple (\texttt{not\_isCoboundary\_signCocycle}). La forme de Sylow, dans \href{\leanblob/Folder46.lean}{\texttt{Folder46.\allowbreak{}lean}}, y est démontrée par la moyenne sur les classes (\texttt{mul\_smul\_sum\_cosets}, \texttt{isCoboundary\_of\_restrict}), puis sur un anneau local pour un sous-groupe d'indice premier à $p$ et pour un sous-groupe de Sylow (\texttt{ker\_trivial\_restrict}, \texttt{ker\_trivial\_sylow}). L'injectivité dans la forme de Sylow y est démontrée par la moyenne tordue sur les classes (\texttt{mul\_smul\_twist\_cocycle}, \texttt{mul\_smul\_sum\_cosets\_twist}, \texttt{isCohomologous\_of\_restrict}), sous l'hypothèse de relèvement pour l'action tordue par $c'$, sur un anneau local (\texttt{injective\_restrict}, \texttt{injective\_sylow}), puis sous l'hypothèse non tordue de la marge quand $c'$ est un cobord sur $\Lambda$ (\texttt{twisted\_lift\_of\_isCoboundary}, \texttt{injective\_sylow\_of\_isCoboundary}) et quand $A$ est commutatif (\texttt{injective\_sylow\_comm}). L'hypothèse \q{$p$ ne divise pas $|\Gamma|$} y est écrite avec la caractéristique du corps résiduel de mathlib. Ne sont pas formalisés l'injectivité dans la forme de Sylow pour $A$ non commutatif sous la seule hypothèse non tordue de la marge, dont on ignore si elle suffit, la base semi-locale des pages~84 à~89 et le passage à la limite par Artin--Rees, que le cas fini rend inutile. \end{sloppypar} \noindent\emph{Pages 84 à 89 : l'inertie.} Avant ces trois pages, la cote en contient six autres (\lot{46}{5}{84}) qui énoncent une version semi-locale du théorème~90. Soient $\mathcal O$ un anneau local, de corps résiduel $k$, sur lequel $\Gamma$ opère ; $\Gamma$ est alors son propre groupe de décomposition $\Gamma_d$, et opère sur $k$. Le groupe d'inertie $\Gamma_i$ est le noyau de cette action : les $\gamma$ qui opèrent trivialement sur~$k$. L'action sur $A$ est semi-linéaire, $\gamma(\lambda a) = \gamma(\lambda)\,\gamma(a)$ pour $\lambda \in \mathcal O$. La page affirme que la restriction $H^1(\Gamma, A^*) \to H^1(\Gamma_i, A^*)$ est injective. Sa démonstration tord l'action, passe par inflation-restriction à $\Gamma/\Gamma_i$ opérant sur $A^{\Gamma_i}$, au-dessus de $\mathcal O^{\Gamma_i}$, admet (\q{on sait que}) que $\Gamma/\Gamma_i$ opère fidèlement sur le corps résiduel de $\mathcal O^{\Gamma_i}$, puis traite le cas $\Gamma_i = \{e\}$ : le cas d'un corps (pages 82 et 83), un dévissage le long des $\mathfrak m^nA$, et Artin--Rees pour conclure. On démontre ici l'énoncé quand $k$ est infini et que l'ordre de $\Gamma_i$ est inversible dans $k$, par une voie plus courte, qui n'a besoin ni de $\mathcal O^{\Gamma_i}$, ni du pas admis, ni du dévissage. Deux outils suffisent. Le premier est l'indépendance des caractères de Dedekind. Les automorphismes de $k$ définis par les éléments de $\Gamma$ sont deux à deux distincts quand on les regroupe par classes modulo $\Gamma_i$. Si $\sum_\sigma a_\sigma\,\sigma(\mu) = 0$ pour tout $\mu \in k$, la somme des $a_\sigma$ sur chaque classe est donc nulle, en particulier $\sum_{\sigma \in \Gamma_i} a_\sigma = 0$. Avec $a_\sigma = 1$, cela dit que la trace $\mu \mapsto \sum_\sigma \sigma(\mu)$ n'est pas identiquement nulle quand $|\Gamma_i| \neq 0$ dans $k$. Le second outil est un élément de trace un. Relevons dans $\mathcal O$ un $\mu$ de trace non nulle en $\lambda_0$. La trace $t = \sum_\sigma \sigma(\lambda_0)$ est inversible, puisque sa réduction ne s'annule pas, et invariante, donc $\lambda = \lambda_0 t^{-1}$ vérifie $\sum_\sigma \sigma(\lambda) = 1$. Cet élément remplace le $1/|\Gamma|$ de la moyenne : si $\bar c$ et $\bar c'$ sont cohomologues modulo $\mathfrak mA$, par $\bar v = \pi(w)$, la moyenne \[ u = \sum_{\sigma \in \Gamma} c'(\sigma)\,\sigma(\lambda w)\,c(\sigma)^{-1} \] vérifie $c'(\gamma)\,\gamma(u) = u\,c(\gamma)$, et sa réduction est $\sum_\sigma \sigma(\lambda)\,\bar v = \bar v$ ; elle est donc inversible, et $c$, $c'$ sont cohomologues dans $A^*$. Il n'y a ni dévissage ni passage à la limite : le relèvement se fait en une seule moyenne. \begin{encadre} \begin{enonce}[D'après les pages 84 à 89, cas local, inertie modérée, corps résiduel infini\piste{46-semilocal-hilbert90-inertia}] Soient $\mathcal O$ un anneau local commutatif, de corps résiduel $k$ infini, $\Gamma$ un groupe fini qui opère sur $\mathcal O$, $\Gamma_i$ son groupe d'inertie, d'ordre inversible dans $k$, et $A$ une $\mathcal O$-algèbre finie, non nécessairement commutative, munie d'une action semi-linéaire de~$\Gamma$. Alors $H^1(\Gamma, A^*) \to H^1(\Gamma_i, A^*)$ est injective : deux cocycles cohomologues sur $\Gamma_i$ le sont sur $\Gamma$. En particulier, si $\Gamma$ opère fidèlement sur $k$, alors $H^1(\Gamma, A^*) = 1$. Le cas $\mathfrak m = 0$ est le théorème~90 pour une algèbre finie quelconque sur un corps infini. \end{enonce} \end{encadre} \begin{proof} Soient $c$ et $c'$ deux cocycles, et $u_0 \in A^*$ avec $c(\gamma) = u_0^{-1}c'(\gamma)\,\gamma(u_0)$ pour $\gamma \in \Gamma_i$. Quitte à remplacer $c'$ par $\gamma \mapsto u_0^{-1}c'(\gamma)\,\gamma(u_0)$, on peut supposer $c = c'$ sur $\Gamma_i$. Soit $B = A/\mathfrak mA$, une $k$-algèbre de dimension finie, et $\gamma \star x = c'(\gamma)\,\gamma(x)\,c(\gamma)^{-1}$ l'action tordue de $\Gamma$ sur $B$. Elle est semi-linéaire sur $k$ et fixe $1$ sous $\Gamma_i$. Soit $X$ l'ensemble de ses points fixes, les $x$ avec $c'(\gamma)\,\gamma(x) = x\,c(\gamma)$. \emph{Lemme de Speiser.} Un élément $v$ fixé par $\Gamma_i$ est dans le $k$-sous-espace engendré par $X$. Sinon, une forme linéaire $f$ s'annule sur $X$ sans s'annuler en $v$. Pour tout $\mu \in k$, la moyenne $\sum_\sigma \sigma \star (\mu v)$ est dans $X$, d'où $\sum_\sigma \sigma(\mu)\,f(\sigma \star v) = 0$. Par Dedekind, $\sum_{\sigma \in \Gamma_i} f(\sigma \star v) = |\Gamma_i|\,f(v) = 0$, ce qui est absurde. \emph{Un point fixe inversible.} On a donc $1 = \sum_j t_j e_j$, avec des $e_j \in X$ et des $t_j \in k$. Le déterminant de la multiplication à gauche par $\sum_j x_j e_j$ est un polynôme $P$ en les $x_j$, qui vaut $1$ en $t$. Le corps fixe $k^\Gamma$ est infini, puisque $[k : k^\Gamma] \leq |\Gamma|$ et que $k$ est infini. Le polynôme $P$ ne s'annule donc pas partout sur $(k^\Gamma)^n$. Pour un tel point $x$, l'élément $\bar u = \sum_j x_j e_j$ est inversible et reste dans $X$, puisque ses coefficients sont invariants. Ainsi $\bar c$ et $\bar c'$ sont cohomologues dans $B^*$. \emph{Relèvement.} L'élément de trace un $\lambda$ existe puisque $|\Gamma_i| \neq 0$ dans $k$, et la moyenne ci-dessus relève la cohomologie de $B^*$ à $A^*$, puisque $1 + \mathfrak mA \subset A^*$ par Nakayama. Si $\Gamma$ opère fidèlement sur $k$, alors $\Gamma_i = \{e\}$, et l'hypothèse sur $\Gamma_i$ est vide. \end{proof} La démonstration n'utilise pas la noethérianité, ni une hypothèse de normalité, ni l'anneau $\mathcal O^{\Gamma_i}$ : le pas que la page admet n'intervient pas dans ce cas. Le corps infini sert au choix d'un point fixe inversible. Pour un corps fini, la page invoque le théorème de Lang. L'ordre de $\Gamma_i$ inversible sert au lemme de Speiser et à l'élément de trace un. Quand $p$ divise $|\Gamma_i|$, la trace peut être identiquement nulle, et la page passe alors par $\mathcal O^{\Gamma_i}$. \begin{sloppypar} \noindent\emph{Portée de la vérification.} Dans \href{\leanblob/Folder46.lean}{\texttt{Folder46.\allowbreak{}lean}}, Lean définit l'inertie (\texttt{inertia}) et démontre l'indépendance de Dedekind regroupée par fibres (\texttt{sum\_inertia\_eq\_zero}, \texttt{exists\_sum\_smul\_ne\_zero}), le lemme de Speiser tordu (\texttt{mem\_span\_fixed}), le cas d'un corps infini (\texttt{isCohomologous\_of\_eqOn\_inertia}), l'élément de trace un et le relèvement (\texttt{exists\_sum\_smul\_eq\_one}, \texttt{isCohomologous\_of\_map\_of\_sum\_eq\_one}), puis l'énoncé encadré (\texttt{isCohomologous\_of\_restrict\_inertia}) et le cas d'une action fidèle sur $k$ (\texttt{isCohomologous\_of\_faithful}). Comme plus haut, $A/\mathfrak mA$ est remplacé par un morphisme surjectif $\pi : A \to B$ compatible à $\Gamma$, de noyau contenu dans $\mathfrak mA$, vers une $k$-algèbre de dimension finie à action semi-linéaire. \end{sloppypar} La base semi-locale se traite de la même façon, sans complétion. Soient $\mathcal O$ un anneau commutatif, $\Gamma$ un groupe fini qui opère sur $\mathcal O$, et $\mathfrak m$ un idéal maximal dont les conjugués $\sigma^{-1}(\mathfrak m) = \{a \mid \sigma(a) \in \mathfrak m\}$ sont tous les idéaux maximaux de $\mathcal O$ ; c'est la transitivité de la page~84, et $\mathcal O$ est alors semi-local. On note $\Gamma_d$ le groupe de décomposition de $\mathfrak m$. \begin{encadre} \begin{enonce}[D'après les pages 84 à 89, base semi-locale et première flèche\piste{46-semilocal-hilbert90-inertia}] Soient $A$ une $\mathcal O$-algèbre finie, non nécessairement commutative, munie d'une action semi-linéaire de~$\Gamma$, et $L \in \mathcal O$ tel que $\sigma(L) \in \mathfrak m$ pour $\sigma \notin \Gamma_d$ et $\sum_{\sigma \in \Gamma} \sigma(L) \equiv 1 \bmod \mathfrak m$. Deux cocycles $c, c' : \Gamma \to A^*$ dont les restrictions à $\Gamma_d$ sont cohomologues modulo $\mathfrak mA$, a fortiori dans $A_{\mathfrak m}^*$, sont cohomologues dans $A^*$. Un tel $L$ existe dès qu'il existe $\lambda \in \mathcal O$ de trace un modulo $\mathfrak m$ pour $\Gamma_d$, en particulier quand l'inertie $\Gamma_i$ est d'ordre inversible dans $k = \mathcal O/\mathfrak m$. Si de plus $k$ est infini, deux cocycles dont les restrictions à $\Gamma_i$ sont cohomologues dans $(A/\mathfrak mA)^*$ sont cohomologues dans $A^*$ : la composée $H^1(\Gamma, A^*) \to H^1(\Gamma_d, A_{\mathfrak m}^*) \to H^1(\Gamma_i, A_{\mathfrak m}^*)$ est injective. \end{enonce} \end{encadre} \begin{proof} Soit $w \in A$, inversible modulo $\mathfrak mA$, d'inverse $w'$, avec $c'(\delta)\,\delta(w) \equiv w\,c(\delta)$ modulo $\mathfrak mA$ pour $\delta \in \Gamma_d$. La moyenne $u = \sum_{\sigma \in \Gamma} c'(\sigma)\,\sigma(Lw)\,c(\sigma)^{-1}$ vérifie $c'(\gamma)\,\gamma(u) = u\,c(\gamma)$. Modulo $\mathfrak mA$, les termes $\sigma \notin \Gamma_d$ disparaissent, puisque $\sigma(L) \in \mathfrak m$, et chacun des autres vaut $\sigma(L)\,w$ ; donc $u \equiv w$, et $u$ est inversible modulo $\mathfrak mA$. Par l'invariance tordue, $u = c'(\sigma)\,\sigma(u)\,c(\sigma)^{-1}$, et $c(\sigma)\,\sigma(w')\,c'(\sigma)^{-1}$ est un inverse de $u$ modulo $\sigma(\mathfrak m)A$, des deux côtés. Un élément de $A$ inversible modulo chacun des idéaux maximaux est inversible : la multiplication par $u$, à gauche comme à droite, est surjective modulo $\prod_\sigma \sigma(\mathfrak m)$, contenu dans le radical de Jacobson, donc surjective par Nakayama. Ainsi $c$ et $c'$ sont cohomologues. Pour construire $L$, les restes chinois donnent $e \in \mathcal O$, $e \equiv 1 \bmod \mathfrak m$ et $e \in \sigma^{-1}(\mathfrak m)$ pour $\sigma \notin \Gamma_d$, puisque ces idéaux maximaux sont distincts de $\mathfrak m$ ; on prend $L = e\lambda$. Quand $|\Gamma_i|$ est inversible dans $k$, Dedekind donne $\mu \in k$ de trace non nulle pour $\Gamma_d$, et $\lambda$ relève $\mu$ divisé par sa trace. Enfin, si $k$ est infini, le cas d'un corps démontré plus haut, appliqué à $\Gamma_d$ opérant sur $A/\mathfrak mA$, rend les restrictions à $\Gamma_d$ cohomologues modulo $\mathfrak mA$ dès qu'elles le sont sur $\Gamma_i$. \end{proof} La page passe par le complété $\hat A = \prod_{\mathfrak n} \hat A_{\mathfrak n}$, où $\hat A^*$ est induit de $\Gamma_d$, puis redescend par Artin--Rees. L'élément $e$ joue ici le rôle de l'idempotent du facteur $\hat A_{\mathfrak m}$, et la moyenne sur $\Gamma$ celui du lemme de Shapiro. Ce lemme lui-même se démontre sans hypothèse sur les ordres : si $A = \prod_{\Gamma/\Gamma_d} \sigma(e)A$ pour un idempotent $e$ dont les conjugués sont centraux et deux à deux orthogonaux quand ils sont distincts, $\Gamma_d$ le stabilisateur de $e$, deux cocycles $\Gamma \to A^*$ dont les restrictions à $\Gamma_d$ sont cohomologues dans $(eA)^*$ sont cohomologues dans $A^*$, par la moyenne $\sum_{g\Gamma_d} c'(g)\,g(z)\,c(g)^{-1}$ sur les classes, d'inverse $\sum_{g\Gamma_d} c(g)\,g(z^{-1})\,c'(g)^{-1}$. \begin{sloppypar} \noindent\emph{Portée de la vérification.} Dans \href{\leanblob/Folder46.lean}{\texttt{Folder46.\allowbreak{}lean}}, Lean démontre le critère d'inversibilité sur une base semi-locale (\texttt{surjective\_of\_forall}, \texttt{isUnit\_of\_forall}), l'énoncé encadré pour un $L$ donné (\texttt{isCohomologous\_of\_semilocal}), la construction de $L$ par les restes chinois et par Dedekind (\texttt{exists\_trace\_one\_semilocal}, \texttt{exists\_trace\_one\_mod}), le cas modéré à corps résiduel infini (\texttt{isCohomologous\_of\_restrict\_inertia\_semilocal}) et le lemme de Shapiro pour un produit (\texttt{isCohomologous\_of\_shapiro}). Le groupe de décomposition est un sous-groupe $D$ caractérisé par $\sigma \in D \iff \sigma^{-1}(\mathfrak m) = \mathfrak m$ ; le corps résiduel est un corps $k$ muni d'une surjection $\mathcal O \to k$ de noyau $\mathfrak m$, compatible à $D$, et $A/\mathfrak mA$ est remplacé comme plus haut par un morphisme surjectif vers une $k$-algèbre de dimension finie, de noyau contenu dans $\mathfrak mA$. La localisation $A_{\mathfrak m}$ et la complétion n'interviennent pas : l'hypothèse porte sur la réduction modulo $\mathfrak mA$, plus faible. \end{sloppypar} N'est pas démontré ici, de la même cote : \begin{encadre} \begin{theoreme*}[Grothendieck, pages 84 à 89, Hilbert~90 semi-local et inertie ; voir aussi Lorenz 1999\piste{46-semilocal-hilbert90-inertia}]\nonverifie Soient $\mathcal O$ un anneau semi-local noethérien, $\Gamma$ un groupe fini qui opère fidèlement et transitivement sur ses idéaux maximaux, et $A$ une $\mathcal O$-algèbre finie, non nécessairement commutative, munie d'une action semi-linéaire de~$\Gamma$. Les applications $H^1(\Gamma, A^*) \to H^1(\Gamma_d, A_{\mathfrak m}^*) \to H^1(\Gamma_i, A_{\mathfrak m}^*)$ vers les groupes de décomposition et d'inertie sont injectives comme applications d'ensembles pointés, et non seulement de noyau trivial. \end{theoreme*} \end{encadre} {\small La finitude de $A$ sur $\mathcal O$ est ajoutée par l'édition, et un pas que la page admet (\q{on sait que}) peut demander une hypothèse de normalité. Lorenz considère ces applications pour un anneau commutatif et n'en donne que le noyau trivial. La seconde flèche est démontrée plus haut quand $\mathcal O$ est local, $k$ infini et l'inertie modérée, et la base semi-locale avec la première flèche quand l'inertie est modérée (ou, plus généralement, quand $\Gamma_d$ a un élément de trace un modulo $\mathfrak m$), ainsi que le lemme de Shapiro pour un produit. Restent non formalisés la première flèche dans le cas sauvage (complétion et descente par Artin--Rees), l'inertie sauvage, où la page passe à $\mathcal O^{\Gamma_i}$ et admet que $\Gamma/\Gamma_i$ opère fidèlement sur son corps résiduel, et le corps résiduel fini (théorème de Lang). Mathlib n'a pas la cohomologie non abélienne $H^1(\Gamma, A^*)$. On se reportera aux notes de Grothendieck (\lot{46}{5}{84}).\par} \section[Cote 53 : un monoïde simplifiable est un groupe]{Cote 53 : un monoïde simplifiable est un groupe\protect\verifie{Folder53}}\label{sec:53} La cote 53, \emph{Groupes algébriques : notes manuscrites (s.d.), lettre (1973)}, trente-trois pages, garde des notes pour un cours sur les groupes algébriques : sur un corps aux pages 2 à 15, sur un anneau aux pages 21 à 33 (distributions, comodules, plongements linéaires). Entre les deux, une lettre d'une autre main, de juin 1973, objecte au cours qu'un monoïde affine de type fini ne se plonge pas toujours dans $\mathrm{GL}_n$ : le monoïde $\{0, 1\}$ muni de la multiplication en est un exemple. La page~21 s'ouvre sur une \q{Rectification} : le plongement fermé multiplicatif se fait dans l'espace des matrices $\mathrm M_n$, et non dans $\mathrm{GL}_n$ (\lot{53}{2}{21}) ; à la page~30, le $\mathrm M$ de la proposition est écrit par-dessus un $\mathrm{GL}$ (\lot{53}{2}{30}). La page donne aussitôt la raison. Un monoïde $G$ de présentation finie sur un anneau, \q{tel que les translations à g.\ (à dr.)\ sont} suivi de deux mots illisibles, par exemple un monoïde qui se plonge dans un groupe, serait un groupe ; la fin de la phrase, \q{objet gr.-pr.}, est elle-même incertaine. La lecture modernisée complète les deux mots par \q{des monomorphismes} et propose une démonstration par le théorème d'Ax--Grothendieck (EGA~IV, 10.4.11 \cite{ega4-3}). L'énoncé repose donc sur une reconstruction : seul le fac-similé dira si les deux mots sont bien ceux-là. La vérification porte sur sa forme classique, pour les points sur un corps algébriquement clos. \noindent\emph{Pourquoi un monoïde fermé de $\mathrm{GL}_n$ serait un groupe.} Dans un groupe, on simplifie : $ax = ay$ entraîne $x = y$. Un sous-monoïde $S$ de $\mathrm{GL}_n$ hérite de cette propriété, et la multiplication à gauche par $a \in S$ est une application injective de $S$ dans lui-même. Si $S$ était fini, une injection d'un ensemble fini dans lui-même serait une bijection, il existerait $b \in S$ avec $ab = 1$, et $S$ serait un groupe. Pour un ensemble infini, l'argument tombe : dans $\mathbb C^*$, le sous-monoïde $\{1, 2, 4, 8, \ldots\}$ est simplifiable et n'est pas un groupe : la multiplication par~$2$ y est injective sans être surjective. Mais ce sous-monoïde n'est pas une variété : il n'est défini par aucun système d'équations polynomiales. \noindent\emph{Le théorème d'Ax--Grothendieck.} Sur un corps algébriquement clos $K$, une application polynomiale injective d'une variété affine dans elle-même est surjective \cite{ax1968, borel1969}. L'idée d'Ax est de se ramener au cas fini. Une application polynomiale ne fait intervenir qu'un nombre fini de coefficients. Sur la clôture algébrique de $\mathbb F_p$, ces coefficients vivent dans un corps fini $\mathbb F_q$, et la clôture est la réunion des $\mathbb F_{q^r}$ : sur chacun, l'application envoie un ensemble fini dans lui-même, injectivement, donc surjectivement, et tout point de la variété est atteint. Le passage aux autres corps algébriquement clos, en caractéristique nulle en particulier, se fait par la logique : \q{injective entraîne surjective} s'écrit, à degrés bornés, comme un énoncé du premier ordre, vrai dans tous les corps algébriquement clos de caractéristique $p$ pour $p$ assez grand, donc dans ceux de caractéristique nulle. L'hypothèse \q{algébriquement clos} est nécessaire : sur $\mathbb Q$, $x \mapsto x^3$ est injective et ne prend pas la valeur~$2$. Mathlib contient ce théorème, démontré par la théorie des modèles, sous la forme \texttt{MvPolynomial.\allowbreak{}ax\_grothendieck\_zeroLocus} : pour le lieu des zéros $S \subset K^\iota$ d'un idéal de polynômes et une application polynomiale $S \to S$ injective, elle est surjective sur~$S$. \noindent\emph{Le cadre.} Un monoïde de points d'une variété affine, à loi polynomiale, est un monoïde $M$ muni d'une application injective $\varphi : M \to K^\iota$, $\iota$ fini, dont l'image est le lieu des zéros d'un idéal de $K[X_i]$, et de polynômes $m_i$ en deux jeux de variables tels que $\varphi(xy) = m(\varphi(x), \varphi(y))$. La translation à gauche par $x$ est alors, dans les coordonnées, l'application polynomiale $v \mapsto m(\varphi(x), v)$. On dit que $M$ est simplifiable à gauche si $xy = xz$ entraîne $y = z$. \begin{encadre} \begin{enonce}[D'après la page 21, forme reconstituée par l'édition, sur les points\piste{53-cancellative-monoid-is-group}] Soient $K$ un corps algébriquement clos et $M$ un monoïde de points d'une variété affine sur $K$, à loi polynomiale. Si $M$ est simplifiable à gauche, tout élément de $M$ est inversible : $M$ est un groupe. \end{enonce} \end{encadre} \begin{proof} Soit $x \in M$. La translation $y \mapsto xy$ est injective, puisque $M$ est simplifiable. Lue dans les coordonnées, c'est l'application polynomiale $v \mapsto m(\varphi(x), v)$ du lieu des zéros $\varphi(M)$ dans lui-même, injective sur ce lieu puisque $\varphi$ l'est. Par Ax--Grothendieck, elle est surjective, et $\varphi(1)$ est atteint : il existe $y$ avec $\varphi(xy) = \varphi(1)$, donc $xy = 1$. Alors $x(yx) = (xy)x = x = x \cdot 1$, et la simplification donne $yx = 1$. L'élément $y$ est un inverse de $x$ des deux côtés. \end{proof} \begin{encadre} \begin{enonce}[D'après la page 21, sous-monoïdes fermés de $\mathrm{GL}_n$] Sur un corps algébriquement clos $K$, un sous-monoïde de $\mathrm{GL}_n(K)$ fermé dans $\mathrm{GL}_n$, c'est-à-dire défini par des équations polynomiales en les coefficients de la matrice et en l'inverse de son déterminant, est un sous-groupe. \end{enonce} \end{encadre} \begin{proof} On repère une matrice inversible $A$ par ses $n^2$ coefficients et par $t = \det(A)^{-1}$ : $\mathrm{GL}_n$ devient le lieu des zéros de $t \det(A) - 1$ dans $K^{n^2 + 1}$, et le sous-monoïde $S$ le lieu des zéros de ses équations et de celle-ci. La loi $(A, t)(B, s) = (AB, ts)$ est polynomiale, et $S$ est simplifiable, comme partie d'un groupe. L'énoncé précédent donne, pour $A \in S$, un $B \in S$ avec $AB = 1$, c'est-à-dire $A^{-1} = B \in S$. \end{proof} \begin{remarque} La démonstration n'utilise que la simplification à gauche, là où la page suppose les translations à gauche et à droite injectives. Le passage de $xy = 1$ à $yx = 1$ est un argument de monoïde, sans géométrie. Un sous-monoïde fermé de $\mathrm{M}_n$ contenu dans $\mathrm{GL}_n$ est fermé dans $\mathrm{GL}_n$ ; c'est un cas particulier du second énoncé. Un sous-monoïde fermé de $\mathrm M_n$ qui contient une matrice non inversible, comme $\{0, 1\}$, n'est évidemment pas un groupe : c'est pourquoi le cours doit plonger les monoïdes dans $\mathrm M_n$. \end{remarque} \begin{remarque} L'énoncé est classique. Brion \cite[§\,2.2, prop.~3]{brion2014} démontre par le même argument (une translation injective est surjective, par le théorème~C d'Ax) qu'un élément d'un monoïde algébrique qui a un inverse à gauche est inversible, et que si $1$ est le seul idempotent, le monoïde est un groupe. Un monoïde simplifiable n'a pas d'autre idempotent que $1$, car $e^2 = e = e \cdot 1$ donne $e = 1$ ; l'énoncé encadré en découle. Pour les monoïdes algébriques linéaires, le livre de Putcha \cite{putcha1988} est la référence que Brion cite ; il n'a pas été relu ici. La fiche de la piste reste \q{non cherchée} pour la forme sur un anneau, avec des monomorphismes de schémas. \end{remarque} \noindent\emph{Portée de la vérification.} Lean formalise un monoïde de points à loi polynomiale par les données $(\varphi, I, m)$ ci-dessus et démontre les deux énoncés (\texttt{isUnit\_of\_isLeftCancelMul} et \texttt{inv\_mem\_of\_isClosed}) par \texttt{ax\_grothendieck\_zeroLocus} ; les translations y sont écrites comme polynômes par substitution (\texttt{translation}, \texttt{eval\_translation}). La forme de la page n'est pas formalisée : un schéma en monoïdes de présentation finie sur un anneau quelconque, des translations qui sont des monomorphismes de schémas, et la surjectivité des endomorphismes radiciels d'EGA~IV, 10.4.11, qui la démontrerait. Mathlib n'a pas les schémas en monoïdes. Le plongement dans $\mathrm M_n$ de la page~30 n'est pas formalisé non plus. \noindent\emph{Le critère d'irréductibilité géométrique de la page~9.} La page~9 porte un \q{Rectificatif sur critère d'irréductibilité géom.} (\lot{53}{1}{9}). La page n'écrit pas \q{$X$ irréductible} ; sa démonstration l'utilise (\q{$p(X'_i) = X$}) et la lecture l'ajoute, car sans cette hypothèse l'énoncé est faux (deux droites disjointes et un point de l'une). Sous la forme corrigée par l'édition, l'énoncé est le suivant. \begin{encadre} \begin{theoreme*}[Page 9, forme corrigée par l'édition, critère d'irréductibilité géométrique\piste{53-geometric-irreducibility-criterion}]\nonverifie Soit $X$ un schéma irréductible sur un corps $k$. Si un $k$-schéma géométriquement irréductible $Z$ s'envoie dans $X$ avec une image non contenue dans l'ensemble des points où passent plusieurs composantes irréductibles de $X_{\bar k}$, alors $X$ est géométriquement irréductible ; un point géométriquement normal de $X_{\mathrm{red}}$ dans l'image suffit. Sans la seconde hypothèse, $x^2 + y^2 = 0$ sur $\mathbf R$, avec pour $Z$ l'origine, est un contre-exemple. \end{theoreme*} \end{encadre} La démonstration de la page se lit ainsi. Soient $k'$ une extension finie galoisienne de $k$, de groupe $G$, $p : X' = X_{k'} \to X$ et $f' : Z' = Z_{k'} \to X'$. L'image $f'(Z')$ est irréductible, puisque $Z'$ l'est, et stable par $G$, puisque $f'$ est défini sur $k$. Elle est contenue dans une composante irréductible $X'_i$ de $X'$. Chaque conjuguée $g X'_i$ est encore une composante et contient $f'(Z')$ ; par l'hypothèse b), un point de $f'(Z')$ n'est que sur une composante, donc $g X'_i = X'_i$. Comme $G$ agit transitivement sur les fibres de $p$, la composante $X'_i$ est l'image réciproque de $p(X'_i)$, et $p(X'_i) = X$ ; donc $X' = X'_i$ est irréductible. Le passage de $k'$ à $\bar k$ se fait par une extension radicielle, qui ne change pas la topologie. Tout le cœur de l'argument est topologique, et c'est cette étape que Lean vérifie, dans une généralité qui ne mentionne plus de corps. \begin{encadre} \begin{enonce}[D'après la page 9, l'étape galoisienne, sous forme topologique] Soient $X'$ et $X$ des espaces sobres, $X$ irréductible, et $p : X' \to X$ une application fermée qui relève les générisations. Soit $G$ un groupe opérant sur $X'$ par homéomorphismes, transitivement sur chaque fibre de $p$. Si une partie irréductible $S$ de $X'$, stable par $G$, contient un point par lequel ne passe qu'une composante irréductible de $X'$, alors $X'$ est irréductible. \end{enonce} \end{encadre} \begin{proof} Soit $C$ une composante irréductible de $X'$ contenant $S$, et $s \in S$ le point de l'hypothèse. Pour $g \in G$, $gC$ est une composante, car $x \mapsto gx$ est un homéomorphisme ; elle contient $g S = S$, donc $s$, et l'unicité donne $gC = C$. Si $p(y) = p(x)$ avec $x \in C$, il existe $g$ avec $y = gx \in gC = C$ : la composante $C$ est saturée pour $p$. Reste à voir que $p(C) = X$. Soient $c$ le point générique de $C$ et $\eta$ celui de $X$. Comme $\eta$ se spécialise en $p(c)$ et que $p$ relève les générisations, il existe $x$ qui se spécialise en $c$ avec $p(x) = \eta$. L'adhérence de $x$ est irréductible et contient $C$, donc lui est égale par maximalité, et $x \in C$. Ainsi $p(C)$ est un fermé qui contient le point générique de $X$ : c'est $X$. Comme $C$ est saturée, $C = p^{-1}(p(C)) = X'$. \end{proof} Dans l'application, $X'$ est $X_{k'}$ et $p$ le morphisme de changement de base : il est fini, donc fermé, et plat, donc il relève les générisations ; les schémas sont sobres, et $\mathrm{Gal}(k'/k)$ opère transitivement sur les fibres. La page justifie $p(X'_i) = X$ par \q{$p$ ouvert et fermé} ; la démonstration ci-dessus remplace l'ouverture par le relèvement des générisations, plus commode à formaliser et vrai ici par platitude. \noindent\emph{Le contre-exemple.} Sur $\mathbf R$, l'anneau $A = \mathbf R[x,y]/(x^2 + y^2)$ est intègre : le morphisme $\mathbf R[x,y] \to \mathbf C[t]$, $x \mapsto t$, $y \mapsto i t$, a pour noyau exactement $(x^2 + y^2)$. En effet, $y^2 + x^2$ est unitaire en $y$ ; un polynôme du noyau a pour reste $a(x) + b(x)\,y$, qui s'envoie sur $a(t) + i\,t\,b(t)$ ; pour $t$ réel, parties réelle et imaginaire donnent $a(t) = 0$ et $t\,b(t) = 0$, d'où $a = b = 0$. Le noyau d'un morphisme vers un anneau intègre est premier, et $X = \operatorname{Spec} A$ est irréductible. Sur $\mathbf C$, en revanche, $x^2 + y^2 = (x + iy)(x - iy)$, et aucun des deux facteurs n'est nilpotent modulo $x^2 + y^2$ : l'évaluation en $(1, -i)$, point du cône, envoie $x + iy$ sur $2$, et l'évaluation en $(1, i)$ envoie $x - iy$ sur $2$. Le nilradical n'est donc pas premier, et $\operatorname{Spec} \mathbf C[x,y]/(x^2 + y^2)$ n'est pas irréductible : ce sont les deux droites $x = \pm i y$. Le point $Z = \operatorname{Spec} \mathbf R$ s'envoie sur l'origine, où elles se coupent : l'hypothèse b) y est en défaut. Au niveau des schémas, le contre-exemple s'énonce avec la définition de Mathlib : un morphisme $X \to S$ est géométriquement irréductible si, pour tout corps $K$ et tout $\operatorname{Spec} K \to S$, le produit fibré $X \times_S \operatorname{Spec} K$ est irréductible. \begin{encadre} \begin{enonce}[Page 9, le contre-exemple au niveau des schémas] On a un isomorphisme de $\mathbf C$-algèbres $\mathbf C \otimes_{\mathbf R} \mathbf R[x,y]/(x^2 + y^2) \simeq \mathbf C[x,y]/(x^2 + y^2)$. Le schéma $X = \operatorname{Spec} \mathbf R[x,y]/(x^2 + y^2)$ est intègre, et il n'est pas géométriquement irréductible sur $\mathbf R$. \end{enonce} \end{encadre} \begin{proof} L'application $z \otimes f \mapsto z f$ de $\mathbf C \otimes_{\mathbf R} \mathbf R[x,y]$ dans $\mathbf C[x,y]$ et l'application $\mathbf C$-linéaire $\mathbf C[x,y] \to \mathbf C \otimes_{\mathbf R} \mathbf R[x,y]$ qui envoie $x$ sur $1 \otimes x$ et $y$ sur $1 \otimes y$ sont des morphismes d'algèbres inverses l'un de l'autre : il suffit de le vérifier sur $x$, $y$ et sur $\mathbf C$. Le produit tensoriel par $\mathbf C$ commute au passage au quotient : $\mathbf C \otimes_{\mathbf R} (\mathbf R[x,y]/I)$ est le quotient de $\mathbf C \otimes_{\mathbf R} \mathbf R[x,y]$ par l'idéal engendré par $1 \otimes I$, et l'isomorphisme précédent envoie $1 \otimes (x^2 + y^2)$ sur $x^2 + y^2$. L'anneau $A$ est intègre (ci-dessus), donc $X$ est intègre. Si $X$ était géométriquement irréductible, la fibre de $X \to \operatorname{Spec} \mathbf R$ au-dessus de $\operatorname{Spec} \mathbf C$ serait irréductible ; c'est $\operatorname{Spec}(A \otimes_{\mathbf R} \mathbf C)$, homéomorphe à $\operatorname{Spec} \mathbf C[x,y]/(x^2 + y^2)$, qui ne l'est pas. \end{proof} \noindent\emph{Portée de la vérification.} Lean démontre l'étape galoisienne (\texttt{irreducibleSpace\_of\_stable}, et \texttt{irreducibleSpace\_of\_map}, où $S$ est l'image d'un espace irréductible $Z'$), avec le lemme \texttt{smul\_mem\_irreducibleComponents}, et le contre-exemple au niveau des anneaux (\texttt{isPrime\_span\_sumSq\_real} par \texttt{ker\_toLines}, et \texttt{not\_irreducibleSpace\_complex}). L'énoncé encadré de la page reste marqué non vérifié : Mathlib a désormais l'irréductibilité géométrique des schémas (\texttt{AlgebraicGeometry.\allowbreak{}GeometricallyIrreducible}), mais il manque, pour en déduire l'énoncé, l'action de $\mathrm{Gal}(k'/k)$ sur $X_{k'}$ et sa transitivité sur les fibres, le passage de toutes les extensions $K$ de $k$ aux extensions finies galoisiennes et l'étape radicielle. Le contre-exemple, lui, est démontré au niveau des schémas : l'isomorphisme $\mathbf C \otimes_{\mathbf R} \mathbf R[x][y] \simeq \mathbf C[x][y]$ (\texttt{baseChangeEquiv}, construit par \texttt{baseChangeHom} et \texttt{baseChangeInv}), puis $\mathbf C \otimes_{\mathbf R} A \simeq \mathbf C[x,y]/(x^2 + y^2)$ (\texttt{tensorQuotSumSqEquiv}, par \texttt{Algebra.\allowbreak{}TensorProduct.\allowbreak{}tensorQuotientEquiv}, \texttt{Ideal.\allowbreak{}quotientEquivAlg} et \texttt{baseChangeEquiv\_tmul\_sumSq}) ; l'intégrité de $X$ (\texttt{isIntegral\_spec\_sumSq}) et l'absence d'irréductibilité géométrique (\texttt{not\_geometricallyIrreducible\_sumSq}, par \texttt{pullbackSpecIso} et \texttt{PrimeSpectrum.\allowbreak{}homeomorphOfRingEquiv}), réunies dans \texttt{isIntegral\_and\_not\_geometricallyIrreducible\_sumSq}, avec la définition \texttt{AlgebraicGeometry.\allowbreak{}GeometricallyIrreducible} de Mathlib. N'est pas formalisée la condition suffisante par un point géométriquement normal de $X_{\mathrm{red}}$. \section[Cote 78 : le critère de fermeture des polygones réguliers sur un anneau, et les 2p-gones en bande]{Cote 78 : le critère de fermeture $u_\alpha^n = 1$ sur un anneau, et les $2p$-gones en bande\protect\verifie{Folder78}}\label{sec:78} La cote 78, \emph{[Polygones réguliers et polynômes cyclotomiques] : notes manuscrites (s.d.)}, que l'inventaire date \q{[à partir de 1977]}, compte cent vingt-neuf pages. Elle cherche une définition du polygone régulier dans un plan affine sur un corps, ou un anneau, quelconque, sans longueurs ni angles : un $n$-gone dont chaque automorphisme combinatoire se prolonge d'une seule façon en une affinité. Dans le repère $(s_0, s_1, s_{-1})$ de trois sommets consécutifs, les pages~81 à~85 ramènent un tel polygone, quand il est \q{propre}, à un seul paramètre $\alpha$, l'invariant numérique, et la rotation s'écrit $u_\alpha(x, y) = (1 - y + \alpha x, x)$ (\lot{78}{5}{81}). Les pages~109 à~113, sous le titre \q{Polynômes cyclotomiques}, définissent des polynômes $F_n \in \mathbb Z[U]$, prouvent une identité entre trois produits consécutifs, écrivent les sommets et la matrice de $u^n$ en fonction de $\alpha$ seul et énoncent, \q{soient $k$ un anneau}, que $u_\alpha^n = 1$ si et seulement si $F_n(\alpha) = 0$ (\lot{78}{6}{109}, \lot{78}{6}{111}, \lot{78}{6}{112}). La page~112 conclut \q{la relation $F_n(\alpha) = 1$} et le premier coefficient de Bézout de la page~113 a un indice douteux ; la lecture modernisée lit $F_n(\alpha) = 0$ et corrige le coefficient. Les pages~84 et~85, puis~94 à~99, décrivent deux polygones de caractéristique $p$ dont les sommets sont alternativement sur deux droites parallèles : l'\q{impropre}, et celui d'invariant $\alpha = -2$ (\lot{78}{5}{85}, \lot{78}{5}{95}, \lot{78}{5}{99}). \noindent\emph{Conventions.} $k$ est un anneau commutatif, $\alpha \in k$, et $S_m \in \mathbb Z[U]$, $m \in \mathbb Z$, les polynômes de Tchebychev de seconde espèce renormalisés : $S_0 = 1$, $S_1 = U$, $S_{m+1} = U S_m - S_{m-1}$, de sorte que $S_{-1} = 0$. On pose \[ F_{2m} = S_{m-1}, \qquad F_{2m+1} = S_m + S_{m-1} \qquad (m \in \mathbb Z), \] d'où $F_0 = 0$, $F_1 = F_2 = 1$, $F_3 = U + 1$, $F_4 = U$, $F_5 = U^2 + U - 1$, $F_6 = U^2 - 1$. On note $u_\alpha$ la bijection $(x, y) \mapsto (1 - y + \alpha x, x)$ de $k^2$, d'inverse $(x, y) \mapsto (y, 1 - x + \alpha y)$, $s_n = u_\alpha^n(0, 0)$ pour $n \in \mathbb Z$, et $\sigma_1(x, y) = (y, x)$. \begin{enonce}[Page 109, les polynômes $F_n$] Les $F_n$ sont ceux de la page : $F_{-n} = -F_n$ et, pour tout $t \in k$ inversible d'inverse $t'$ et tout entier $m \geq 0$, \[ F_{2m+2}(t + t')\,(t^2 - 1)\,t^m = t^{2m+2} - 1, \qquad F_{2m+1}(t + t')\,(t - 1)\,t^m = t^{2m+1} - 1. \] \end{enonce} \begin{proof} L'égalité $F_{-n} = -F_n$ se lit sur $S_{-m-2} = -S_m$. Dans chaque classe de parité, la récurrence de $S$ donne $F_{n+4} = U F_{n+2} - F_n$. Les deux formules se vérifient pour $m = 0$ et $m = 1$ ; si $A_m$ désigne le membre de gauche de l'une d'elles, la récurrence donne $A_{m+2} = (t + t')\,t\,A_{m+1} - t^2 A_m$, et $(t^2 + tt')(t^{j+2} - 1) - t^2(t^j - 1) = t^{j+4} - 1 + (tt' - 1)(t^{j+2} - 1)$. \end{proof} \begin{theoreme}[Grothendieck, pages 109 à 113, le critère de fermeture sur un anneau\piste{78-closure-criterion-over-rings}] \leavevmode \begin{enumerate} \item Pour tout $n \in \mathbb Z$, on a dans $\mathbb Z[U]$ \[ F_n F_{n+1} - U F_{n-1} F_n + F_{n-2} F_{n-1} = 1, \] c'est-à-dire $A_n F_{n-1} + F_n F_{n+1} = 1$ avec $A_n = F_{n-2} - U F_n$ ; en particulier $F_{n-1}$ et $F_{n+1}$ sont étrangers. \item Pour tout $n \in \mathbb Z$ et tout $(x, y) \in k^2$, avec $X_n = F_n F_{n+1}(\alpha)$, \[ u_\alpha^n(x, y) = (1 - x - y)\, s_n + x\, s_{n+1} + y\, s_{n-1}, \] où $s_n = (X_n, X_{n-1}) = \bigl(F_n F_{n+1}(\alpha), F_{n-1} F_n(\alpha)\bigr)$. \item Pour $n \in \mathbb Z$, les conditions suivantes sont équivalentes : a) $u_\alpha^n = \mathrm{id}$ ; b) $s_n = s_0$ ; c) $u_\alpha^n(s_i) = s_i$, pour un $i \in \mathbb Z$ donné ; d) $F_n(\alpha) = 0$. \end{enumerate} \end{theoreme} \begin{proof} 1) Si $n = 2m$, les quatre polynômes sont $S_{m-1}$, $S_m + S_{m-1}$, $S_{m-1} + S_{m-2}$ et $S_{m-2}$ ; en remplaçant $S_m$ par $U S_{m-1} - S_{m-2}$, le membre de gauche devient $S_{m-1}^2 - U S_{m-1} S_{m-2} + S_{m-2}^2$. Si $n = 2m + 1$, il devient de même $S_m^2 - U S_m S_{m-1} + S_{m-1}^2$. Or $Q_m = S_m^2 - U S_m S_{m-1} + S_{m-1}^2$ ne dépend pas de $m$ : $Q_{m+1} = S_{m+1}(S_{m+1} - U S_m) + S_m^2 = -S_{m+1} S_{m-1} + S_m^2 = Q_m$, et $Q_0 = 1$. C'est l'identité de Cassini des $S_m$. La relation de Bézout n'en est qu'une réécriture. 2) L'identité au rang $n + 1$, évaluée en $\alpha$, donne $X_{n+1} = \alpha X_n - X_{n-1} + 1$ pour tout $n$. Notons $V_n(x, y)$ le membre de droite. On a $V_0(x, y) = (x, y)$, puisque $X_0 = X_{-1} = 0$ et $X_1 = X_{-2} = 1$. La récurrence donne $u_\alpha \circ V_n = V_{n+1}$ : la seconde coordonnée de $u_\alpha(V_n(x, y))$ est la première de $V_n(x, y)$, et la première est $1 - (\text{seconde}) + \alpha\,(\text{première})$, où l'on remplace chacun des trois termes $1 - X_{j-1} + \alpha X_j$ par $X_{j+1}$, pour $j = n$, $n + 1$, $n - 1$, les poids $1 - x - y$, $x$, $y$ ayant pour somme $1$. On conclut par récurrence vers le haut et, comme $u_\alpha$ est bijective, vers le bas. 3) a) $\Rightarrow$ b) est clair. d) $\Rightarrow$ a) : si $F_n(\alpha) = 0$, alors $X_n = X_{n-1} = 0$, puis $X_{n+1} = 1$ et $X_{n-2} = 1$ par la récurrence, et la formule de 2) se réduit à $u_\alpha^n(x, y) = (x, y)$. b) $\Rightarrow$ d) : si $F_n F_{n+1}(\alpha) = F_{n-1} F_n(\alpha) = 0$, on multiplie l'identité évaluée en $\alpha$ par $F_n(\alpha)$ : \[ F_n(\alpha) = F_n(\alpha)\cdot F_nF_{n+1}(\alpha) + \bigl(F_{n-2}(\alpha) - \alpha F_n(\alpha)\bigr)\cdot F_{n-1}F_n(\alpha) = 0. \] c) $\Leftrightarrow$ b) : $u_\alpha^n$ et $u_\alpha^i$ commutent, donc $u_\alpha^n(s_i) = u_\alpha^i(s_n)$, et $u_\alpha^i$ est injective. \end{proof} \begin{remarque} Le théorème tient tel que la lecture l'énonce, sur tout anneau commutatif et pour tout $n \in \mathbb Z$, diviseurs de zéro compris : la réciproque passe par la relation de Bézout et non par une factorisation. Les colonnes de la formule 2) sont $s_{n+1} - s_n$, $s_{n-1} - s_n$ et $s_n$, soit $\bigl(F_{n+1}(F_{n+2} - F_n), F_n(F_{n+1} - F_{n-1})\bigr)$, $\bigl(F_n(F_{n-1} - F_{n+1}), F_{n-1}(F_{n-2} - F_n)\bigr)$ et $(F_n F_{n+1}, F_{n-1} F_n)$ : c'est la première version de la matrice de la page~111, celle qui est barrée, que la lecture retient. La suite $X_n$ vérifie une récurrence linéaire d'ordre deux avec second membre, et, avec la suite de Lucas $U_m = U_m(\alpha, 1)$ ($U_0 = 0$, $U_1 = 1$, $U_{m+1} = \alpha U_m - U_{m-1}$) \cite{lucas1878}, on a $F_{2m}(\alpha) = U_m$ et $F_{2m+1}(\alpha) = U_{m+1} + U_m$ ; la piste demande si l'équivalence sur un anneau quelconque y figure déjà, sous un autre nom. Le fichier vérifie aussi que $\sigma_1 u_\alpha \sigma_1 = u_\alpha^{-1}$ et $\sigma_1(s_n) = s_{-n}$, de sorte que $u_\alpha$ et $\sigma_1$ font opérer le groupe diédral sur les sommets, et que la forme $f_\alpha(x, y) = x^2 - x + y^2 - y - \alpha xy$ de la page~96 est invariante par $u_\alpha$ et nulle en tous les sommets. Enfin une affinité de $k^2$ est déterminée par ses valeurs en $s_0 = (0, 0)$, $s_1 = (1, 0)$ et $s_{-1} = (0, 1)$ : un automorphisme du polygone combinatoire se prolonge au plus d'une façon. \end{remarque} \begin{contrexemple}[Page 113, le coefficient de la page] Le couple $A_n = F_{n-2} - U F_{n-1}$, $B_n = F_n$ ne vérifie pas $A_n F_{n-1} + B_n F_{n+1} = 1$ pour $n = 4$. \end{contrexemple} \begin{proof} Pour $n = 4$, $(1 - U(U + 1))(U + 1) + U(U^2 + U - 1) = 1 - U - U^2$, qui vaut $-1$ en $U = 1$. \end{proof} \noindent\emph{Les deux polygones en bande.} Pour $\alpha = -2$, $u_{-2}(x, y) = (1 - y - 2x, x)$ ; le polygone impropre de la page~85 a pour rotation $v(x, y) = (1 - y, -x)$, et l'on pose $t_n = v^n(0, 0)$. Une \emph{caractéristique} $p$ est un entier $p \geq 0$ tel que, pour $m \in \mathbb Z$, l'image de $m$ dans $k$ soit nulle si et seulement si $p$ divise $m$ ; on suppose $k$ non nul. \begin{enonce}[Pages 84, 85 et 94 à 99, existence des $2p$-gones en bande\piste{78-strip-2p-gon}] Soit $k$ un anneau non nul de caractéristique $p$. \begin{enumerate} \item Pour $m \in \mathbb Z$, $s_{2m} = (-m, m)$ et $s_{2m+1} = (1 + m, -m)$ : les sommets pairs sont sur la droite $x + y = 0$, les impairs sur la droite parallèle $x + y = 1$, et $f_{-2}(x, y) = (x + y)(x + y - 1)$. \item $u_{-2}^n = \mathrm{id}$ si et seulement si $2p$ divise $n$, ce qui équivaut à $F_n(-2) = 0$ ; $u_{-2}$ est d'ordre $2p$, et $s_n = s_m$ si et seulement si $2p$ divise $n - m$. \item Trois sommets consécutifs ne sont jamais alignés : le déterminant de $(s_{n+1} - s_n, s_{n-1} - s_n)$ vaut $1$. La partie linéaire $(x, y) \mapsto (-2x - y, x)$ est de déterminant~$1$. \item Pour le polygone impropre, $v^{2m}$ est la translation de vecteur $m\,(1, -1)$, $t_{2m} = (m, -m)$ et $t_{2m+1} = (m + 1, -m)$, sur les deux mêmes droites ; $v^n = \mathrm{id}$ si et seulement si $2p$ divise $n$, $v$ est d'ordre $2p$, $t_n = t_m$ si et seulement si $2p$ divise $n - m$, trois sommets consécutifs ne sont pas alignés (déterminant $\pm 1$), $\sigma_1 v \sigma_1 = v^{-1}$, et la partie linéaire $(x, y) \mapsto (-y, -x)$ est de déterminant $-1$. \end{enumerate} \end{enonce} \begin{proof} 1) Par récurrence sur $m$ dans les deux sens : $u_{-2}(-m, m) = (1 + m, -m)$ et $u_{-2}(1 + m, -m) = (-(m + 1), m + 1)$. La factorisation de $f_{-2}$ est immédiate. 2) Par 1), $s_{2m} = (0, 0)$ équivaut à $m = 0$ dans $k$, c'est-à-dire à $p \mid m$, ou encore à $2p \mid 2m$ ; et $s_{2m+1} = (0, 0)$ imposerait $m = 0$ et $1 + m = 0$, donc $1 = 0$. Le théorème ci-dessus (b $\Leftrightarrow$ a $\Leftrightarrow$ d) donne $u_{-2}^n = \mathrm{id} \iff 2p \mid n \iff F_n(-2) = 0$, d'où l'ordre. Enfin $s_n = s_m$ équivaut à $u_{-2}^{n-m}(s_m) = s_m$, donc à $2p \mid n - m$ par la condition c). 3) Pour $n = 2m$, les deux vecteurs sont $(1 + 2m, -2m)$ et $(2m, 1 - 2m)$, de déterminant $1 - 4m^2 + 4m^2 = 1$ ; le cas impair est analogue. 4) $v(1 - y + m, -x - m) = (x + m + 1, y - m - 1)$ et $v(x + m, y - m) = (1 - y + m, -x - m)$ donnent par récurrence $v^{2m}(x, y) = (x + m, y - m)$ et $v^{2m+1}(x, y) = (1 - y + m, -x - m)$. Les sommets s'en déduisent, et l'on raisonne comme en 2) : $t_{2m} = (0, 0)$ si et seulement si $p \mid m$, $t_{2m+1} \neq (0, 0)$, et $v^{2m}$ est l'identité dès que $m = 0$ dans $k$. Les déterminants se calculent sur les sommets : les vecteurs sont $(1, 0)$ et $(0, 1)$ en un sommet pair, $(0, -1)$ et $(-1, 0)$ en un sommet impair. \end{proof} Le polygone d'invariant $\alpha = -2$, dessiné sur $\mathbf Q$ dans les coordonnées $(x - y,\ x + y)$ : les sommets pairs sur la droite $x + y = 0$, les impairs sur $x + y = 1$, de $s_{-2}$ à $s_5$. Sur $\mathbf Q$ il ne se referme pas ; en caractéristique $p$, $s_{n + 2p} = s_n$ et c'est un $2p$-gone. \begin{center} \begin{tikzpicture}[x=0.95cm, y=1.5cm, every node/.style={font=\small}] \draw[black!45] (-4.6,0) -- (5.6,0) node[right] {$x + y = 0$}; \draw[black!45] (-4.6,1) -- (5.6,1) node[right] {$x + y = 1$}; \coordinate (a) at (2,0); % s_{-2} \coordinate (b) at (-1,1); % s_{-1} \coordinate (c) at (0,0); % s_0 \coordinate (d) at (1,1); % s_1 \coordinate (e) at (-2,0); % s_2 \coordinate (f) at (3,1); % s_3 \coordinate (g) at (-4,0); % s_4 \coordinate (h) at (5,1); % s_5 \draw (a)--(b)--(c)--(d)--(e)--(f)--(g)--(h); \foreach \p in {a,b,c,d,e,f,g,h} \fill (\p) circle (1.5pt); \node[below] at (a) {$s_{-2}$}; \node[above] at (b) {$s_{-1}$}; \node[below] at (c) {$s_0$}; \node[above] at (d) {$s_1$}; \node[below] at (e) {$s_2$}; \node[above] at (f) {$s_3$}; \node[below] at (g) {$s_4$}; \node[above] at (h) {$s_5$}; \end{tikzpicture} \end{center} \begin{remarque} L'existence tient en toute caractéristique, sans supposer $p$ premier ni impair. Pour $p = 2$, $\alpha = -2 = 0$ et l'on retrouve le carré, d'ordre $4 = 2p$, comme le note la lecture ; pour $p = 0$, les deux rotations sont d'ordre infini et les sommets forment les deux $\infty$-polygones en escalier de la page~85. Le déterminant $-1$ ne sépare le polygone impropre des polygones unimodulaires que si $2 \neq 0$, c'est-à-dire pour $p$ impair. Les formules 1) et 4) montrent que les deux polygones ont le même ensemble de sommets : $s_{2m+1} = t_{2m+1}$ et $s_{2m} = t_{-2m}$. Le premier zigzague en parcourant les deux droites en sens contraires, $(0, 0)$, $(1, 0)$, $(-1, 1)$, $(2, -1)$, et ainsi de suite ; le second monte en escalier en les parcourant dans le même sens, $(0, 0)$, $(1, 0)$, $(1, -1)$, $(2, -1)$, et ainsi de suite. Ils ne diffèrent que par l'ordre des sommets et par le déterminant de la rotation. \end{remarque} Ne sont pas démontrés ici : l'énoncé de la piste selon lequel le $2p$-gone impropre est le seul polygone régulier fini non unimodulaire, que la lecture ajoute et qui demande la classification des réalisations régulières ; la proposition de la page~83, qui met les réalisations épinglées en bijection avec les couples $(\alpha, \beta)$ vérifiant $\alpha\beta = 0$ et $\beta(\beta + 2) = 0$ ; la factorisation $F_n = \prod_{d \mid n,\, d \geq 3} \Psi_d$ et le polynôme semi-cyclotomique $\Psi_n$ des pages~114 à~120, avec la réduction $\Psi_p \equiv (U - 2)^{(p-1)/2}$ modulo $p$ ; le $p$-gone de la parabole (pages~95 et~100), dont la piste est retrouvée dans la littérature ; les gerbes et la descente des pages~39 à~48. \section[Cote 64 : la configuration octaédrale en caractéristique 5]{Cote 64 : la configuration octaédrale en caractéristique 5\protect\verifie{Folder64}}\label{sec:64} La cote 64, \emph{Modules courbes elliptiques en caractéristiques $\neq 2$ : notes manuscrites (s.d.)}, cent cinquante-six pages que l'inventaire date \q{[à partir de 1980-1982]}, consacre sa partie~II aux structures octaédrales dans $\mathbf P^1$ (pages~43 à~52, \lot{64}{3}{44}). Une action fidèle du groupe de Klein se met localement sous la forme $\sigma_1(z) = -z$, $\sigma_2(z) = 1/z$, et la somme des axes est la configuration octaédrale $\Delta = \{0, \infty, \pm 1, \pm i\}$. Pour identifier $\mathrm{Aut}(X, \Delta)$ au groupe des rotations de l'octaèdre, la page~48 calcule le fixateur de deux sommets non opposés, $\infty$ et $-1$ : un tel automorphisme s'écrit $z \mapsto az + (a - 1)$, et s'il n'est pas l'identité il permute $\{0, 1, i, -i\}$. Les quatre conditions sur $a$ qui en résultent ont, dit la page, une intersection vide hors des caractéristiques $2$ et~$5$. La marge borne le calcul par \q{car.\ $\neq 3$ et $5$}, et la lecture ajoute l'hypothèse \q{$5$ inversible} partout où elle sert. \begin{theoreme}[Grothendieck, page 48]\label{thm:64-fixateur} Soit $K$ un corps où $2 \neq 0$, et $i \in K$ avec $i^2 = -1$. Si $z \mapsto az + (a - 1)$ envoie $\{0, 1, i, -i\}$ dans lui-même, alors $5(a - 1) = 0$. En particulier, si $5 \neq 0$ dans $K$, le fixateur de $\infty$ et $-1$ dans $\mathrm{Aut}(\mathbf P^1_K, \Delta)$ est trivial. \end{theoreme} \begin{proof} Les quatre points sont distincts, puisque $2 \neq 0$. Si $a = 0$, l'image de $0$ est $-1$, qui n'est aucun des quatre points. Sinon l'application est injective, donc permute les quatre points, et conserve leur somme, qui vaut~$1$ ; or elle la change en $a \cdot 1 + 4(a - 1) = 5a - 4$. D'où $5(a - 1) = 0$. \end{proof} Les six points de $\Delta$ sont les sommets d'un octaèdre dont les sommets opposés sont $0$ et $\infty$, $1$ et $-1$, $i$ et $-i$. Le fixateur de deux sommets non opposés, $\infty$ et $-1$ (cerclés), permute les quatre autres. \begin{center} \begin{tikzpicture}[x=1cm, y=1cm, every node/.style={font=\small}] \coordinate (inf) at (0,1.9); \coordinate (z) at (0,-1.9); \coordinate (p1) at (1.9,-0.25); \coordinate (m1) at (-1.9,0.25); \coordinate (pi) at (0.7,0.55); \coordinate (mi) at (-0.7,-0.55); \draw (m1)--(mi)--(p1); \draw[densely dashed] (p1)--(pi)--(m1); \foreach \v in {m1,mi,p1} { \draw (inf)--(\v); \draw (z)--(\v); } \draw[densely dashed] (inf)--(pi); \draw[densely dashed] (z)--(pi); \foreach \v in {inf,z,p1,m1,pi,mi} \fill (\v) circle (1.5pt); \draw (inf) circle (4pt); \draw (m1) circle (4pt); \node[above=3pt] at (inf) {$\infty$}; \node[below=2pt] at (z) {$0$}; \node[right=2pt] at (p1) {$1$}; \node[left=3pt] at (m1) {$-1$}; \node at (0.95,0.13) {$i$}; \node at (-1.02,-0.1) {$-i$}; \end{tikzpicture} \end{center} \begin{contrexemple}[énoncé de l'édition, d'après la note de la lecture à la page 49]\label{ce:64-car5} En caractéristique~$5$, le fixateur de $\infty$ et $-1$ n'est pas trivial : $z \mapsto 2z + 1$ permute $\{0, 1, i, -i\}$. Sur $\mathbf F_5$, avec $i = 2$, la configuration $\Delta$ est $\mathbf P^1(\mathbf F_5)$ tout entier ; les bijections de $\mathbf P^1(\mathbf F_5)$ induites par $\mathrm{GL}_2(\mathbf F_5)$, qui préservent toutes $\Delta$, sont au nombre de $120$ et non de $24$, et le fixateur de $\infty$ et $-1$ est formé de l'identité et des $z \mapsto az + (a - 1)$ pour $a = 2, 3, 4$. \end{contrexemple} \begin{proof} Comme $i^2 = -1 = 4$, $i = \pm 2$. Pour $i = 2$, l'application $z \mapsto 2z + 1$ envoie $0 \mapsto 1 \mapsto 3 = -i \mapsto 2 = i \mapsto 0$ ; de même pour $i = -2$. Sur $\mathbf F_5$, les six points $\infty, 0, 1, -1, 2, -2$ sont les six points de $\mathbf P^1(\mathbf F_5)$. Le décompte des bijections induites et du fixateur se fait sur les $625$ matrices de $M_2(\mathbf F_5)$ ; Lean le vérifie par calcul (\texttt{card\_pgl}, \texttt{card\_fixer}). \end{proof} \begin{remarque} La démonstration du théorème~\ref{thm:64-fixateur} n'utilise que $2 \neq 0$ et $5 \neq 0$ : la caractéristique~$3$, que la marge exclut, n'a pas à l'être. Le contre-exemple confirme l'hypothèse \q{$5$ inversible} de la lecture : sans elle, $\mathrm{Aut}(X, \Delta)$ est $\mathrm{PGL}_2(\mathbf F_5)$, d'ordre $120$, et non le groupe des rotations de l'octaèdre, d'ordre~$24$. \end{remarque} Ne sont pas démontrés ici : la forme normale locale de la page~46, l'égalité $\mathrm{Aut}(X, \Delta) = \mathrm{Aut}^+_{\mathrm{oct}}(\Delta)$ qui suit du théorème, et les énoncés relatifs au-dessus d'une base, qui restent ouverts : \begin{encadre} \begin{theoreme*}[Grothendieck, pages 44 à 52, configurations octaédrales sur une base ; voir aussi Beauville~\cite{beauville2010}\piste{64-octahedral-configurations-relative}]\nonverifie Soit $X$ un fibré en droites projectives sur un schéma $S$ de caractéristiques résiduelles différentes de~$2$. Se correspondent bijectivement : les sous-schémas en groupes de $\mathrm{Aut}_S(X)$ localement isomorphes à $(\mathbf Z/2)^2$, ceux localement isomorphes à $\mathfrak S_4$, et les configurations octaédrales régulières, diviseurs étales de degré~$6$ munis d'une antipodie. Les couples $(X, \Delta)$ dont le torseur d'orientation est identifié à $\mu_4^*$ équivalent aux revêtements étales finis de degré~$4$ de~$S$. \end{theoreme*} \end{encadre} {\small Les feuillets en esquissent une démonstration incomplète (pages 46 à 49). Le corollaire~2 n'est pas démontré, et l'hypothèse qui en fait une équivalence est une addition marginale de lecture incertaine. Là où la page identifie $\mathrm{Aut}_S(X, \Delta)$ au groupe des rotations de l'octaèdre, l'édition suppose $5$ inversible, hypothèse nécessaire par le contre-exemple~\ref{ce:64-car5}. Beauville traite le cas d'un corps, sans base. Mathlib n'a pas les formes de $\mathbf P^1$ sur une base.\par} \begin{encadre} \begin{theoreme*}[Grothendieck, pages 74 à 79 et 84 à 91, épinglages de Legendre ; voir aussi Antieau--Meier~\cite{antieaumeier2020}\piste{64-legendre-pinning-moduli}]\nonverifie Sur $\mathbf Z[1/2]$, les courbes elliptiques munies d'un épinglage de Jacobi de niveau~$2$ et d'un épinglage de Legendre (un vecteur tangent à l'origine, tordu par un $\mu_4$-torseur fixé, dont le carré correspond à l'espace tangent de $E/\pm1$ en l'image de l'origine) forment un groupoïde rigide représenté par $U_{0,3} \times \mu_4^*$. Le groupe $\mu_4 \times \mathfrak S_3$ opère sur ce schéma, $\mathfrak S_3$ tautologiquement sur $U_{0,3}$ et par la signature sur~$\mu_4^*$. \end{theoreme*} \end{encadre} {\small La représentabilité est affirmée sans démonstration (page~85). Antieau et Meier (2020, définition~4.4, proposition~4.5 et lemme~4.7 dans la numérotation de arXiv:1608.00851) décrivent, sur $\mathbf Z[1/2]$, l'espace de Legendre $X = \mathbf A^1 \smallsetminus \{0, 1\}$ comme le $C_2$-torseur des racines carrées de $p\,\omega^{\otimes 2}$ au-dessus de $\mathcal M(2) \simeq BC_{2,X}$, et notent que l'action de $\mathfrak S_3$ ne se relève pas strictement à $X$ ; l'épinglage tordu par $\mu_4^*$, qui rend l'action de $\mu_4 \times \mathfrak S_3$ stricte sur $U_{0,3} \times \mu_4^*$, n'y figure pas. Le $\mathfrak S_3$ qui opère ici sur $U_{0,3}$ est celui des sections~\ref{sec:62} et~\ref{sec:146}. Mathlib n'a pas les espaces de modules de courbes elliptiques. On se reportera aux notes de Grothendieck (\lot{64}{4}{74}).\par} \section[Cote 80 : un contre-exemple au théorème des arrangements cruciaux]{Cote 80 : un contre-exemple au théorème des arrangements cruciaux\protect\verifie{Folder80}}\label{sec:80} La cote 80, \emph{Systèmes de pseudo-droites}, n'est pas datée de sa main ; l'inventaire la date \q{à partir de 1981}, et une notice administrative du 13~mai 1981, à la page~27, appuie cette date. Un arrangement de pseudo-droites est une famille finie de courbes fermées simples du plan projectif réel qui se coupent deux à deux en un seul point ; les droites en sont l'exemple. Les pages~20 à~28 cherchent les arrangements \q{cruciaux} et leur donnent des noms (\lot{80}{2}{22}) : $\mathrm{I}_N$, $\mathrm{I}_{p,q}$ et $\mathrm{II}'_{p,q}$ sont formés de deux faisceaux, c'est-à-dire que deux sommets suffisent pour que chaque pseudo-droite passe par l'un d'eux ; $\mathrm{II}_4$ et $\mathrm{II}_5$ sont quatre et cinq pseudo-droites en position générale, sans trois concourantes ; $\mathrm{III}_6$ est le quadrangle complet, les six droites qui joignent quatre points dont trois ne sont jamais alignés (quatre points triples) ; $\mathrm{IV}_7$ est un quadrilatère complet et ses trois diagonales. La page~24 énonce (\lot{80}{2}{24}) : \begin{quote} \emph{Théorème : supposons qu'il n'existe pas deux sommets tels que les ps.\ droites passent par l'un d'eux [\dots]. Supposons de plus que K ne contienne pas de sous-arrangement du type $\mathrm{II}_5$ ; elle est de l'un des types suivants : $\mathrm{III}_6$, $\mathrm{IV}_7$.} \end{quote} \noindent Pour le réfuter, des droites suffisent. On écrit une droite $u_0x + u_1y + u_2z = 0$ du plan projectif comme un triplet d'entiers $u$ ; trois droites $u, v, w$ sont concourantes si et seulement si le déterminant de la matrice de lignes $u, v, w$ est nul. Toutes les vérifications deviennent alors des calculs finis sur des entiers. \begin{encadre} \begin{contrexemple}[Énoncé de l'édition, page 24] Soient $A = (0, 0)$, $B = (1, 0)$, $C = (0, 1)$ dans le plan affine, et les six droites \[ AB : y = 0, \quad BC : x + y = 1, \quad CA : x = 0, \quad a : y = 2x, \quad b : y = 3x - 3, \quad c : y = 5x + 1, \] les trois dernières passant respectivement par $A$, $B$ et $C$. Cet arrangement a exactement trois points triples, $A$, $B$ et $C$ ; il n'existe pas deux sommets par l'un desquels passe chacune des six droites ; cinq quelconques d'entre elles contiennent trois droites concourantes, de sorte qu'il ne contient pas de $\mathrm{II}_5$ ; il n'est ni $\mathrm{III}_6$, qui a quatre points triples, ni $\mathrm{IV}_7$, qui a sept droites. \end{contrexemple} \end{encadre} \begin{proof} Les triplets sont $(0, 1, 0)$, $(1, 1, -1)$, $(1, 0, 0)$, $(2, -1, 0)$, $(3, -1, -3)$ et $(5, -1, 1)$. Parmi les vingt triples de droites, trois seulement ont un déterminant nul : $\{AB, CA, a\}$, $\{AB, BC, b\}$ et $\{BC, CA, c\}$, qui concourent en $A$, $B$ et $C$. Deux droites distinctes sont toujours non proportionnelles, puisque chacune forme avec l'autre et une troisième un déterminant non nul. Un sommet est l'intersection de deux droites, et une droite y passe si elle est l'une des deux ou si elle forme avec elles un triple concourant. Chaque point triple porte trois droites et chaque point double deux, et deux points triples distincts ont une droite commune, un côté du triangle : deux sommets portent au plus cinq droites, jamais six. Cinq droites parmi six en omettent une. Si c'est un côté, disons $BC$, les droites $AB$, $CA$ et $a$ restent et concourent en $A$ ; si c'est $a$, il reste $AB$, $BC$ et $b$, qui concourent en $B$, et de même pour $b$ et $c$. Enfin il y a trois points triples et non quatre, et six droites et non sept. En Lean, ces assertions sont décidées par calcul sur les entiers. \end{proof} \begin{remarque} Le contre-exemple contient un $\mathrm{II}'_{3,2}$, trois pseudo-droites par un point et deux par un autre sans droite de jonction : les cinq droites $AB$, $CA$, $a$, $b$, $c$ n'ont qu'un triple concourant, $\{AB, CA, a\}$. La forme encadrée de la page~24, et la version corrigée par la lecture où l'on exclut aussi $\mathrm{II}'_{3,2}$, ne sont donc pas atteintes. La lecture corrige aussi la parenthèse de la page parce que $\mathrm{IV}_7$ contient lui aussi un $\mathrm{II}'_{3,2}$, et cela se vérifie de la même façon : pour le carré $A = (0, 0)$, $B = (1, 0)$, $C = (1, 1)$, $D = (0, 1)$, avec $E = AB \cap CD$ et $F = AD \cap BC$ à l'infini, les sept droites $AB$, $BC$, $CD$, $DA$, $AC$, $BD$, $EF$ ont six points triples, et parmi elles $AB$, $AD$, $AC$, $BD$, $EF$ n'ont que le triple $\{AB, AD, AC\}$. \end{remarque} Le calcul porte sur des droites. Un arrangement de droites est un arrangement de pseudo-droites, et le contre-exemple vaut donc pour l'énoncé de la page tel qu'il est écrit ; les pseudo-droites en général ne sont pas formalisées. Viennent ensuite les autres énoncés de la cote, avec ce qu'en dit Lean. \begin{encadre} \begin{theoreme*}[Grothendieck, pages 20, 24 et 28, arrangements sans bigones\piste{80-bigon-free-five-line-dichotomy}]\verifie{Folder80Maps2} Tout arrangement de pseudo-droites du plan projectif réel sans pseudo-droite bigonale est l'arrangement simple de quatre pseudo-droites ($\mathrm{II}_4$), ou contient un sous-arrangement de l'un de trois types : cinq pseudo-droites en position générale ($\mathrm{II}_5$), un faisceau de trois et un faisceau de deux sans la droite qui joint leurs centres ($\mathrm{II}'_{3,2}$), ou le quadrangle complet ($\mathrm{III}_6$). \end{theoreme*} \end{encadre} {\small La page tire cet énoncé du théorème de la page~24, faux tel qu'il est écrit, et ne donne pour le lemme de la page~28 qu'une \q{idée} ; le nom $\mathrm{II}'_{3,2}$ est de la lecture. L'édition le démontre, sans Lean, avec le lemme de numérotation. Un arrangement sans bigones n'est pas un quasi-faisceau (chaque droite du faisceau n'y porte que le centre et son point sur la transversale) ; il a donc un point double $p = a \cap b$ (Kelly et Rottenberg, théorème~3.6 \cite{kellyrottenberg1972} ; voir aussi Bokowski et Pokora \cite{bokowskipokora2018}). La droite $a$ porte au moins deux autres sommets $q_i$, $q_j$ ; deux pseudo-droites $c \ni q_i$ et $d \ni q_j$ qui coupent $b$ en des points distincts forment avec $a$, $b$ quatre pseudo-droites en position générale $Q$, et s'il n'en existe pas, toutes passent par un même point de $b$, qui est alors bigonale. Une autre pseudo-droite qui ne passe par aucun ou par un seul des six sommets de $Q$ donne $\mathrm{II}_5$ ou $\mathrm{II}'_{3,2}$ ; sinon c'est une diagonale du quadrilatère $Q$, passant par deux sommets opposés ; une diagonale seule serait bigonale, deux donnent $\mathrm{III}_6$. Pour la numérotation, on part de $\mathrm{III}_6$ s'il est présent (toute pseudo-droite coupe ses six côtés en au moins trois points), sinon de $Q$, en ajoutant en dernier la diagonale éventuelle ; ajouter une pseudo-droite n'ôte aucun sommet aux autres, si bien que chaque arrangement partiel est sans bigones. Une énumération par ordinateur de tous les arrangements d'au plus neuf pseudo-droites le confirme. La version combinatoire est vérifiée en Lean (\texttt{Folder80Maps2.lean}) pour les cartes combinatoires de la page~60 : une carte généralisée (drapeaux et trois involutions) de caractéristique d'Euler~$1$, dont les drapeaux sont étiquetés par les pseudo-droites, chacune connexe et passant une fois par chacun de ses sommets, deux d'entre elles se coupant en un seul sommet ; \q{sans bigone} veut dire que chaque pseudo-droite porte au moins trois sommets, ce qui exclut aussi les faisceaux (\texttt{map\_dichotomy}). L'inégalité de Melchior, tirée de $\chi = 1$ et de ce que les faces ont au moins trois côtés (le squelette n'a ni boucle ni arête multiple), donne un point double (\texttt{melchior}) ; le reste est de l'incidence pure : quatre pseudo-droites en position générale, puis une cinquième, qui donne $\mathrm{II}_5$, $\mathrm{II}'_{3,2}$ ou une diagonale ; deux diagonales donnent $\mathrm{III}_6$, une seule est bigonale (\texttt{dichotomy}). Le lemme de numérotation de la page~28 et le passage d'un arrangement topologique à sa carte ne sont pas formalisés. On se reportera aux notes de Grothendieck (\lot{80}{1}{20}).\par} \begin{encadre} \begin{theoreme*}[D'après les pages 24 et 26, cas latticiel, condition b) lue par l'édition\piste{80-lattice-criterion}]\nonverifie Pour un arrangement de pseudo-droites du plan projectif réel, les cellules fermées de la décomposition induite se coupent deux à deux suivant le vide ou une seule cellule fermée si et seulement si aucune pseudo-droite n'est bigonale et l'arrangement n'est pas l'arrangement simple de quatre pseudo-droites~$\mathrm{II}_4$. \end{theoreme*} \end{encadre} {\small La page~26 l'énonce sans démonstration. Vérifié en Lean (\texttt{Folder80Maps1.lean}) : l'énoncé est faux dans le sens « si », déjà pour de vraies droites. L'arrangement $\mathrm{II}'_{3,2}$, formé des droites $x = 0$, $x = z$, $x = 2z$ et $y = 0$, $y = z$, n'a pas de pseudo-droite bigonale et n'est pas $\mathrm{II}_4$, mais ses deux faces « de coin » ont pour intersection les deux centres $[0 : 1 : 0]$ et $[1 : 0 : 0]$, qui ne forment pas une cellule (\texttt{lattice\_criterion\_false}) ; la page~24 le dit pourtant latticiel. Le critère juste, démontré dans le modèle des covecteurs (signes des points, fermeture topologique comprise), est : on est dans le cas latticiel si et seulement s'il n'existe pas deux points par l'un desquels passe chaque pseudo-droite, c'est-à-dire si l'arrangement n'est d'aucun des types $\mathrm{I}_N$, $\mathrm{I}_{p,q}$, $\mathrm{II}'_{p,q}$, l'hypothèse même du théorème de la page~24 (\texttt{lattice\_iff}, \texttt{lattice\_iff\_not\_twoPencil}). Le sens « seulement si » de la page tient : une pseudo-droite bigonale, ou $\mathrm{II}_4$, fournit deux tels points (\texttt{not\_lattice\_of\_bigonal}, \texttt{not\_lattice\_of\_four}). Le critère abstrait vaut pour tout ensemble de vecteurs de signes symétrique et stable par composition, donc pour toute pseudo-droite par la représentation de Folkman--Lawrence, qui n'est pas formalisée. On se reportera aux notes de Grothendieck (\lot{80}{2}{24}).\par} \begin{encadre} \begin{theoreme*}[Grothendieck, pages 39 à 54, squelette d'un arrangement sans bigones\piste{80-skeleton-full-faithfulness}]\nonverifie Un arrangement combinatoire de pseudo-droites du plan projectif réel sans pseudo-droite bigonale est déterminé par son $1$-squelette muni de la décomposition des arêtes en pseudo-droites, et cela fonctoriellement : le foncteur des arrangements sans bigones vers les arrangements de dimension~$1$ sans bigones est pleinement fidèle, de sorte que tout automorphisme du squelette décomposé vient de la carte. \end{theoreme*} \end{encadre} {\small Les feuillets en esquissent une démonstration incomplète (pages 41 à 54). Les conditions (A1) à (A6) y sont dites satisfaites \q{bien entendu}, sans démonstration, et l'indépendance des choix en~(34) n'est pas vérifiée. Partiellement vérifié en Lean (\texttt{Folder80Maps3.lean}), pour les cartes combinatoires de la page~60 (carte généralisée de caractéristique d'Euler~$1$ étiquetée par les pseudo-droites, sans bigone, chaque pseudo-droite allant tout droit en chaque sommet). Le foncteur est fidèle (\texttt{faithful}). Le \q{théorème général des cartes} de la page~41 est démontré : un isomorphisme de squelettes décomposés vient d'un isomorphisme de cartes si et seulement s'il respecte les chemins de trois arêtes consécutives d'une face (\texttt{lift\_iff}) ; la pleine fidélité revient donc à lire ces chemins sur le squelette. En homologie modulo~$2$, $\chi = 1$ donne $\dim Z_1/B_1 \leqslant 1$, la relation $c_2 = c(K)$ de la page~42 (\texttt{finrank\_Z1\_le}) ; une pseudo-droite est un cycle qui ne borde pas (\texttt{lineChain\_not\_mem}), et une pseudo-droite coupe le bord d'une réunion de faces en un nombre pair de points (\texttt{parity}). D'où la condition~(A5) de la page~50 : si une quatrième pseudo-droite $\Delta$ évite les trois sommets d'un triangle, un cycle triangulaire borde si et seulement si $\Delta$ en coupe un nombre pair de côtés (\texttt{triangle\_iff}) ; l'orientation canonique du triangle se lit donc sur le squelette et ne dépend pas de~$\Delta$. Les segments d'une pseudo-droite se lisent sur le squelette (\texttt{seg\_unique}), et tout isomorphisme de squelettes décomposés respecte cette orientation (\texttt{SkelIso.triangle\_map}). Le théorème de la page~54 est démontré pour les arrangements simples (\texttt{full\_simple}) : le triangle découpé par un chemin de face borde (\texttt{path\_bounds}, par un comptage de parité le long de la droite de l'arête médiane), les coins en un sommet de deux droites se lisent sur le squelette (\texttt{corner2}), et tout isomorphisme de squelettes décomposés se relève. Restent les points multiples ((A1)--(A3) en un sommet d'au moins trois droites), (A6) et le quadrangle complet III$_6$. La condition (A4) est démontrée en des sommets de multiplicité quelconque : deux arêtes quittant les extrémités d'une arête du même côté découpent un triangle qui borde, et de côtés opposés un triangle qui ne borde pas (\texttt{side\_bounds}, \texttt{side\_not}) ; le côté se lit donc sur le squelette dès qu'une quatrième droite évite le triangle. Restent (A1)--(A3) aux points multiples (l'ordre cyclique déduit des côtés), (A6) et le quadrangle complet III$_6$. Le théorème de la page~54 est démontré, points multiples compris, dès que tout triangle a une quatrième droite évitant ses sommets (\texttt{full\_of\_fourth'}) : si tout triangle a une quatrième droite évitant ses sommets, tout isomorphisme de squelettes décomposés se relève de façon unique. L'ingrédient est (A1)--(A3) : les côtés d'une arête se lisent par les triangles qui bordent (\texttt{side\_tri}), et deux arêtes en un sommet sont adjacentes si aucune arête n'est entre elles (\texttt{between\_iff}, \texttt{SkelIso.corner\_map}). Restent les arrangements où un triangle a toutes les autres droites par ses sommets, dont le quadrangle complet III$_6$ : c'est (A6). L'hypothèse de quatrième droite découle d'une condition intrinsèque : un triangle ayant un sommet double a toujours une quatrième droite évitant ses sommets (\texttt{fourth\_at}). D'où la pleine fidélité dès que tout triangle a un sommet sur exactement deux droites (\texttt{full\_of\_simpleCorner}). Restent les arrangements ayant un triangle sans quatrième droite : ses trois sommets sont multiples et toutes les autres droites passent par eux. C'est (A6) et le quadrangle complet III$_6$, entre autres. Plus précisément, restent non formalisés les conditions (A1) à (A4), qui lisent sur le squelette l'ordre circulaire en un sommet et le transport le long d'une arête, et les cas~(A6) et $\mathrm{III}_6$ de l'orientation canonique ; le théorème de la page~54 n'est donc pas démontré en entier. Mathlib n'a pas les arrangements de pseudo-droites ni les cartes. On se reportera aux notes de Grothendieck (\lot{80}{2}{39}).\par} {\small Le cas restant se démontre par un autre chemin, celui des chirotopes (\texttt{Folder80Signs.lean}). Un chirotope attribue un signe à chaque triple de pseudo-droites sans point commun : il dit dans quel sens tourne le triangle qu'elles forment. Un isomorphisme de squelettes décomposés conserve, le long de chaque pseudo-droite, l'ordre circulaire de ses sommets au retournement près. En rang~$2$, cela veut dire que les deux chirotopes, restreints aux triples qui contiennent cette pseudo-droite, ne diffèrent que par un signe global et par le retournement de certaines des autres pseudo-droites. Le produit $\psi$ des deux chirotopes, corrigé par ces signes, s'écrit alors en chaque pseudo-droite $i$ sous la forme $\psi(i,j,l) = \delta^i_j\delta^i_l$. Si une quatrième pseudo-droite évite les sommets d'un triangle, les quatre triples formés par ces quatre pseudo-droites ont la même valeur, et leur produit vaut~$1$ : on retrouve (A5) sous une autre forme (\texttt{eq\_zero\_of\_fourth}). Sinon, on coupe le triangle $a, b, c$ en deux le long d'une pseudo-droite $x$ qui passe par $b \cap c$ et par un troisième sommet de~$a$. Les triangles $a, b, x$ et $a, x, c$ ont chacun une quatrième pseudo-droite, qui passe par $a \cap c$ pour le premier et par $a \cap b$ pour le second (\texttt{eq\_zero}). Dans le quadrangle complet, les trois pseudo-droites auxiliaires sont les côtés qui passent par le quatrième point. Les deux chirotopes diffèrent donc d'une réorientation (\texttt{reorientation\_of\_locallyEquivalent}), et le théorème de Folkman et Lawrence fournit l'homéomorphisme. Le pas de rang~$2$ est démontré lui aussi. Le long d'une pseudo-droite, les autres se rangent en classes, une par sommet, et la somme des signes sur un cycle de quatre arêtes dit si deux sommets en séparent deux autres. Une fonction de signes dont toutes ces sommes s'annulent, sur un graphe multiparti complet d'au moins trois parts, est une constante plus une coupure (\texttt{const\_add\_cut}). Deux chirotopes qui ont les mêmes relations de séparation le long de chaque pseudo-droite diffèrent donc d'une réorientation (\texttt{reorientation\_of\_sameSeparation}). Le théorème de Folkman et Lawrence n'est pas formalisé, et l'argument, qui est celui de l'édition, n'a pas été relu par un spécialiste.\par} \section[Cote 82 : $\mathfrak{sl}(2)$ et la conique en caractéristique 2, cas déployé]{Cote 82 : $\mathfrak{sl}(2)$ et la conique en caractéristique 2, cas déployé\protect\verifie{Folder82}}\label{sec:82} La cote 82, \emph{SO(3) $\simeq$ GP(1)}, notes que l'inventaire date \q{[vers 1982]}, compare les formes de $\mathrm{SO}(3)$ et de $\mathrm{PGL}(2)$ sur une base quelconque. Aux pages~77 et~78, sur une base où $2 = 0$, elle prend le module $\tilde{\mathfrak g}$ des matrices $2 \times 2$ de trace nulle avec $\varphi(u, v) = \mathrm{Tr}(uv)$ : comme $\mathrm{Tr}\,1 = 2 = 0$, $\mathcal O_S \cdot 1 \subset \tilde{\mathfrak g}$ est le noyau de $\varphi$ (58). Le morphisme (59), qui envoie un sous-groupe de Borel, c'est-à-dire une droite isotrope $L \subset \tilde{\mathfrak g}$, sur son orthogonal, se factorise par $\mathbf P(\tilde{\mathfrak g}/\mathcal O_S)$ (60), et la page affirme que (60) est le Frobenius relatif, non un monomorphisme (\lot{82}{4}{77}). L'édition le vérifie dans le cas déployé, sur tout anneau commutatif $R$ où $2 = 0$, dans les coordonnées $u = x\tilde X + y\tilde Y + z\tilde H$, $\tilde X = E_{12}$, $\tilde Y = E_{21}$, $\tilde H = \mathrm{diag}(1, -1)$, pour lesquelles $u^2 = (xy + z^2) \cdot 1$. Aux pages~26 et~27, sur une base où $2 = 0$, une forme de $\mathfrak{sl}(2)$ équivaut à un couple $(V, E)$, $V$ de rang~$2$ et $E$ une extension de $V$ par $\det V$ ; le groupe des automorphismes d'une forme est un groupe affine \q{lisse de dim rel.~6}, celui d'un plan affine symplectique $\mathrm{SL}(V) \ltimes V$, \q{lisse de dim~5}. La lecture identifie $\mathfrak{sl}(2)$ à l'algèbre de Heisenberg : son centre $\mathcal O \tilde H$ est son algèbre dérivée et le crochet induit $\Lambda^2 V \simeq \mathcal O \tilde H$. \begin{theoreme}[D'après les pages 26 et 27, cas déployé\piste{82-char2-sl2-forms-affine}] Soit $R$ un anneau commutatif où $2 = 0$. Dans $\mathfrak{sl}_2(R)$, $[u, u'] = (xy' - yx')\tilde H$ pour $u = x\tilde X + y\tilde Y + z\tilde H$, et le centre $R\tilde H$ est fait de crochets. Tout endomorphisme d'algèbres de Lie de $\mathfrak{sl}_2(R)$ s'écrit de façon unique $u \mapsto g(x, y) + (ax + by + \det g \cdot z)\tilde H$, avec $g \in M_2(R)$ et $a, b \in R$, la composition étant celle de $\mathrm{GL}(V) \ltimes \operatorname{Hom}(V, \det V)$ ; c'est un automorphisme si et seulement si $\det g$ est inversible. Ainsi $\operatorname{Aut}(\mathfrak{sl}_2)(R) \simeq \mathrm{GL}_2(R) \ltimes R^2$, et les automorphismes qui fixent $\tilde H$ forment $\mathrm{SL}_2(R) \ltimes R^2$. Les dérivations forment un $R$-module libre de rang~$6$, celles qui annulent $\tilde H$ un module libre de rang~$5$. \end{theoreme} \noindent L'énoncé tient : voir \texttt{bijective\_iff}, \texttt{bijective\_fix\_iff}, \texttt{autFun\_comp}, \texttt{finrank\_der} et \texttt{finrank\_derFix} dans \href{\leanblob/Folder82.lean}{\texttt{Folder82.\allowbreak{}lean}}. Les dimensions $6$ et $5$ de la page sont celles des algèbres de Lie. Ne sont pas démontrés : les formes sur une base, $\mathfrak{gp}(1)$ et le couplage, le caractère lisse des schémas d'automorphismes. \begin{theoreme}[D'après les pages 77 et 78, cas déployé\piste{82-char2-conic-frobenius}]\label{thm:82-frobenius} Soit $R$ un anneau commutatif où $2 = 0$. Alors $\tilde H = 1$ et le noyau de $\varphi$ sur $\tilde{\mathfrak g}$ est $R \cdot 1$. Pour $s, t \in R$, l'élément $s^2\tilde X + t^2\tilde Y + st\tilde H$ est de carré nul, et son orthogonal pour $\varphi$ est l'hyperplan $t^2 x + s^2 y = 0$, qui contient $1$ et ne dépend que de $(s^2 : t^2)$ : (60) est $(s : t) \mapsto (s^2 : t^2)$. Sur $R = \mathbf F_2[\varepsilon]/(\varepsilon^2)$, les points distincts $(1 : \varepsilon)$ et $(1 : 0)$ de $\mathbf P^1(R)$ ont le même orthogonal : (60) n'est pas un monomorphisme. \end{theoreme} \noindent L'énoncé tient tel que la note de la lecture le donne (\texttt{ker\_phi}, \texttt{orth\_iff}, \texttt{orth\_smul}, \texttt{not\_mono}, dans \href{\leanblob/Folder82.lean}{\texttt{Folder82.\allowbreak{}lean}}). Le calcul de l'orthogonal vaut pour tous $s$, $t$, sans hypothèse d'unimodularité. \begin{encadre} \begin{theoreme*}[Grothendieck, page 78, (61)]\nonverifie Pour une algèbre de quaternions sur une base de caractéristique~$2$, il existe un isomorphisme canonique $\mathbf P(\tilde{\mathfrak g}/\mathcal O_S) \simeq X^{(2)}$, et (60) est le Frobenius relatif $X \to X^{(2)}$ : il est fini, plat de rang~$2$ et radiciel. \end{theoreme*} \end{encadre} {\small La page~78 l'affirme sans démonstration. Sur un corps, la projection depuis le noyau de la conique est classique ; la forme relative et canonique ne l'est pas. Mathlib n'a pas les coniques sur une base ni le Frobenius relatif des schémas. On se reportera aux notes de Grothendieck (\lot{82}{4}{77}).\par} \section[Cote 84 : le produit des algèbres quadratiques, en coordonnées]{Cote 84 : le produit des algèbres quadratiques, en coordonnées\protect\verifie{Folder84}}\label{sec:84} La cote 84, \emph{[Formes quadratiques] : notes manuscrites (s.d.)}, cent quatre-vingt-douze pages que l'inventaire date \q{[à partir de 1982-vers 1986]}, étudie les formes quadratiques binaires et les algèbres quadratiques au-dessus d'une base quelconque, sans diviser par~$2$. Sa deuxième partie construit le produit $A_1 * A_2$ de deux algèbres quadratiques. La page~47 encadre $T_0^2 \equiv \delta \pmod 4$ ; la page~48 énonce, quand $2$ est régulier, l'équivalence entre revêtements quadratiques et triplets $(L, \delta, T_0)$ (\lot{84}{3}{47}, \lot{84}{3}{48}). La page~63 pose \q{sauf erreur} $b = b_1b_2$ et en tire $c$ par $4c = b^2 - \delta$ ; l'encadré écrit \q{$4c_1c_1$}, le membre de droite et le calcul donnent $4c_1c_2$ (\lot{84}{4}{63}). La page~64 vérifie par une identité polynomiale que l'élément $u_1b_2 + u_2b_1 + 2u_1u_2$ annule l'équation du produit quand $u_1$ et $u_2$ annulent les leurs (\lot{84}{4}{64}). Page~84, elle calcule des générateurs de $\operatorname{Im}(\sigma_1 \otimes \sigma_2 - \mathrm{id})$ ; page~85, elle énonce la proposition sur les coinvariants, avec un décompte de rangs au-dessus de $X_0 = V(2)$ ; page~86, le corollaire sur les invariants, \q{et inversement si on sait que ceci reste vrai après toute changement de base} (\lot{84}{5}{84}, \lot{84}{5}{85}, \lot{84}{5}{86}). Page~89, le théorème donne $b = b_1b_2$, $c = c_1b_2^2 + c_2b_1^2 - 4c_1c_2$ et $\delta = \delta_1\delta_2$ (\lot{84}{5}{89}) ; page~102, l'image $i(\mathcal U) = 2U_1U_2 + b_1U_2 + b_2U_1$ du générateur dans $A_1 \otimes A_2$ (\lot{84}{6}{102}). Pages~65 à~79, elle introduit les extensions $\chi$-trivialisées et leur produit ; page~78, le cas scindé donne $b = b_1 \otimes b_2$, et une note marginale de la page~79, oblique et en partie illisible, donne le critère d'inversibilité (\lot{84}{4}{78}, \lot{84}{4}{79}). Pages~125 à~131, elle refait le produit en coordonnées pour un quotient $M$ quelconque et commence la relation de cocycle sans l'achever ; page~169, elle met en place les produits poussé et tiré (\lot{84}{7}{125}, \lot{84}{7}{129}, \lot{84}{7}{131}, \lot{84}{9}{169}). \noindent\emph{Algèbres quadratiques libres.} Pour $b, c \in R$, on note $A(b, c) = R[U]/(U^2 + bU + c)$, de base $(1, U)$, et $\delta(b, c) = b^2 - 4c$. Le changement de variable $V = \varepsilon U + t$, $\varepsilon \in R^\times$, $t \in R$, envoie l'équation de $U$ sur celle de $V$ avec \[ (b', c') = (\varepsilon b - 2t,\ \varepsilon^2c - \varepsilon bt + t^2). \] Dans le cas libre, $L = A/R$ est engendré par l'image de $U$, $T_0$ est la réduction de la trace $-b$ modulo~$2$, donc $T_0 \equiv b$ modulo~$2$, et changer de base de $L$ revient à multiplier par $\varepsilon$. Le triplet $(L, \delta, T_0)$ de la page~48 devient, à isomorphisme près, la classe de $(\delta, b \bmod 2)$ sous $(\delta, b) \mapsto (\varepsilon^2\delta, \varepsilon b)$. \begin{enonce}[Pages 47 à 53, \emph{le théorème des triplets, cas libre}\pisteresolue{84-two-regular-triplet-classification}] Soit $R$ un anneau commutatif. \begin{enumerate} \item Les $R$-algèbres $A(b, c)$ et $A(b', c')$ sont isomorphes si et seulement si $(b', c')$ se déduit de $(b, c)$ par un changement de variable $V = \varepsilon U + t$. \item (Page~47) Pour tous $b, c$, $b^2 - \delta(b, c) = 4c$. Si $\tau^2 - \delta \in 4R$, alors $(\tau + 2a)^2 - \delta \in 4R$ pour tout $a$. Si $\tau^2 - \delta \in 4R$, il existe $c$ avec $\delta(\tau, c) = \delta$. \item (Page~48) Supposons que $2$ ne divise pas zéro dans $R$. Alors $A(b, c) \simeq A(b', c')$ si et seulement s'il existe $\varepsilon \in R^\times$ avec $\delta(b', c') = \varepsilon^2\delta(b, c)$ et $b' \equiv \varepsilon b$ modulo $2R$. Avec $\varepsilon = 1$ (la base de $L$ fixée), il existe une translation $V = U + t$ de $(b, c)$ sur $(b', c')$ si et seulement si $\delta(b', c') = \delta(b, c)$ et $b' \equiv b$ modulo $2R$, et cette translation est unique. \item (Page~53, sur $\mathbb Z$) Un entier $\delta$ est de la forme $b^2 - 4c$ si et seulement si $\delta \equiv 0$ ou $1$ modulo~$4$, et $A(b, c) \simeq A(b', c')$ si et seulement si $\delta(b, c) = \delta(b', c')$. \item Sur $\mathbb F_2$, $(1, 0)$ et $(1, 1)$ ont le même $\delta = 1$ et le même $b$, et $A(1, 0) = \mathbb F_2[U]/(U^2 + U)$ n'est pas isomorphe à $A(1, 1) = \mathbb F_2[U]/(U^2 + U + 1)$. \end{enumerate} \end{enonce} \begin{proof} (1) Tout élément de $A(b, c)$ s'écrit $a + eU$, et $a + eU = 0$ entraîne $a = e = 0$ : le polynôme unitaire $U^2 + bU + c$ de degré~$2$ ne divise aucun polynôme non nul de degré au plus~$1$, et le reste de la division par lui donne l'écriture. Si $V = \varepsilon U + t$ convient, $\varepsilon U + t$ annule $V^2 + b'V + c'$ dans $A(b, c)$ : le calcul donne $\varepsilon^2(U^2 + bU + c)$. On obtient un morphisme $A(b', c') \to A(b, c)$, $V \mapsto \varepsilon U + t$ ; le changement inverse $U = \varepsilon^{-1}V - \varepsilon^{-1}t$ donne le morphisme réciproque, et les deux composés fixent les générateurs. Réciproquement, soit $\varphi : A(b, c) \to A(b', c')$ un isomorphisme. Écrivons $\varphi^{-1}(V) = t + \varepsilon U$ et $\varphi(U) = s + \eta V$. Alors $U = \varphi^{-1}(\varphi(U)) = (s + \eta t) + \eta\varepsilon U$, donc $\eta\varepsilon = 1$ et $\varepsilon$ est inversible. L'image par $\varphi^{-1}$ de l'équation de $V$, où l'on remplace $U^2$ par $-bU - c$, donne \[ (t^2 + b't + c' - \varepsilon^2c) + (2t\varepsilon + b'\varepsilon - \varepsilon^2b)\,U = 0, \] d'où $b' = \varepsilon b - 2t$ après multiplication par $\eta$, puis $c' = \varepsilon^2c - \varepsilon bt + t^2$. (2) Ce sont des identités : $(\tau + 2a)^2 - \tau^2 = 4(a\tau + a^2)$, et si $\tau^2 - \delta = 4k$, on prend $c = k$. (3) Un changement de variable donne $\delta(b', c') = \varepsilon^2\delta(b, c)$ en développant, et $b' = \varepsilon b + 2(-t)$ ; cela vaut sur tout anneau. Réciproquement, si $b' = \varepsilon b + 2s$ et $\delta(b', c') = \varepsilon^2\delta(b, c)$, posons $t = -s$. Alors $b' = \varepsilon b - 2t$, et l'égalité des discriminants s'écrit $4c' = 4(\varepsilon^2c - \varepsilon bt + t^2)$. Comme $2$ est régulier, $4$ l'est, et $c' = \varepsilon^2c - \varepsilon bt + t^2$. Le cas $\varepsilon = 1$ est le même calcul ; deux translations $t$, $t'$ vérifient $2t = 2t'$, donc $t = t'$. (4) Si $b$ est pair, $b^2 - 4c \equiv 0$ ; s'il est impair, $b^2 - 4c \equiv 1$ modulo~$4$. Inversement $\delta = 0^2 - 4(-\delta/4)$ ou $\delta = 1^2 - 4\cdot\frac{1 - \delta}{4}$. Les unités de $\mathbb Z$ sont $\pm 1$, donc $\varepsilon^2 = 1$ et l'énoncé~(3) se réduit à $\delta = \delta'$ et $b' \equiv b$ modulo~$2$. Cette congruence découle de $\delta = \delta'$ : $(b' - b)(b' + b) = 4(c' - c)$ est pair, donc l'un des facteurs l'est, et $b' - b$, $b' + b$ ont la même parité. (5) Dans $\mathbb F_2$, la seule unité est $1$ et $t^2 = t$ pour tout $t$ ; un changement de variable envoie donc $(1, c)$ sur $(1, c - t + t^2) = (1, c)$. Par~(1), $A(1, 0) \not\simeq A(1, 1)$. \end{proof} \begin{remarque} Dans le cas libre, la classification des algèbres quadratiques par $(\delta, b \bmod 2)$ quand $2$ est régulier découle de la proposition~3.11 et du théorème~4.3 de Voight (2016) \cite{voight2016}. La vérification porte sur le cas libre du théorème de la page~48 : $L$ trivial, l'algèbre donnée par une base $(1, U)$, et la correspondance sur les classes d'isomorphisme. Le cas $L$ inversible non trivial, sur une base affine, est démontré plus bas, ainsi que la compatibilité aux changements de base et la reconstruction de $E$, $A$, de la trace, de la norme et du produit par divisions (pages~49 à~52) ; l'équivalence de catégories fibrées sur un schéma ne l'est pas. L'énoncé~(1) vaut sur tout anneau et ne demande pas que $2$ soit régulier ; l'hypothèse sert à l'injectivité de $(b, c) \mapsto (\delta, b \bmod 2)$ sur les classes, et l'exemple de $\mathbb F_2$, où $\mathbb F_2 \times \mathbb F_2$ et $\mathbb F_4$ ont les mêmes $\delta$ et $T_0$, montre qu'elle est nécessaire. La surjectivité, (2), vaut sur tout anneau. Sur $\mathbb Z$, on retrouve que les discriminants sont les entiers congrus à $0$ ou $1$ modulo~$4$ et qu'un anneau quadratique est déterminé par son discriminant ; $T_0$ y est déterminé par $\delta$, comme la lecture le dit. \end{remarque} \noindent\emph{Conventions.} $R$ est un anneau commutatif quelconque. Les algèbres $A_i$ ont pour bases $(1, U_i)$ avec $U_i^2 + b_iU_i + c_i = 0$, de sorte que $\mathrm{Tr}(U_i) = -b_i$ et que la conjugaison est $\sigma_i(1) = 1$, $\sigma_i(U_i) = -b_i - U_i$ ; on pose $\delta_i = b_i^2 - 4c_i$. C'est la convention de la lecture (pages~98 à~102). Du côté des extensions, $E_i$ a pour base $(e_i, x_i)$, où $e_i$ engendre $L_i$ et $x_i$ est le scindage ; $\psi(e_i) = 0$, $\psi(x_i) = 1$, $T_i = 2x_i - b_ie_i$ et $\sigma_i(x) = \psi(x)T_i - x$, donc $\sigma_i(e_i) = -e_i$ et $\sigma_i(x_i) = x_i - b_ie_i$ (page~84). On écrit $E_1 \otimes E_2 = R^4$ dans la base $(e_1 \otimes e_2, e_1 \otimes x_2, x_1 \otimes e_2, x_1 \otimes x_2)$, $\sigma_1 \otimes \sigma_2$ par le produit de Kronecker des deux matrices, et $E_1 * E_2 = R^2$ dans la base $(e_1 \otimes e_2, x_1 * x_2)$. L'application $E_1 \otimes E_2 \to E_1 * E_2$ est celle de la page~63, $(x_1 + u_1) * (x_2 + u_2) = x_1 * x_2 + u_1b_2 + u_2b_1 + 2u_1u_2$ : elle envoie $(a, a', a'', a''')$ sur $(2a + b_2a' + b_1a'',\ a''')$. Du côté des algèbres, $A = A_1 * A_2$ a pour base $(1, \mathcal U)$, $A_1 \otimes A_2$ la base $(1, U_1, U_2, U_1U_2)$, et $i$ envoie $(\lambda, \mu)$ sur $(\lambda, \mu b_2, \mu b_1, 2\mu)$. \begin{enonce}[Pages 63, 64, 89 et 102, \emph{la formule du produit}\pisteresolue{84-product-quadratic-algebras-formula}] Soient $A_1$, $A_2$ deux $R$-algèbres commutatives et $u_i \in A_i$ avec $u_i^2 + b_iu_i + c_i = 0$, $b_i, c_i \in R$. Posons $U_1 = u_1 \otimes 1$, $U_2 = 1 \otimes u_2$ dans $A_1 \otimes_R A_2$, $b = b_1b_2$ et $c = c_1b_2^2 + c_2b_1^2 - 4c_1c_2$. \begin{enumerate} \item (Page~64) Dans tout anneau commutatif, avec $Q_i = u_i^2 + b_iu_i + c_i$ et $u = 2u_1u_2 + b_1u_2 + b_2u_1$, \[ u^2 + bu + c = b_2^2Q_1 + b_1^2Q_2 + 4\bigl(Q_1Q_2 - c_1Q_2 - c_2Q_1\bigr). \] \item (Page~102) L'élément $\mathcal U = 2U_1U_2 + b_1U_2 + b_2U_1$ vérifie $\mathcal U^2 + b\,\mathcal U + c = 0$ dans $A_1 \otimes_R A_2$ ; il existe donc un unique morphisme de $R$-algèbres $R[\mathcal U]/(\mathcal U^2 + b\,\mathcal U + c) \to A_1 \otimes_R A_2$ envoyant $\mathcal U$ sur cet élément. \item (Pages~63 et~89) $b^2 - 4c = \delta_1\delta_2$, et $c_1\delta_2 + c_2\delta_1 + 4c_1c_2 = c_1b_2^2 + c_2b_1^2 - 4c_1c_2$. \end{enumerate} \end{enonce} \begin{proof} (1) et (3) sont des identités entre polynômes à coefficients entiers ; on les vérifie en développant. (2) Les inclusions $A_1 \to A_1 \otimes A_2$ et $A_2 \to A_1 \otimes A_2$ sont des morphismes de $R$-algèbres ; elles transportent les équations de $u_1$ et $u_2$ en $U_1^2 + b_1U_1 + c_1 = 0$ et $U_2^2 + b_2U_2 + c_2 = 0$. L'identité~(1), appliquée dans l'anneau $A_1 \otimes A_2$ à $U_1$ et $U_2$, donne $\mathcal U^2 + b\,\mathcal U + c = 0$, puisque $Q_1 = Q_2 = 0$. La propriété universelle de $R[\mathcal U]/(\mathcal U^2 + b\,\mathcal U + c)$ donne le morphisme. \end{proof} \begin{remarque} La formule du produit est publiée par Voight (2016, construction~3.12 et théorème~3.24) \cite{voight2016}, qui l'attribue à A.~Hahn (1994), le monoïde général à O.~Loos (1996), et son existence à une lettre de P.~Deligne à M.~Rost et à M.~Bhargava (2005). L'identité de la page~64 vaut sans hypothèse sur $u_1$, $u_2$, dans tout anneau commutatif, et la vérification ne divise jamais par~$2$ : le produit est défini sur $\mathbb Z$. La lecture de \q{$4c_1c_1$} en $4c_1c_2$ est confirmée : avec $4c_1c_2$, l'identité~(1) et la relation $b^2 - 4c = \delta_1\delta_2$ tiennent, et la première forme de l'encadré est égale à la seconde. Seule la partie en coordonnées de la piste est démontrée ; la construction intrinsèque de $X_1 * X_2$ et l'unicité de la forme quadratique de la page~89 ne le sont pas. \end{remarque} \begin{encadre} \begin{theoreme}[Grothendieck, pages 84 et 85, \emph{proposition}\piste{84-product-coinvariants-one-etale}] Dans les coordonnées ci-dessus, l'application induite \[ (E_1 \otimes E_2)/\operatorname{Im}(\sigma_1 \otimes \sigma_2 - \mathrm{id}) \to E_1 * E_2 \] est bien définie, et elle est bijective si et seulement si $2R + b_1R + b_2R = R$. \end{theoreme} \end{encadre} \begin{proof} On calcule $\sigma_1 \otimes \sigma_2 - \mathrm{id}$ sur la base : $e_1 \otimes e_2 \mapsto 0$, $e_1 \otimes x_2 \mapsto (b_2, -2, 0, 0)$, $x_1 \otimes e_2 \mapsto (b_1, 0, -2, 0)$, $x_1 \otimes x_2 \mapsto (b_1b_2, -b_1, -b_2, 0)$ ; ce sont les générateurs de la page~84. L'application $(a, a', a'', a''') \mapsto (2a + b_2a' + b_1a'', a''')$ les annule, d'où l'application induite. Elle a même image que $E_1 \otimes E_2 \to E_1 * E_2$. Si elle est surjective, $(1, 0)$ est atteint, donc $2a + b_2a' + b_1a'' = 1$ pour des $a, a', a'' \in R$, et $2R + b_1R + b_2R = R$. Réciproquement, si $2g_0 + b_1g_1 + b_2g_2 = 1$, l'image de $(y_0g_0, y_0g_2, y_0g_1, y_1)$ est $(y_0, y_1)$. Sous la condition, montrons que le noyau est dans $\operatorname{Im}(\sigma_1 \otimes \sigma_2 - \mathrm{id})$ ; l'injectivité de l'application induite en résulte. Écrivons $f = (2, b_2, b_1)$ et $g = (g_0, g_2, g_1)$, de sorte que $f \cdot g = 1$. Un élément du noyau est $(a_0, a_1, a_2, 0)$ avec $f \cdot a = 0$. Les relations de Koszul $\kappa_{jk} = f_k\varepsilon_j - f_j\varepsilon_k$ de $f$ dans $R^3$ sont $\kappa_{01} = (b_2, -2, 0)$, $\kappa_{02} = (b_1, 0, -2)$ et $\kappa_{12} = (0, b_1, -b_2)$ ; les deux premières sont les images de $e_1 \otimes x_2$ et $x_1 \otimes e_2$, la troisième celle de $x_1 \otimes x_2 - b_1\, e_1 \otimes x_2$. Or \[ a = \sum_{j < k} (g_ka_j - g_ja_k)\,\kappa_{jk}, \] car la $i$-ème coordonnée du second membre est $a_i (f \cdot g) - g_i (f \cdot a) = a_i$. L'élément $a$ est donc l'image d'une combinaison explicite des vecteurs de base. \end{proof} \begin{enonce}[Page 86, \emph{corollaire}\piste{84-product-coinvariants-one-etale}] Dans les coordonnées ci-dessus, disons que $A \to (A_1 \otimes A_2)^{\sigma_1 \otimes \sigma_2}$ est un isomorphisme si $i$ est injectif et si son image est le sous-module des invariants de $\sigma_1 \otimes \sigma_2$. \begin{enumerate} \item Si $2R + b_1R + b_2R = R$, c'est un isomorphisme. \item C'est un isomorphisme après tout changement de base $R \to S$ si et seulement si $2R + b_1R + b_2R = R$. \item Sur $R = \mathbb Z[X]$, avec $b_1 = X$ et $b_2 = 0$, c'est un isomorphisme, alors que $2$, $X$ et $0$ engendrent un idéal propre. \end{enumerate} \end{enonce} \begin{proof} Un vecteur $(p, q, r, s)$ (coefficients de $1$, $U_1$, $U_2$, $U_1U_2$) est invariant si et seulement si $-b_1q - b_2r + b_1b_2s = 0$, $2q = b_2s$ et $2r = b_1s$. L'image $(\lambda, \mu b_2, \mu b_1, 2\mu)$ de $i$ vérifie ces relations. (1) Soit $2g_0 + b_1g_1 + b_2g_2 = 1$. Si $i(\lambda, \mu) = 0$, alors $\lambda = 0$ et $\mu = \mu(2g_0 + b_1g_1 + b_2g_2) = 0$. Soit $(p, q, r, s)$ invariant. Des relations on tire $b_1q = b_2r$, car $b_1b_2s = 2b_1q$ (on multiplie $2q = b_2s$ par $b_1$). Posons $\mu = sg_0 + rg_1 + qg_2$. Alors $2\mu = s$, $b_1\mu = r$ et $b_2\mu = q$ ; par exemple $b_2\mu - q = g_0(b_2s - 2q) + g_1(b_2r - b_1q) = 0$, en remplaçant $q$ par $q(2g_0 + b_1g_1 + b_2g_2)$. Donc $(p, q, r, s) = i(p, \mu)$. (2) La condition passe à tout $S$ : l'image de $1 = 2g_0 + b_1g_1 + b_2g_2$ est une relation du même type, et (1) s'applique. Réciproquement, si l'idéal $I = (2, b_1, b_2)$ n'est pas $R$, prenons $S = R/I$, qui n'est pas nul. Dans $S$, $2 = b_1 = b_2 = 0$, et le vecteur $U_2 = (0, 0, 1, 0)$ est invariant. S'il était $i(\lambda, \mu)$, sa coordonnée sur $U_2$ serait $\mu b_1 = 0$, et l'on aurait $1 = 0$ dans $S$. (3) Avec $b_1 = X$, $b_2 = 0$, les relations deviennent $2q = 0$, $2r = Xs$. L'anneau $\mathbb Z[X]$ est intègre, donc $q = 0$ et $i$ est injectif ($2\mu = 0$ entraîne $\mu = 0$). L'élément $2$ est premier dans $\mathbb Z[X]$ et ne divise pas $X$ ; de $2 \mid Xs$ on tire $s = 2\mu$, puis $r = X\mu$ en simplifiant par~$2$, et $(p, q, r, s) = i(p, \mu)$. Enfin, si $2g_0 + Xg_1 = 1$, le coefficient constant donne $2\,g_0(0) = 1$ dans $\mathbb Z$, ce qui est impossible. \end{proof} \begin{remarque} La proposition de la page~85 tient en coordonnées sur tout anneau commutatif, dans les deux sens, sans changement de base, sans hypothèse de rang et sans la réduction au cas $2 = 0$ que la page annonce. Le noyau est engendré par les relations de Koszul de la suite unimodulaire $(2, b_2, b_1)$. Lorsque les deux algèbres sont séparables, l'identification du produit aux invariants de $\sigma_1 \otimes \sigma_2$ est énoncée par Voight (théorème~3.24\,(iii)) \cite{voight2016} ; voir aussi Kanzaki et C.~Small (1972), qu'il cite. Pour le corollaire de la page~86, la condition suffit sur $R$ lui-même, et la réciproque demande l'hypothèse de la page, \q{après toute changement de base} : l'exemple de $\mathbb Z[X]$ montre que l'isomorphisme sur $R$ seul n'entraîne pas la condition. Un changement de base vers $R/(2, b_1, b_2)$ suffit. La formulation ponctuelle (en tout point de $V(2)$, l'un des $T_{i,0}$ engendre $L_{i,0}$) n'est pas démontrée ; elle équivaut à la condition en coordonnées dès que $L_1$, $L_2$ sont triviaux et munis de scindages, comme la page le dit aussi. Le passage de l'énoncé sur les coinvariants à l'énoncé sur les invariants par dualité n'est pas formalisé : les deux sont démontrés séparément, en coordonnées. \end{remarque} \noindent\emph{Extensions $\chi$-scindées en coordonnées.} Soit $\chi \in R$. On prend une extension scindée $0 \to L \to M \oplus L \to M \to 0$, $\alpha(\xi) = (0, \xi)$, $\psi(\eta, \xi) = \eta$, de $R$-modules quelconques. Un $\chi$-scindage est un couple $(\pi, \varpi)$, $\pi : M \oplus L \to L$, $\varpi : M \to M \oplus L$, avec $\pi\alpha = \chi$, $\psi\varpi = \chi$ et $\alpha\pi + \varpi\psi = \chi$ (page~169). Pour $b : M \to L$, on pose $\pi_b(\eta, \xi) = b(\eta) + \chi\xi$ et $\varpi_b(\eta) = (\chi\eta, -b(\eta))$. La transvection $T_w$, pour $w : M \to L$, est $(\eta, \xi) \mapsto (\eta, \xi + w(\eta))$. Le produit de deux objets $b_1 : M_1 \to L_1$ et $b_2 : M_2 \to L_2$ est $b_1 \otimes b_2 : M_1 \otimes M_2 \to L_1 \otimes L_2$ (page~78, \q{Il n'y a pas plus simple !}, et page~129). Pour $M = L = R$, un objet est un scalaire $b$, et l'objet unité est $b = 1$, $\pi(u, \lambda) = \lambda + \chi u$ (page~78). \begin{enonce}[Pages 77--79 et 123--131, extensions $\chi$-scindées\piste{84-chi-trivialised-extension-product}] \begin{enumerate} \item Le couple $(\pi_b, \varpi_b)$ est un $\chi$-scindage. Réciproquement, tout $\chi$-scindage $(\pi, \varpi)$ de $M \oplus L$ est de cette forme, avec $b = \pi|_M$. \item Il existe un endomorphisme $f$ de $M \oplus L$ induisant l'identité sur $L$ et sur $M$ et tel que $\pi_{b'} \circ f = \pi_b$ si et seulement si $b = b' + \chi w$ pour un $w : M \to L$ ; c'est alors $T_w$. On a aussi $T_w \circ \varpi_b = \varpi_{b'}$ et $T_w \circ T_{w'} = T_{w + w'}$. \item (Page~129) Pour $u_i : M_i \to L_i$, $(b_1 + \chi u_1) \otimes (b_2 + \chi u_2) = b_1 \otimes b_2 + \chi u$ avec $u = b_1 \otimes u_2 + u_1 \otimes b_2 + \chi\, u_1 \otimes u_2$. \item (Page~131) Si l'on change d'abord par $u_i$, puis par $u'_i$ en partant de $b'_i = b_i + \chi u_i$, la somme des deux données est celle du changement par $u_i + u'_i$ : $u'' = u + u'$. \item (Page~78) Le produit est associatif, commutatif et unitaire : à travers les isomorphismes d'associativité et de commutativité des produits tensoriels, $(b_1 \otimes b_2) \otimes b_3$ correspond à $b_1 \otimes (b_2 \otimes b_3)$ et $b_1 \otimes b_2$ à $b_2 \otimes b_1$ ; à travers $R \otimes M \simeq M$ et $R \otimes L \simeq L$, $\mathrm{id}_R \otimes b$ correspond à $b$. \item (Page~79) Pour $M = L = R$, disons $b \sim b'$ s'il existe $\varepsilon \in R^\times$ et $w \in R$ avec $\varepsilon b = b' + \chi w$ (un isomorphisme qui agit par $\varepsilon$ sur $L$). La relation est compatible au produit, et la classe de $b$ est inversible, c'est-à-dire $bb' \sim 1$ pour un $b'$, si et seulement si $bR + \chi R = R$, si et seulement si $b$ est inversible dans $R/\chi R$ : la section $T_0 = -b_0$ engendre $L_0$ sur $V(\chi)$. \end{enumerate} \end{enonce} \begin{proof} (1) Les trois relations se vérifient sur $(\eta, 0)$ et $(0, \xi)$ ; par exemple $\alpha\pi_b(\eta, \xi) + \varpi_b(\eta) = (0, b\eta + \chi\xi) + (\chi\eta, -b\eta) = \chi(\eta, \xi)$. Si $(\pi, \varpi)$ est un $\chi$-scindage, $\pi(0, \xi) = \chi\xi$ donne $\pi = \pi_b$. La relation $\alpha\pi + \varpi\psi = \chi$ appliquée à $(\eta, 0)$ donne $\varpi(\eta) = \chi(\eta, 0) - (0, b\eta)$, et $\varpi = \varpi_b$. (2) Si $f$ induit l'identité sur $L$ et sur $M$, alors $f(0, \xi) = (0, \xi)$ et la première coordonnée de $f(\eta, 0)$ est $\eta$, donc $f = T_w$ avec $w(\eta)$ la seconde coordonnée de $f(\eta, 0)$. On a $\pi_{b'}(T_w(\eta, \xi)) = b'\eta + \chi\xi + \chi w\eta = \pi_{b' + \chi w}(\eta, \xi)$, d'où la condition $b = b' + \chi w$, en évaluant en $(\eta, 0)$. Inversement $T_w$ convient. Le calcul de $T_w \circ \varpi_b$ et de $T_w \circ T_{w'}$ est direct. (3) et (4) Le produit tensoriel d'applications linéaires est bilinéaire ; on développe. Pour (4), on compare $u + u'$, où $u' = (b_1 + \chi u_1) \otimes u'_2 + u'_1 \otimes (b_2 + \chi u_2) + \chi\, u'_1 \otimes u'_2$, avec $(b_1 \otimes (u_2 + u'_2)) + ((u_1 + u'_1) \otimes b_2) + \chi\,(u_1 + u'_1) \otimes (u_2 + u'_2)$ ; les deux développements ont les mêmes neuf termes. (5) Ce sont la naturalité des isomorphismes d'associativité et de commutativité, qui sont dans mathlib, et un calcul sur les tenseurs purs pour l'unité. (6) Si $\varepsilon_i b_i = b'_i + \chi w_i$, alors $\varepsilon_1\varepsilon_2 b_1b_2 = b'_1b'_2 + \chi(b'_1w_2 + w_1b'_2 + \chi w_1w_2)$. Si $\varepsilon bb' = 1 + \chi w$, alors $b(\varepsilon b') + \chi(-w) = 1$. Si $bg + \chi h = 1$, alors $bg = 1 + \chi(-h)$, et $bg \sim 1$ avec $\varepsilon = 1$. Enfin $bR + \chi R = R$ équivaut à l'existence de $g$ avec $bg \equiv 1$ modulo $\chi R$. \end{proof} \begin{remarque} Seule la partie en coordonnées de la piste est démontrée, pour une extension scindée de modules quelconques, sans diviser par $\chi$ ni par~$2$. Le recollement de ces coordonnées en un produit $E_1 * E_2$ sur une base non affine et la compatibilité des contraintes entre elles (la quatrième compatibilité de la page~177 n'est pas écrite) ne le sont pas ; la construction par somme amalgamée et la propriété universelle des applications bi-affines (pages~68 à~76) sont démontrées sur une base affine à la fin de la section. La relation de cocycle de la page~131, que la page commence sans l'achever, est vraie avec les signes $b'_i = b_i + \chi u_i$. Le critère d'inversibilité de la note marginale de la page~79 est démontré dans le cas $L = M = R$ (pour $L$ quelconque, voir le théorème de la fin de la section) : l'inverse de la classe de $b$ est la classe de $g$ dès que $bg \equiv 1$ modulo~$\chi$, et l'on n'a besoin d'aucune unité $\varepsilon$ autre que $1$ pour le construire. \end{remarque} \begin{enonce}[Pages 125, 127 et 169, \emph{produit poussé et produit tiré}\piste{84-chi-trivialised-extension-product}] En coordonnées, le produit poussé porte le $\chi$-scindage de $b = b_1 \otimes b_2$ et le produit tiré celui de $-b$ (page~125). \begin{enumerate} \item Si $\gamma\chi = 2$, la transvection $T_{\gamma b}$ envoie le $\chi$-scindage $\pi_b$ sur $\pi_{-b}$ : $\pi_{-b} \circ T_{\gamma b} = \pi_b$. \item (Page~125, \q{commute !}) Si $\gamma\chi = 2$, pour un changement de scindage qui remplace $b$ par $b + \chi u$ du côté poussé et $-b$ par $-b - \chi u$ du côté tiré, $T_{\gamma b} \circ T_u = T_{-u} \circ T_{\gamma(b + \chi u)}$. \item Pour les objets unités ($M = L = R$, $b_1 = b_2 = \mathrm{id}$), il existe un endomorphisme de $R \oplus R$ qui induit l'identité sur $L$ et sur $M$ et envoie le scindage poussé sur le scindage tiré si et seulement s'il existe $\gamma$ avec $\gamma\chi = 2$. Sur $\mathbb Z$, avec $\chi = 4$, il n'en existe pas. \end{enumerate} \end{enonce} \begin{proof} (1) Par l'énoncé précédent, $\pi_{-b} \circ T_{\gamma b} = \pi_{-b + \chi\gamma b} = \pi_{-b + 2b} = \pi_b$. (2) Les transvections se composent par addition : il faut $\gamma b + u = -u + \gamma b + \gamma\chi u$, ce qui est $\gamma\chi u = 2u$. (3) Par l'énoncé précédent, un tel endomorphisme existe si et seulement si $\mathrm{id} = -\mathrm{id} + \chi w$ pour un $w : R \to R$ ; en $1$, cela donne $w(1)\chi = 2$, et inversement $w = \gamma\,\mathrm{id}$ convient. Sur $\mathbb Z$, $4\gamma = 2$ n'a pas de solution. \end{proof} \begin{remarque} L'hypothèse $\gamma\chi = 2$, que la lecture prend à la page~127 pour l'isomorphisme de la page~169, est suffisante, et elle est nécessaire dès les objets unités, parmi les isomorphismes qui induisent l'identité sur $L_1 \otimes L_2$ et $M_1 \otimes M_2$ : la comparaison demande que $2$ soit multiple de $\chi$. Le signe $-b$ du produit tiré est pris de la page~125 ; la construction du produit tiré comme produit fibré (page~169) et l'identification de la flèche du milieu du diagramme de la page~167 avec l'opérateur $F_{11}$ ne sont pas formalisées. \end{remarque} Ne sont pas démontrés ici : l'équivalence de catégories fibrées du théorème de la page~48 sur une base non affine et le lien de la page~45 entre algèbres et triplets $(L, P_1, Q)$ pour $L$ non trivial (le cas $L$ inversible sur une base affine, les changements de base et la reconstruction des pages~49 à~52 sont démontrés à la fin de la section), la construction intrinsèque du produit $X_1 * X_2$ et des extensions $\chi$-scindées sur une base non affine (sur une base affine, la somme amalgamée des pages~68 à~70 et la propriété universelle des pages~75 et~76 sont démontrées à la fin de la section), la construction du produit tiré comme produit fibré et l'opérateur $F_{11}$ (pages~141 à~169), l'unicité de la forme quadratique du théorème de la page~89, la formulation ponctuelle de la proposition de la page~85 et du corollaire de la page~86, l'énoncé du corollaire pour $\underline{\mathrm{Hom}}(-, M)$, le passage des coinvariants aux invariants par dualité, la trace et la norme de $A_1 \otimes A_2$ sur $A$ (pages~104 et~105), la quatrième partie du dossier et le reste de la troisième. \noindent\emph{Le cas $L$ inversible, sur une base affine.} Sur $X = \operatorname{Spec} R$, la page~45 décrit un revêtement quadratique par un triplet $(L, P_1, Q)$ : $L$ inversible, $P_1$ un torseur sous $L$ et $Q : P_1 \to L^{\otimes 2}$ une fonction polynôme de degré~$2$ de partie homogène $u \mapsto u^2$. Sur une base affine le torseur est trivial ; le choix d'une origine $x_0$ identifie $P_1$ à $L$ et écrit $Q(x_0 + u) = u \otimes u + b \otimes u + c$, avec $b = 2x_0 - T \in L$ et $c \in L \otimes L$ (\texttt{qform}). Un morphisme $(L, b, c) \to (L', b', c')$ est un isomorphisme $\varphi : L \to L'$ accompagné de l'application de torseurs $x_0 + u \mapsto x'_0 + t + \varphi(u)$, $t \in L'$, qui transporte $Q$ sur $Q'$ : $Q'(t + \varphi u) = (\varphi \otimes \varphi)(Q(u))$ pour tout $u$ (\texttt{IsCoverHom}). Le triplet associé est $(L, \delta, T_0)$ avec $\delta = b \otimes b - 4c$ (\texttt{discL}) et $T_0$ la classe de $b$ dans $L/2L = \Gamma(V(2), L_0)$ ; la condition $T_0^2 \equiv \delta \bmod 4$ dit qu'un relèvement $\tau$ de $T_0$ vérifie $\tau \otimes \tau - \delta \in 4\,(L \otimes L)$ (\texttt{TripletCond}). Un morphisme de triplets est un isomorphisme $\varphi$ avec $(\varphi \otimes \varphi)(\delta) = \delta'$ et $\varphi_0(T_0) = T'_0$, où $\varphi_0 : L/2L \to L'/2L'$ est induit par $\varphi$ (\texttt{mod2}). \begin{encadre} \begin{theoreme}[Grothendieck, pages 45 à 53, classification par triplets, base affine\pisteresolue{84-two-regular-triplet-classification}] Soit $R$ un anneau commutatif, et $L$, $L'$ des $R$-modules inversibles. \begin{enumerate} \item Sur tout $R$, $(\varphi, t)$ est un morphisme si et seulement si $\varphi(b) = b' + 2t$ et $(\varphi \otimes \varphi)(c) = c' + b' \otimes t + t \otimes t$ ; les morphismes forment un groupoïde, d'identité $(\mathrm{id}, 0)$, de composé $(\psi, s) \circ (\varphi, t) = (\psi\varphi, s + \psi t)$ et d'inverse $(\varphi^{-1}, -\varphi^{-1}t)$. \item (Page~47) Sur tout $R$, $(L, \delta, T_0)$ vérifie $T_0^2 \equiv \delta \bmod 4$, et la condition ne dépend pas du relèvement $\tau$ choisi. Un morphisme $(\varphi, t)$ de revêtements est un morphisme de triplets. \item (Page~48) Supposons que $2$ ne divise pas zéro dans $R$. Tout morphisme de triplets $\varphi$ se relève en un unique morphisme $(\varphi, t)$ de revêtements. Tout triplet $(L, \delta, T_0)$ avec $T_0^2 \equiv \delta \bmod 4$ provient d'un revêtement de même $L$, et cela vaut sur tout $R$. Le foncteur $(L, b, c) \mapsto (L, \delta, T_0)$ est donc une équivalence de groupoïdes ; en particulier deux revêtements sont isomorphes si et seulement si leurs triplets le sont. \end{enumerate} \end{theoreme} \end{encadre} \begin{proof} On utilise deux faits sur un module inversible $L$. D'abord $L \otimes L$ est symétrique : $x \otimes y = y \otimes x$ (\texttt{Module.\allowbreak{}Invertible.\allowbreak{}tmul\_comm} de mathlib, par localisation en un idéal maximal, où $L$ devient libre de rang~$1$). C'est ce qui donne un sens au produit $b\,u$ de la page. Ensuite, si $x \otimes w = 0$ pour tout $w \in L$, alors $x = 0$ (\texttt{eq\_zero\_of\_tmul\_eq\_zero}) : on écrit $1 = \sum \gamma_i(w_i)$ avec $\gamma_i \in L^\vee$, ce que permet l'inversibilité, et l'on applique $\mathrm{id} \otimes \gamma_i$ à $x \otimes w_i = 0$, d'où $x = \sum \gamma_i(w_i)\,x = 0$. (1) En $u = 0$, la condition donne $t \otimes t + b' \otimes t + c' = (\varphi \otimes \varphi)(c)$. En $u = \varphi^{-1}(w)$, les termes en $w \otimes w$ et les termes constants se simplifient, et il reste, par symétrie, $(\varphi(b) - b' - 2t) \otimes w = 0$ pour tout $w$, donc $\varphi(b) = b' + 2t$. La réciproque se vérifie en développant. Pour le composé, $s + \psi t + \psi\varphi u = s + \psi(t + \varphi u)$, et $(\psi \otimes \psi)(\varphi \otimes \varphi) = \psi\varphi \otimes \psi\varphi$. Pour l'inverse, on applique la condition à $u = -\varphi^{-1}t + \varphi^{-1}w$ et l'on compose par $\varphi^{-1} \otimes \varphi^{-1}$ (\texttt{isCoverHom\_iff}, \texttt{isCoverHom\_refl}, \texttt{isCoverHom\_trans}, \texttt{isCoverHom\_symm}). (2) Le relèvement $\tau = b$ donne $b \otimes b - \delta = 4c$. Si $\tau' = \tau - 2a$, la symétrie donne $\tau' \otimes \tau' - \tau \otimes \tau = 4(a \otimes a - \tau \otimes a)$. Si $\varphi(b) = b' + 2t$ et $(\varphi \otimes \varphi)(c) = c' + b' \otimes t + t \otimes t$, alors \[ (\varphi \otimes \varphi)(\delta) = (b' + 2t) \otimes (b' + 2t) - 4(c' + b' \otimes t + t \otimes t) = b' \otimes b' - 4c' = \delta', \] et $\varphi(b) - b' = 2t \in 2L'$ (\texttt{tripletCond\_iff\_forall}, \texttt{tripletCond\_discL}, \texttt{isCoverHom\_triplet}). (3) Un module inversible est projectif, donc facteur direct d'un module libre ; si $2$ est régulier dans $R$, il l'est sur tout module libre, donc sur $L'$ et sur $L' \otimes L'$, qui est inversible (\texttt{two\_smul\_injective\_of\_projective}). Soit $\varphi$ un morphisme de triplets. La condition sur $T_0$ donne $t$ avec $\varphi(b) = b' + 2t$. Alors \[ 4\,(\varphi \otimes \varphi)(c) = \varphi(b) \otimes \varphi(b) - \delta' = (b' + 2t) \otimes (b' + 2t) - b' \otimes b' + 4c' = 4\,(c' + b' \otimes t + t \otimes t), \] et l'on simplifie par~$4$ : $(\varphi, t)$ est un morphisme par~(1). Si $(\varphi, t')$ en est un autre, $2t = 2t'$, donc $t = t'$. Enfin, si $\tau$ relève $T_0$ et $\tau \otimes \tau - \delta = 4k$, le revêtement $(L, \tau, k)$ a pour triplet $(L, \delta, T_0)$ ; c'est la formule $c = (\tau^2 - \delta)/4$ de la page, sans division (\texttt{triplet\_full\_faithful}, \texttt{triplet\_ess\_surj}, \texttt{triplet\_classification}, \texttt{cover\_iso\_iff\_triplet\_iso}). \end{proof} \begin{remarque} Le cas $L$ non trivial ne demande rien de plus que le cas libre, une fois les produits $b\,u$ lus dans $L \otimes L$ : la symétrie de $L \otimes L$ remplace la commutativité de $R$, et la projectivité de $L$ et de $L \otimes L$ transporte la régularité de~$2$. Comme dans le cas libre, l'hypothèse sur~$2$ ne sert qu'à la pleine fidélité, et l'exemple de $\mathbb F_2$ montre qu'elle est nécessaire ; la surjectivité essentielle vaut sur tout anneau. Seule la symétrie utilise le rang~$1$ : pour le sens « morphisme de revêtements $\Rightarrow$ morphisme de triplets », il suffit que $L'$ soit inversible. L'énoncé démontré porte sur les triplets $(L, P_1, Q)$ de la page~45, l'origine de $P_1$ choisie, sur une base affine. \end{remarque} \noindent\emph{Changement de base.} Soit $R \to S$ un morphisme d'anneaux commutatifs. Pour un $R$-module $L$, on note $L_S = S \otimes_R L$, $b_S = 1 \otimes b$ pour $b \in L$, et $c \mapsto c_S$ l'application $R$-linéaire $L \otimes_R L \to L_S \otimes_S L_S$, $x \otimes y \mapsto (1 \otimes x) \otimes (1 \otimes y)$ (\texttt{bc2}) ; pour $\varphi : L \simeq L'$, $\varphi_S = \mathrm{id}_S \otimes \varphi$. \begin{enonce}[Pages 45 à 48, \emph{compatibilité aux changements de base}\pisteresolue{84-two-regular-triplet-classification}] Soit $R \to S$ un morphisme d'anneaux commutatifs, $L$, $L'$ des $R$-modules, $L'$ inversible. \begin{enumerate} \item $\delta(b_S, c_S) = \delta(b, c)_S$ ; si $\tau \otimes \tau - \delta \in 4\,(L \otimes L)$ pour un relèvement $\tau$ de $T_0$, alors $\tau_S \otimes \tau_S - \delta_S \in 4\,(L_S \otimes L_S)$ : la condition $T_0^2 \equiv \delta \bmod 4$ passe à $S$. \item Si $(\varphi, t)$ est un morphisme de revêtements $(L, b, c) \to (L', b', c')$, alors $(\varphi_S, t_S)$ est un morphisme $(L_S, b_S, c_S) \to (L'_S, b'_S, c'_S)$. Si $\varphi$ est un morphisme de triplets, $\varphi_S$ en est un. \end{enumerate} Le foncteur $(L, b, c) \mapsto (L, \delta, T_0)$ commute donc aux changements de base, sur les objets et sur les morphismes. \end{enonce} \begin{proof} L'application $c \mapsto c_S$ est bien définie : $(1 \otimes rx) \otimes (1 \otimes y) = r\,(1 \otimes x) \otimes (1 \otimes y)$, le scalaire $r$ agissant sur $L_S \otimes_S L_S$ par son image dans $S$. Par récurrence sur les tenseurs, elle commute à $\varphi \otimes \varphi$ : $((\varphi \otimes \varphi)\,c)_S = (\varphi_S \otimes \varphi_S)(c_S)$. (1) Par linéarité, $(b \otimes b - 4c)_S = b_S \otimes b_S - 4c_S$ ; si $\tau' - \tau = 2a$, alors $\tau'_S - \tau_S = 2a_S$, et $\tau \otimes \tau - \delta = 4k$ donne $\tau_S \otimes \tau_S - \delta_S = 4k_S$. (2) $L'_S$ est inversible sur $S$ (mathlib), et l'on applique le critère en coordonnées du théorème précédent sur $S$ : $\varphi_S(b_S) = (\varphi b)_S = b'_S + 2t_S$ et $(\varphi_S \otimes \varphi_S)(c_S) = ((\varphi \otimes \varphi)c)_S = c'_S + b'_S \otimes t_S + t_S \otimes t_S$. Pour un morphisme de triplets, $(\varphi_S \otimes \varphi_S)(\delta_S) = ((\varphi \otimes \varphi)\delta)_S = \delta'_S$, et $\varphi(\tau) - \tau' = 2a$ donne $\varphi_S(\tau_S) - \tau'_S = 2a_S$ (\texttt{discL\_baseChange}, \texttt{tripletCond\_baseChange}, \texttt{isCoverHom\_baseChange}, \texttt{tripletHom\_baseChange}). \end{proof} \noindent\emph{La reconstruction des pages 49 à 52.} Dans le cas libre, $A = A(b, c)$, $\delta = b^2 - 4c$, et $\mathrm{Tr}$, $N$ sont la trace et la norme de $A$ sur $R$ (celles de mathlib, \texttt{Algebra.\allowbreak{}trace} et \texttt{Algebra.\allowbreak{}norm}). Pour $y = a + eU \in A$, on pose $\beta = \mathrm{Tr}(y)$ et $\gamma = e$, de sorte que $y = (\beta + \gamma z)/2$ avec $z = 2U + b$, $z^2 = \delta$ (\texttt{recon}) ; pour $x \in E = \check A$, on pose $\lambda = \psi(x) = x(1)$ et $\zeta = (2x - \lambda\,\mathrm{Tr})(U) = 2x(U) + \lambda b$, la coordonnée de $2x - \psi(x)T \in L$ (\texttt{eCoord}). La fonction de la page~45, dans le scindage $x_0 = (1, 0)$, est $Q(x) = x(U)^2 + b\,x(1)x(U) + c\,x(1)^2$, c'est-à-dire $Q(x_0 + u) = u^2 + bu + c$ (\texttt{qE}), et $\varphi_N(y) = \mathrm{Tr}(y)\,\mathrm{Tr} - \mathrm{Tr}(y\,\cdot)$ est la forme polaire de la norme (\texttt{phiN}). \begin{encadre} \begin{theoreme}[Grothendieck, pages 46 et 49 à 52, reconstruction de $E$, $A$, de la trace, de la norme et du produit\pisteresolue{84-two-regular-triplet-classification}] Soit $R$ un anneau commutatif et $b, c \in R$. \begin{enumerate} \item $\mathrm{Tr}(a + eU) = 2a - eb$ et $N(a + eU) = a^2 - abe + ce^2$. \item (Page~49) Sur tout $R$, les couples $(\beta, \gamma)$ des éléments de $A$ sont ceux qui vérifient $\beta \equiv \gamma b$ modulo~$2$, et les couples $(\lambda, \zeta)$ des éléments de $E$ ceux qui vérifient $\zeta \equiv \lambda b$ modulo~$2$ ; $b$ est un relèvement de $T_0$. Si $2$ est régulier, $y \mapsto (\beta, \gamma)$ et $x \mapsto (\lambda, \zeta)$ sont injectives. \item (Pages~50 et~51) L'unité a pour couple $(2, 0)$, et, sans division, \[ 2\beta(yy') = \beta\beta' + \gamma\gamma'\delta, \qquad 2\gamma(yy') = \beta\gamma' + \gamma\beta', \qquad 4N(y) = \beta^2 - \gamma^2\delta. \] \item (Pages~50 et~52) $2\,x(y) = \lambda\beta + \gamma\zeta$, et $4Q(x) = \zeta^2 - \lambda^2\delta$. \item (Pages~46 et~50) $\varphi_N(y)$ a pour couple $(\beta, -\gamma\delta)$, et $Q(\varphi_N(y)) = -N(y)\,\delta$. \item (Pages~49 à~52, $L$ inversible) Soit $\tau \in L$ et $\delta \in L \otimes L$ avec $\tau \otimes \tau - \delta \in 4\,(L \otimes L)$, et $(\beta, \gamma)$, $(\beta', \gamma') \in R \times \check L$ avec $\beta \equiv \gamma(\tau)$ et $\beta' \equiv \gamma'(\tau)$ modulo~$2$. Alors $\beta^2 - \gamma^2\delta \in 4R$, $\beta\beta' + \gamma\gamma'\delta \in 2R$ et $\beta\gamma' + \beta'\gamma \in 2\check L$ ; si $2$ est régulier, des moitiés $\beta''$, $\gamma''$ de ces deux derniers vérifient encore $\beta'' \equiv \gamma''(\tau)$ modulo~$2$. Si $\zeta \in L$ et $\zeta \equiv \lambda\tau$ modulo $2L$, alors $\zeta \otimes \zeta - \lambda^2\delta \in 4\,(L \otimes L)$. \end{enumerate} \end{theoreme} \end{encadre} \begin{proof} (1) Dans la base $(1, U)$, la multiplication par $y = a + eU$ envoie $1$ sur $a + eU$ et $U$ sur $-ec + (a - eb)U$, puisque $U^2 = -bU - c$ ; la trace et le déterminant de la matrice $\begin{pmatrix} a & -ec \\ e & a - eb \end{pmatrix}$ sont $2a - eb$ et $a^2 - abe + ce^2$ (\texttt{trace\_qalg}, \texttt{norm\_qalg}). (2) $\beta = 2a - eb = eb + 2(a - eb)$ ; inversement, si $\beta = \gamma b + 2s$, l'élément $(s + \gamma b) + \gamma U$ convient. Si $\beta = \gamma = 0$, alors $2a = 0$, donc $a = 0$ quand $2$ est régulier. Du côté de $E$, $\mathrm{Tr}(U) = -b$ donne $\zeta = 2x(U) + \lambda b$ ; la forme $\lambda\,1^\vee + s\,U^\vee$ a pour couple $(\lambda, \lambda b + 2s)$, et $x$ est connu par $x(1)$ et $x(U)$ (\texttt{recon\_range}, \texttt{recon\_injective}, \texttt{eCoord\_range}, \texttt{eCoord\_injective}). (3) à (5) Ce sont des identités entre polynômes en $a, e, a', e', b, c$ et $x(1), x(U)$, une fois écrits $yy' = (aa' - ee'c) + (ae' + a'e - ee'b)U$, $\varphi_N(y)(1) = 2a - eb$ et $\varphi_N(y)(U) = 2ec - ab$ (\texttt{recon\_one}, \texttt{recon\_mul}, \texttt{recon\_norm}, \texttt{coupling}, \texttt{four\_qE}, \texttt{phiN\_coords}). (6) On écrit $\beta = \gamma(\tau) + 2s$, $\beta' = \gamma'(\tau) + 2s'$, $\delta = \tau \otimes \tau - 4k$, et $\gamma\gamma'\delta$ pour $(\gamma \otimes \gamma')(\delta)$. Alors $\beta^2 - \gamma^2\delta = 4(\gamma(\tau)s + s^2 + \gamma^2k)$ et $\beta\beta' + \gamma\gamma'\delta = 2(\gamma(\tau)\gamma'(\tau) + s\gamma'(\tau) + s'\gamma(\tau) + 2ss' - 2\gamma\gamma'k)$. La symétrie de $\check L \otimes \check L$, à laquelle on applique $f \otimes g \mapsto g(\tau)f$, donne $\gamma'(\tau)\gamma = \gamma(\tau)\gamma'$, d'où $\beta\gamma' + \beta'\gamma = 2(\gamma(\tau)\gamma' + s\gamma' + s'\gamma)$. Évaluée en $\tau$, la seconde moitié donne $2\gamma''(\tau) = \beta\gamma'(\tau) + \beta'\gamma(\tau)$, et $2(\beta'' - \gamma''(\tau)) = 4(ss' - \gamma\gamma'k)$ ; on simplifie par~$2$. Enfin, si $\zeta = \lambda\tau + 2a$, la symétrie $a \otimes \tau = \tau \otimes a$ donne $\zeta \otimes \zeta - \lambda^2\delta = 4(\lambda^2k + \lambda\,\tau \otimes a + a \otimes a)$ (\texttt{div\_norm}, \texttt{div\_prod\_fst}, \texttt{div\_prod\_snd}, \texttt{div\_prod\_mem}, \texttt{div\_qform}). \end{proof} \begin{remarque} Chaque division des pages~49 à~52 est donc légitime, comme la page le vérifie \q{à chaque étape}, et dans le cas libre la description de $A$ et de $E$ par les couples $(\beta, \gamma)$ et $(\lambda, \zeta)$ redonne l'algèbre, sa trace, sa norme et son produit. Le signe de $Q(\varphi_N(x)) = -N(x)\,\delta$, couvert page~46 et écrit $+$ page~52, est confirmé. Pour $L$ non trivial, seule la légitimité des divisions et la stabilité du produit sont démontrées ; que les couples $(\beta, \gamma)$ forment un anneau isomorphe à l'algèbre du revêtement ne l'est pas, faute de l'équivalence de la page~45. \end{remarque} \begin{enonce}[Pages 45 et 48, \emph{la forme globale}\piste{84-two-regular-triplet-classification}]\nonverifie Sur un schéma ou un topos localement annelé où $2$ n'est pas diviseur de zéro, la catégorie fibrée des revêtements quadratiques est équivalente à celle des triplets $(L, P_1, Q)$ (page~45), donc à celle des triplets $(L, \delta, T_0)$, compatiblement aux changements de base. \end{enonce} \noindent Ne sont pas démontrés : l'équivalence de la page~45 entre algèbres quadratiques localement libres de rang~$2$ et triplets $(L, P_1, Q)$, quand $L$ n'est pas trivial (le cas libre est l'énoncé des pages~47 à~53 ci-dessus) ; elle demande que $\mathcal O \to A$ soit scindé et que $A/\mathcal O$ soit inversible, ce qui n'est pas formalisé ; le passage d'une base affine à un schéma, où $P_1$ n'a plus d'origine globale et les morphismes se recollent. La compatibilité aux changements de base entre bases affines est démontrée plus haut ; c'est le recollement qui manque pour en faire une équivalence de catégories fibrées sur un schéma. \noindent\emph{La catégorie des extensions $\chi$-scindées.} On reprend les coordonnées ci-dessus, sur un anneau commutatif $R$ et pour $\chi \in R$. Un objet est un triplet $(M, L, b)$, $b : M \to L$ linéaire, c'est-à-dire l'extension scindée $0 \to L \to M \oplus L \to M \to 0$ munie du $\chi$-scindage $(\pi_b, \varpi_b)$ (\texttt{ChiExt}). Un morphisme $(M, L, b) \to (M', L', b')$ est un triplet $(f, \varphi, w)$, $f : M \to M'$, $\varphi : L \to L'$, $w : M \to L'$, avec $\varphi \circ b = b' \circ f + \chi w$ ; il représente l'application $F(\eta, \xi) = (f\eta, \varphi\xi + w\eta)$ de $M \oplus L$ dans $M' \oplus L'$. Le composé de $(f, \varphi, w)$ puis $(g, \psi, v)$ est $(gf, \psi\varphi, \psi w + vf)$. Le produit est $(M_1 \otimes M_2, L_1 \otimes L_2, b_1 \otimes b_2)$ (page~78), celui de deux morphismes est $(f_1 \otimes f_2, \varphi_1 \otimes \varphi_2, w)$ avec $w = b'_1f_1 \otimes w_2 + w_1 \otimes b'_2f_2 + \chi\, w_1 \otimes w_2$, la donnée $u$ de la page~129 ; l'unité est $(R, R, \mathrm{id})$, $\pi(u, \lambda) = \lambda + \chi u$. Les contraintes d'associativité, d'unité et de commutativité sont celles du produit tensoriel sur $M$ et sur $L$, avec $w = 0$. \begin{encadre} \begin{theoreme}[Grothendieck, pages 65 à 79, produit des extensions $\chi$-scindées, base affine\piste{84-chi-trivialised-extension-product}] Soit $R$ un anneau commutatif et $\chi \in R$. \begin{enumerate} \item Une application linéaire $F : M \oplus L \to M' \oplus L'$ qui induit $f$ sur $M$ et $\varphi$ sur $L$ est de la forme $(\eta, \xi) \mapsto (f\eta, \varphi\xi + w\eta)$ ; elle respecte les $\chi$-rétractions, $\pi_{b'} F = \varphi\pi_b$, si et seulement si $\varphi b = b'f + \chi w$, et de même pour les $\chi$-sections, $F\varpi_b = \varpi_{b'}f$. \item Les extensions scindées munies d'un $\chi$-scindage, avec ces morphismes et le produit $b_1 \otimes b_2$, forment une catégorie monoïdale symétrique. \item Un morphisme $(f, \varphi, w)$ est un isomorphisme dès que $f$ et $\varphi$ en sont. \item (Page~79) Soit $L$ un $R$-module et $b \in L$. L'objet $(R, L, b)$ est inversible pour le produit, c'est-à-dire $(R, L, b) * Y \simeq (R, R, \mathrm{id})$ pour un objet $Y$, si et seulement si $L$ est un module inversible et $b$ engendre $L$ modulo $\chi$, $L = Rb + \chi L$, c'est-à-dire si la section $T_0 = -b_0$ engendre $L_0 = L/\chi L$ sur $V(\chi)$. \end{enumerate} \end{theoreme} \end{encadre} \begin{proof} (1) $F(0, \xi) = (0, \varphi\xi)$, et la première coordonnée de $F(\eta, 0)$ est $f\eta$ ; on pose $w\eta$ la seconde. Alors $\pi_{b'}F(\eta, \xi) = b'f\eta + \chi\varphi\xi + \chi w\eta$ et $\varphi\pi_b(\eta, \xi) = \varphi b\eta + \chi\varphi\xi$ ; de même $F\varpi_b(\eta) = (\chi f\eta, -\varphi b\eta + \chi w\eta)$ et $\varpi_{b'}(f\eta) = (\chi f\eta, -b'f\eta)$ (\texttt{eq\_extMap}, \texttt{extMap\_pi\_iff}, \texttt{extMap\_varpi\_iff}). (2) Le composé est un morphisme : $\psi\varphi b = \psi(b'f + \chi w) = (b''g + \chi v)f + \chi\,\psi w = b''(gf) + \chi(\psi w + vf)$. Le produit de deux morphismes en est un : $(b_1 \otimes b_2)(\varphi_1 \otimes \varphi_2) = (b'_1f_1 + \chi w_1) \otimes (b'_2f_2 + \chi w_2)$, qu'on développe par bilinéarité de $\otimes$ sur les morphismes, ce qui donne $(b'_1 \otimes b'_2)(f_1 \otimes f_2) + \chi w$ : c'est le calcul de la page~129, sans division. Les axiomes portent sur trois composantes. Sur $M$ et sur $L$, ce sont ceux de la catégorie monoïdale symétrique des $R$-modules (\texttt{ModuleCat} de mathlib). Sur $w$, il reste deux identités. La fonctorialité du produit, $(p_1 \otimes p_2)(q_1 \otimes q_2) = p_1q_1 \otimes p_2q_2$, se ramène, après avoir remplacé $b'_i\varphi'_i$ par $f'_ib''_i + \chi w'_i$, à l'égalité de deux sommes de huit termes. La naturalité de l'associativité développe les deux membres en sept termes $(x_1 \otimes x_2) \otimes x_3$ et $x_1 \otimes (x_2 \otimes x_3)$, $x_i \in \{b'_if_i, w_i\}$, que l'associativité du produit tensoriel identifie. Toutes les autres identités, pentagone, triangle, hexagones, symétrie, n'ont que des $w$ nuls (\texttt{ChiExt.\allowbreak{}instMonoidalCategory}, \texttt{ChiExt.\allowbreak{}instSymmetricCategory}, avec \texttt{tensorHom\_comp\_tensorHom'} et \texttt{associator\_naturality'}). (3) Si $f$ et $\varphi$ sont inversibles, $(f^{-1}, \varphi^{-1}, -f^{-1}w\varphi^{-1})$ est un morphisme, en composant $\varphi b = b'f + \chi w$ par $f^{-1}$ et $\varphi^{-1}$, et c'est l'inverse : les composantes $w$ des deux composés sont $w\varphi^{-1} - w\varphi^{-1} = 0$ et $-f^{-1}w + f^{-1}w = 0$ (\texttt{ChiExt.\allowbreak{}isIso\_of}). (4) Nécessité. Soit $Y = (M', L', b')$ et $(f, \varphi, w)$ un isomorphisme $(R, L, b) * Y \to (R, R, \mathrm{id})$. Sa composante $\varphi : L \otimes L' \to R$ est un isomorphisme, donc $L$ est inversible (\texttt{Module.\allowbreak{}Invertible.\allowbreak{}left} de mathlib). Sa composante $f : R \otimes M' \to R$ est surjective : il existe $m'$ avec $f(1 \otimes m') = 1$. Posons $y = b'(m')$ ; la relation $\varphi(b \otimes b') = f + \chi w$, évaluée en $1 \otimes m'$, donne $\varphi(b \otimes y) = 1 + \chi c$. Pour $x \in L$, la symétrie $x \otimes b = b \otimes x$ de $L \otimes L$ (\texttt{Module.\allowbreak{}Invertible.\allowbreak{}tmul\_comm}), à laquelle on applique $u \otimes v \otimes y \mapsto \varphi(v \otimes y)\,u$, donne $(1 + \chi c)\,x = \varphi(x \otimes y)\,b$, donc $x = \varphi(x \otimes y)\,b + \chi(-cx) \in Rb + \chi L$. Suffisance. Écrivons $1 = \sum \gamma_i(x_i)$ avec $\gamma_i \in L^\vee$, ce que permet l'inversibilité de $L$, et $x_i = r_ib + \chi y_i$. Alors $\beta = \sum r_i\gamma_i$ vérifie $\beta(b) = 1 - \chi\sum\gamma_i(y_i) = 1 + \chi c$. (Lean le dit sans choisir de somme : l'idéal $\beta(b)$, $\beta \in L^\vee$, plus $\chi R$, contient l'image de l'accouplement $L^\vee \otimes L \to R$, qui est $R$.) Soit $Y = (R, L^\vee, 1 \mapsto \beta)$. Le morphisme $(R \otimes R \simeq R,\ L \otimes L^\vee \simeq R,\ c \cdot (R \otimes R \simeq R))$ vérifie la relation, puisque $(rb) \otimes (s\beta) \mapsto rs\,\beta(b) = rs + \chi\,c\,rs$, et c'est un isomorphisme par~(3). Enfin $L = Rb + \chi L$ équivaut à ce que la classe de $b$ engendre $L/\chi L$ (\texttt{ChiExt.\allowbreak{}invertible\_iff\_generates}, \texttt{generates\_iff\_span}, \texttt{ChiExt.\allowbreak{}invertible\_iff\_span}). \end{proof} \begin{remarque} La note marginale de la page~79 dit \q{$L$ inversible et $T_0$ base de $L_0$} ; la preuve ci-dessus montre que l'inversibilité de $L$ est nécessaire, et qu'avec elle il suffit que $b$ engendre $L$ modulo~$\chi$ : on n'a pas à localiser, ni à rendre $b$ unitaire hors de $V(\chi)$ comme le fait la lecture. L'inverse est $(R, L^\vee, \beta)$ pour toute forme $\beta$ avec $\beta(b) \equiv 1$ modulo $\chi$ ; pour $L = R$, c'est la classe de $g$ avec $bg \equiv 1$ de l'énoncé précédent. Rien n'est divisé par $\chi$ ni par $2$, et $\chi$ peut être nul : pour $\chi = 0$, l'objet est inversible si et seulement si $b$ est une base de $L$. Le critère n'utilise que les objets dont le quotient est $R$, qui sont tous scindés sur une base affine. \end{remarque} \noindent\emph{Le produit intrinsèque, sur une base affine.} Une extension $\chi$-trivialisée de $\mathcal O$ par $L$ est la donnée de $\iota : L \to E$, $\psi : E \to R$ et $\pi : E \to L$ linéaires avec $\psi\iota = 0$ et $\pi\iota = \chi$ (\texttt{ChiTriv}) ; rien n'est scindé, et l'exactitude n'est supposée que là où elle sert. Pour deux d'entre elles, on pose $K = (L_1 \otimes E_2) \oplus (E_1 \otimes L_2)$, d'image $E_1 \otimes_0 E_2$ dans $E_1 \otimes E_2$ par $j = (\iota_1 \otimes \mathrm{id}, \mathrm{id} \otimes \iota_2)$, et $\mu = (\mathrm{id} \otimes \pi_2, \pi_1 \otimes \mathrm{id}) : K \to L_1 \otimes L_2$ (page~68). Le produit est le quotient \[ E_1 * E_2 = \bigl((E_1 \otimes E_2) \oplus (L_1 \otimes L_2)\bigr) / \{(j(k), -\mu(k))\}, \] où $x_1 * x_2$ est la classe de $(x_1 \otimes x_2, 0)$ (\texttt{Amal}, \texttt{starA}, \texttt{incl}). \begin{encadre} \begin{theoreme}[Grothendieck, pages 68 à 76, le produit par somme amalgamée, base affine\piste{84-chi-trivialised-extension-product}] Soit $R$ un anneau commutatif et $\chi \in R$. \begin{enumerate} \item $E_1 * E_2$ est la somme amalgamée de $E_1 \otimes E_2$ et de $L_1 \otimes L_2$ le long de $K$, dans la catégorie des $R$-modules. Elle porte, sans division et sans scindage, $\psi(x_1 * x_2) = \psi_1(x_1)\psi_2(x_2)$, l'application $L_1 \otimes L_2 \to E_1 * E_2$ et la $\chi$-rétraction $\pi(x_1 * x_2) = \pi_1(x_1) \otimes \pi_2(x_2)$, $\pi = \chi$ sur $L_1 \otimes L_2$ (page~70) : c'est une extension $\chi$-trivialisée. \item (Pages~72 à~74) $u_1 * x_2 = u_1 \otimes \pi_2(x_2)$, $x_1 * u_2 = \pi_1(x_1) \otimes u_2$, et $(x_1 + u_1) * (x_2 + u_2) = x_1 * x_2 + u_1 \otimes \pi_2(x_2) + \pi_1(x_1) \otimes u_2 + \chi\,u_1 \otimes u_2$. \item Toute suite exacte $0 \to L \to E \to R \to 0$ est scindée. Pour des scindages $x_1$, $x_2$, de rétractions $p_1$, $p_2$, on a $E_1 * E_2 \simeq R \times (L_1 \otimes L_2)$, avec $\psi$ la première projection, $L_1 \otimes L_2$ le second facteur et $\pi(\lambda, u) = \lambda\, b_1 \otimes b_2 + \chi u$, $b_i = \pi_i(x_i)$. En particulier $0 \to L_1 \otimes L_2 \to E_1 * E_2 \to R \to 0$ est exacte, scindée par $x_1 * x_2$, et $b = b_1 \otimes b_2$ (page~78) : c'est le produit $(\mathcal O, L_1, b_1) \otimes (\mathcal O, L_2, b_2)$ de la catégorie des extensions $\chi$-scindées ci-dessus. \item (Pages~75 et~76) Soit $N$ un $R$-module, $f : P_1 \times P_2 \to N$, où $P_i = \psi_i^{-1}(1)$, et $\alpha : L_1 \otimes L_2 \to N$ linéaire, avec \[ \begin{gathered} f(x_1 + u_1, x_2) = f(x_1, x_2) + \alpha(u_1 \otimes \pi_2(x_2)), \\ f(x_1, x_2 + u_2) = f(x_1, x_2) + \alpha(\pi_1(x_1) \otimes u_2). \end{gathered} \] Si les extensions sont exactes, il existe une unique application linéaire $g : E_1 * E_2 \to N$ avec $g(x_1 * x_2) = f(x_1, x_2)$ sur $P_1 \times P_2$ et $g = \alpha$ sur $L_1 \otimes L_2$. Réciproquement, toute application linéaire $g$ définit ainsi un tel couple $(f, \alpha)$. \end{enumerate} \end{theoreme} \end{encadre} \begin{proof} (1) Une application linéaire hors du quotient est un couple $(g, h)$ avec $g \circ j = h \circ \mu$ ; c'est la propriété universelle de la somme amalgamée, et le cocône correspondant est colimite dans \texttt{ModuleCat} (\texttt{isPushout}). Le couple $(\psi_1 \otimes \psi_2, 0)$ convient, puisque $\psi_i\iota_i = 0$ ; le couple $(\pi_1 \otimes \pi_2, \chi)$ aussi, puisque $\pi_1\iota_1(u_1) \otimes \pi_2(x_2) = \chi\,u_1 \otimes \pi_2(x_2) = \chi\,\mu(u_1 \otimes x_2)$, et de même de l'autre côté. (2) C'est la relation $(j(k), -\mu(k)) = 0$ pour $k = u_1 \otimes x_2$ et $k = x_1 \otimes u_2$, puis la bilinéarité. (3) Si $\psi(x_0) = 1$, l'endomorphisme $e \mapsto e - \psi(e)x_0$ est à valeurs dans $\ker\psi = \iota(L)$, et l'on en tire la rétraction $p$ (\texttt{ChiTriv.\allowbreak{}splittingOf}) ; alors $e = \iota p(e) + \psi(e)x_0$ et $\pi = \chi p + \psi\, b$. L'application $e_1 \otimes e_2 \mapsto (\psi_1(e_1)\psi_2(e_2),\ p_1(e_1) \otimes \pi_2(e_2) + \psi_1(e_1)\, b_1 \otimes p_2(e_2))$, avec l'identité sur $L_1 \otimes L_2$, passe au quotient : sur $e_1 \otimes \iota_2 u_2$, la seconde coordonnée vaut $(\chi p_1(e_1) + \psi_1(e_1) b_1) \otimes u_2 = \pi_1(e_1) \otimes u_2$. Son inverse est $(\lambda, u) \mapsto \lambda\,x_1 * x_2 + u$ : par~(2), $e_1 * e_2 = \psi_1(e_1)\psi_2(e_2)\,x_1 * x_2 + p_1(e_1) \otimes \pi_2(e_2) + \psi_1(e_1)\, b_1 \otimes p_2(e_2)$. On lit $\psi$, $\iota$ et $\pi$ dans ces coordonnées ; l'identification avec le produit de la catégorie précédente est $R \otimes R \simeq R$ sur $M$ et l'identité sur $L_1 \otimes L_2$ (\texttt{splitEquiv}, \texttt{split\_coords}, \texttt{prod\_exact}, \texttt{prodSplitting\_b}, \texttt{ChiExt.\allowbreak{}ofSectionTensorIso}). (4) Existence : $g(\lambda, u) = \lambda f(x_1, x_2) + \alpha(u)$ dans les coordonnées de~(3) ; pour $y_i = x_i + \iota_i p_i(y_i)$ dans $P_i$, les deux relations donnent $f(y_1, y_2) = f(x_1, x_2) + \alpha(b_1 \otimes p_2(y_2)) + \alpha(p_1(y_1) \otimes \pi_2(y_2))$, qui est $g(y_1 * y_2)$. Unicité : par la formule de~(3) pour $e_1 * e_2$, $g$ est connu par $g(x_1 * x_2) = f(x_1, x_2)$ et par $\alpha$. La réciproque est~(2) (\texttt{biaffine\_universal}, \texttt{biaffine\_of\_linear}). \end{proof} \begin{remarque} La construction de la page~68 est démontrée telle quelle, sans division et sans choisir de scindage, pour $\chi$ quelconque, nul ou diviseur de zéro ; sur une base affine, toute extension de $\mathcal O$ est scindée, et le produit intrinsèque y coïncide avec le produit en coordonnées $b_1 \otimes b_2$, ce qui transporte au produit intrinsèque la structure de catégorie monoïdale symétrique démontrée plus haut. La remarque de la page~76, que la donnée de $\alpha$ n'est pas superflue, se retrouve dans l'énoncé : $g$ est déterminé par $f$ et $\alpha$ ensemble, $\mu$ n'étant pas surjectif en général. La variante de la page où l'on exige aussi $\pi_\Pi(f(x_1, x_2)) = \pi_1(x_1) \otimes \pi_2(x_2)$ n'est pas formalisée. \end{remarque} \begin{enonce}[Pages 65 à 79, \emph{le produit intrinsèque}\piste{84-chi-trivialised-extension-product}]\nonverifie Soit $\chi \in \Gamma(\mathcal O)$ sur un schéma ou un topos annelé quelconque. Les extensions $0 \to L \to E \to M \to 0$, non nécessairement scindées, munies d'un $\chi$-scindage, forment une catégorie monoïdale symétrique pour le produit $E_1 * E_2$ construit par somme amalgamée de $E_1 \otimes E_2$ et $L_1 \otimes L_2$ le long de $E_1 \otimes_0 E_2$, sans division ; dans le cas scindé, il redonne $b = b_1 \otimes b_2$. \end{enonce} \noindent Ne sont pas démontrés : la fonctorialité et les contraintes du produit par somme amalgamée écrites intrinsèquement, sans passer par les coordonnées ; les extensions d'un quotient $M$ quelconque ; le passage d'une base affine à un schéma, où les extensions de $\mathcal O$ par $L$ ne sont plus scindées globalement et où les coordonnées se recollent par la relation de cocycle de la page~131. La construction par somme amalgamée, son identification avec le produit en coordonnées et la propriété universelle des applications bi-affines sont démontrées sur une base affine (théorème ci-dessus). \section[Cote 160 : le déterminant de Moore et les coefficients de Dickson]{Cote 160 : le déterminant de Moore et les coefficients de Dickson\protect\verifie{Folder160}}\label{sec:160} La cote 160, \emph{Schémas [en] groupes : notes manuscrites (s.d.)}, est rangée dans le groupe \q{Dérivateurs} que l'inventaire date de 1990-[1991] ; ses vingt-deux pages traitent des sous-groupes finis de $\mathbb G_a$ en caractéristique $p$. Aux pages~7 à~9, le déterminant de Moore $\Delta_n(\xi) = \det(\xi_j^{p^i})$ donne par la règle de Cramer les coefficients $A_i$ de la relation $\xi_k^{p^n} + A_{n-1}\xi_k^{p^{n-1}} + \dots + A_0 \xi_k = 0$, et la page~9 affirme sans raison que $\Delta_n$ divise les numérateurs (\lot{160}{1}{9}). Les pages~14 et~15 transposent la construction à un faisceau $E$ localement libre de rang~$n$ muni de $u : E^{(p)} \simeq E$ : $\Delta_n^E$ est homogène de degré $\frac{p^n-1}{p-1}$, les $A_i^E$, définis hors du diviseur des zéros de $\Delta_n^E$, s'étendent à $V(E)$ tout entier, et $A_0^E = \pm(\Delta_n^E)^{p-1}$ (\lot{160}{1}{14}). On traite ici le cas où $E$ est trivialisé et $u$ l'identité. \begin{theoreme}[D'après les pages 9, 14 et 15, $E$ trivialisé\piste{160-relative-moore-determinant}] Soit $p$ premier. Sur tout anneau commutatif, $\Delta_n(c\xi) = c^{(p^n-1)/(p-1)}\Delta_n(\xi)$. Il existe des polynômes $A_0, \dots, A_{n-1} \in \mathbf F_p[X_1, \dots, X_n]$ tels que, pour toute $\mathbf F_p$-algèbre $S$ et tout $\xi \in S^n$, $\xi_k^{p^n} + \sum_i A_i(\xi)\, \xi_k^{p^i} = 0$ pour tout $k$ ; si $\Delta_n(\xi)$ est inversible, les $A_i(\xi)$ sont les seuls coefficients de cette relation. Enfin $A_0 = (-1)^n \Delta_n^{p-1}$. \end{theoreme} \noindent L'énoncé tient : voir \texttt{moore\_smul'}, \texttt{dickson\_relation\_eval}, \texttt{dickson\_unique} et \texttt{A\_zero\_eval} dans \href{\leanblob/Folder160.lean}{\texttt{Folder160.\allowbreak{}lean}}, avec le signe $(-1)^n$ que page et lecture laissent en $\pm$. \begin{remarque} Les $A_i$ sont les coefficients de $\prod_{\lambda \in \mathbf F_p^n}(T - \lambda \cdot X)$, et $\Delta_{n+1}(T, X_1, \dots, X_n) = (-1)^n \Delta_n \prod_\lambda (T - \lambda \cdot X)$ : les $p^n$ formes $\lambda \cdot X$ sont des racines distinctes d'un polynôme de degré $p^n$ en $T$ dont le coefficient dominant $\pm\Delta_n$ est non nul (par récurrence sur $n$). La factorisation de la page~7 et sa constante $c$ ne servent pas. \end{remarque} \noindent\emph{Le signe du corollaire de la page~13.} Pour un sous-groupe étale $M = \operatorname{Ker} f_a$ de $\mathbb G_a$ de rang $p^n$, $f_a = x^{p^n} + a_{n-1}x^{p^{n-1}} + \dots + a_0 x$, la page~13 affirme que les trivialisations de $\Lambda^n_{\mathbf F_p} M$ correspondent bijectivement aux racines $(p-1)$-ièmes de $a_0$ (\lot{160}{1}{13}). Le signe laissé en $\pm$ à la page~9 compte ici. Sur un corps, une base $e = (e_1, \dots, e_n)$ de $M$ donne la trivialisation $e_1 \wedge \dots \wedge e_n$, et $\Delta_n(e)$ en est la valeur ; le théorème précédent donne $a_0 = A_0(e) = (-1)^n \Delta_n(e)^{p-1}$. \begin{encadre} \begin{contrexemple}[Énoncé de l'édition, page 13] Sur $\mathbf F_3$, avec $n = 1$ et $M = \mathbf F_3 = \operatorname{Ker}(x^3 - x)$, on a $a_0 = -1$, qui n'a pas de racine carrée dans $\mathbf F_3$, alors que $\Lambda^1 M = M$ a deux trivialisations, ses deux éléments non nuls. Le corollaire est faux dès que $p$ et $n$ sont impairs. \end{contrexemple} \end{encadre} \noindent En effet $A_0(1) = (-1)^1 \cdot 1^2 = -1$, et les carrés de $\mathbf F_3$ sont $0$ et $1$. En général, si $y^{p-1} = a_0$, alors $(y/\Delta_n)^{p-1} = (-1)^n$, et $-1$ n'est pas une puissance $(p-1)$-ième dans $\mathbf F_p$ pour $p$ impair. \begin{encadre} \begin{enonce}[Énoncé de l'édition, forme corrigée sur un corps] Soient $K$ un corps de caractéristique $p$, $n \geq 1$ et $e \in K^n$ avec $\Delta_n(e) \neq 0$. Pour une matrice $g$ à coefficients dans $\mathbf F_p$, notons $g \cdot e$ la famille $\bigl(\sum_k g_{jk} e_k\bigr)_j$. Alors $\Delta_n(g \cdot e) = \det(g)\,\Delta_n(e)$ ; $\Delta_n(e)$ est une racine $(p-1)$-ième de $(-1)^n a_0$, où $a_0 = A_0(e)$ ; toute racine $(p-1)$-ième de $(-1)^n a_0$ est de la forme $\Delta_n(g \cdot e)$ avec $g \in \mathrm{GL}_n(\mathbf F_p)$ ; et $\Delta_n(g \cdot e) = \Delta_n(h \cdot e)$ si et seulement si $\det g = \det h$. Les trivialisations correspondent donc aux racines $(p-1)$-ièmes de $(-1)^n a_0$, les fibres étant les orbites de $\mathrm{SL}_n(\mathbf F_p)$. \end{enonce} \end{encadre} \begin{proof} Les coefficients de $g$ sont fixes par Frobenius, donc $\bigl(\sum_k g_{jk} e_k\bigr)^{p^i} = \sum_k g_{jk} e_k^{p^i}$ : la matrice de Moore de $g \cdot e$ est celle de $e$ multipliée par la transposée de $g$, et les déterminants se multiplient. La deuxième assertion est le théorème précédent, puisque $(-1)^n A_0(e) = \Delta_n(e)^{p-1}$. Soit $y$ avec $y^{p-1} = \Delta_n(e)^{p-1}$ ; alors $y \neq 0$, et $c = y/\Delta_n(e)$ vérifie $c^{p-1} = 1$, donc $c^p = c$. Les solutions de $c^p = c$ dans $K$ sont les $p$ éléments de $\mathbf F_p$, puisqu'un polynôme de degré $p$ a au plus $p$ racines : $c \in \mathbf F_p^\times$, et la matrice diagonale $g = \mathrm{diag}(c, 1, \dots, 1)$ donne $\Delta_n(g \cdot e) = c\,\Delta_n(e) = y$. La dernière assertion vient de la première, $\Delta_n(e)$ étant non nul et $\mathbf F_p \to K$ injectif. \end{proof} \begin{lemme}[Changement de base] Soient $K$ un corps de caractéristique $p$ et $e, f \in K^n$ deux familles $\mathbf F_p$-libres engendrant le même sous-$\mathbf F_p$-espace $M \subset K$. Il existe $g \in \mathrm{GL}_n(\mathbf F_p)$ tel que $f = g \cdot e$, et alors $\Delta_n(f) = \det(g)\,\Delta_n(e)$. \end{lemme} \begin{proof} Les familles $e$ et $f$ sont deux bases de $M$ ; la matrice de passage $P$, de colonnes les coordonnées des $f_j$ dans la base $e$, est inversible, et $f_j = \sum_k P_{kj} e_k$, soit $f = {}^t\!P \cdot e$ avec $\det {}^t\!P = \det P$ inversible. La formule pour $\Delta_n$ est alors la première assertion de l'énoncé précédent. Voir \texttt{exists\_act\_eq\_of\_span\_eq} et \texttt{moore\_eq\_of\_span\_eq}, qui s'appuient sur \texttt{Basis.\allowbreak{}toMatrix}, \texttt{Basis.\allowbreak{}invertibleToMatrix} et \texttt{Basis.\allowbreak{}sum\_toMatrix\_smul\_self} de Mathlib. \end{proof} \noindent Les valeurs $\Delta_n(f)$, pour $f$ parcourant les bases de $M$, sont donc exactement les $\Delta_n(g \cdot e)$ pour une base fixée $e$ : avec l'énoncé précédent, elles forment l'ensemble des racines $(p-1)$-ièmes de $(-1)^n a_0$, et deux bases ont même valeur si et seulement si elles diffèrent d'un élément de $\mathrm{SL}_n(\mathbf F_p)$. \noindent\emph{Le théorème de Dickson.} Les pages~9 à~12 en tirent les invariants de $\Gamma_n = \mathrm{GL}_n(\mathbf F_p)$ et de $S\Gamma_n = \mathrm{SL}_n(\mathbf F_p)$, opérant sur $\mathbf F_p[X_1, \dots, X_n]$ par $X_j \mapsto \sum_k g_{jk} X_k$ (\lot{160}{1}{9}). \begin{theoreme}[Dickson, pages 9 à 12\piste{160-relative-moore-determinant}] Soit $p$ premier. Un polynôme $f \in \mathbf F_p[X_1, \dots, X_n]$ est invariant par $\mathrm{GL}_n(\mathbf F_p)$ si et seulement s'il appartient à la sous-algèbre engendrée par $A_0, \dots, A_{n-1}$, et ceux-ci sont algébriquement indépendants : $\mathbf F_p[X_1, \dots, X_n]^{\mathrm{GL}_n(\mathbf F_p)} = \mathbf F_p[A_0, \dots, A_{n-1}]$ est une algèbre de polynômes. De même $\mathbf F_p[X_1, \dots, X_n]^{\mathrm{SL}_n(\mathbf F_p)} = \mathbf F_p[\Delta_n, A_1, \dots, A_{n-1}]$, algèbre de polynômes en $\Delta_n, A_1, \dots, A_{n-1}$. \end{theoreme} \begin{proof}[Esquisse] La démonstration vérifiée est la démonstration galoisienne, non celle de la page, qui passe par le Main Theorem de Zariski. Les $A_i$ sont invariants : $g$ permute les formes $\lambda \cdot X$, donc fixe $\prod_\lambda (T - \lambda \cdot X)$ ; et $\Delta_n(g \cdot X) = \det(g)\,\Delta_n(X)$. Chaque $X_k$ est racine du polynôme unitaire $\prod_\lambda (T - \lambda \cdot X)$, à coefficients dans $\mathbf F_p[A]$ ; $\mathbf F_p[X]$ est donc entier sur $\mathbf F_p[A]$, et les $n$ éléments $A_i$, qui engendrent une algèbre sur laquelle une algèbre de degré de transcendance $n$ est algébrique, sont algébriquement indépendants ; de même pour $\Delta_n, A_1, \dots, A_{n-1}$, puisque $A_0 = (-1)^n \Delta_n^{p-1}$. Le corps $\mathbf F_p(X)$ est le corps de décomposition sur $\mathbf F_p(A)$ de ce polynôme, séparable puisque sa dérivée est la constante $A_0 \neq 0$ ; c'est une extension galoisienne. Un automorphisme $\sigma$ de $\mathbf F_p(X)$ au-dessus de $\mathbf F_p(A)$ envoie chaque $X_k$ sur une racine, soit une forme $\lambda_k \cdot X$ ; il agit donc comme la matrice $g$ de lignes $\lambda_k$, qui est inversible puisque $\sigma$ est injectif. Un invariant $f$ est fixé par tous les $\sigma$, donc appartient à $\mathbf F_p(A)$ ; entier sur $\mathbf F_p[A]$, algèbre de polynômes donc intégralement close, il appartient à $\mathbf F_p[A]$. Pour $\mathrm{SL}_n$, on prend le corps $\mathbf F_p(\Delta_n, A_1, \dots, A_{n-1})$ : un $\sigma$ qui le fixe fixe $\Delta_n$, donc $\det g = 1$. Voir \texttt{dickson\_theorem}, \texttt{dickson\_algebraicIndependent}, \texttt{dickson\_theorem\_SL} et \texttt{dicksonSL\_algebraicIndependent}, qui s'appuient sur \texttt{IsGalois.\allowbreak{}of\_separable\_splitting\_field}, \texttt{IsGalois.\allowbreak{}mem\_bot\_iff\_fixed} et le degré de transcendance de Mathlib. \end{proof} \noindent Le lemme de la page~11 sur $A_\alpha(X_1, \dots, X_{n-s}, 0, \dots, 0)$, les degrés $p^n - p^i$ des $A_i$ et la démonstration géométrique de la page (quasi-finitude, surjectivité par les sous-groupes de $\mathbb G_a$, Main Theorem de Zariski) ne sont pas formalisés. Ne sont pas démontrés ici : la version relative pour $(E, u)$ non trivial et la trivialisation $(\Lambda^n \check E)^{\otimes(p-1)} \simeq \mathcal O_S$ par $\Lambda^n \check u$ ; la bijection $a \mapsto \operatorname{Ker} f_a$ des pages~2 à~6 ; la forme relative du corollaire de la page~13 sur une base $S$, et l'identification de $\Delta_n(e)$ à une trivialisation de $\Lambda^n_{\mathbf F_p} M$ au sens de la puissance extérieure. \section[Cote 69 : les automorphismes du graphe des vingt-sept droites qui fixent un triangle]{Cote 69 : les automorphismes du graphe des vingt-sept droites qui fixent un triangle\protect\verifie{Folder69}}\label{sec:69} La cote 69, \emph{Graphes cubiques : notes manuscrites (s.d.)}, cent dix-neuf pages, étudie le graphe $C$ des vingt-sept droites d'une surface cubique, deux droites étant liées quand elles se coupent, et son groupe d'automorphismes $W$, d'ordre $51\,840$. Aux pages~25 et~26, elle marque un triangle $t$ (trois droites deux à deux concourantes) et décrit $(C, t)$ par un ensemble $t$ à trois éléments, un plan $V$ sur $\mathbf F_2$ et un torseur sous une extension centrale $\widetilde\Psi$ d'ordre $32$, produit de Baer de trois copies de $Q_8$ (\lot{69}{2}{25}, \lot{69}{2}{26}). La page~25 donne le groupe $W'_t$ des automorphismes qui fixent $t$ point par point comme extension de $\mathfrak S_4$ par $\mathbf F_2^3$, et le corollaire de la page~26 en tire l'ordre du groupe $W_t$ des automorphismes de $(C, t)$. \noindent\emph{Conventions.} Les sommets sont $a_i$, $b_i$ ($0 \leq i \leq 5$) et $c_{ij}$ ($i < j$) ; $a_i$ et $b_j$ sont liés si $i \neq j$, $a_i$ et $b_i$ sont liés à $c_{jk}$ si $i \in \{j, k\}$, $c_{ij}$ et $c_{kl}$ sont liés si $\{i, j\} \cap \{k, l\} = \emptyset$, et il n'y a pas d'autre arête. C'est le modèle classique des vingt-sept droites ; chaque sommet a dix voisins. On prend $t = \{a_0, b_1, c_{01}\}$. \begin{theoreme}[Grothendieck, page 26] Le groupe $W_t$ des automorphismes de $C$ qui conservent le triangle $t$ est d'ordre $32 \cdot 36 = 1152$. \end{theoreme} \noindent L'énoncé tient : voir \texttt{card\_Wt} et \texttt{card\_aut} dans \href{\leanblob/Folder69.lean}{\texttt{Folder69.\allowbreak{}lean}}. Le sous-groupe $W'_t$ est d'ordre $192 = 8 \cdot 24$, comme le donne la suite exacte de la page~25 (\texttt{card\_pointwise}). La vérification est un calcul fini : la base $a_0, b_1, a_1, a_2, a_3, a_4$ a des orbites de tailles $3, 2, 8, 4, 3, 2$ ; chaque orbite est contenue dans l'ensemble des sommets qui ont les mêmes incidences avec les points déjà fixés, et parcourue par des automorphismes explicites que le noyau vérifie ; un automorphisme qui fixe la base fixe tout, car la base sépare les sommets. La cote~74 retrouve $1152$ par un autre chemin, les $96$ autotopies de la table de Klein (§\,\ref{sec:74}). Ne sont pas démontrés ici : la description de $(C, t)$ par $(t, V, \widetilde P)$ et l'équivalence de catégories de la page~26, l'identification de $\widetilde\Psi$ au produit de Baer des relevés de $Q_8$, la suite exacte $1 \to \widetilde\Psi \to W_t \to \mathfrak S_t \times \mathfrak S_{V^*} \to 1$, et le rapprochement de $W_t$ avec $W(F_4)$. \section[Cote 89 : la relation fondamentale en rang deux]{Cote 89 : trois vecteurs de somme nulle dans un module libre de rang deux\protect\verifie[\leanblobmain]{Folder89}}\label{sec:89} La cote 89, \emph{[Hexagone] combinatoire. [Ensembles 3-3] : notes manuscrites (s.d.)}, vingt pages non datées du groupe de cotes 69 à 102 que l'inventaire date de 1976 à vers 1986, part de la structure la plus pauvre qui soit : six objets rangés en deux groupes de trois. Les pages~2 à~14 y lisent un hexagone, puis un plan sur $\mathbf F_3$. Les pages~15 à~18 reprennent la question sur un anneau quelconque : comment reconstituer un module libre de rang~$2$ à partir de l'ensemble de ses droites, muni de quelques données combinatoires (\lot{89}{1}{15}). Pour définir l'addition à partir des seules droites, la page~16 s'appuie sur une relation entre trois vecteurs, qu'elle dit se vérifier \q{de suite}. C'est elle que l'on démontre ici. \emph{Les données.} Soient $\Lambda$ un anneau commutatif et $V$ un $\Lambda$-module libre de rang~$2$. Une \emph{droite} de $V$ est un facteur direct libre de rang~$1$ ; pour une droite $x$, on note $D_x$ le sous-module et $T_x$ l'ensemble de ses générateurs. Deux générateurs d'une même droite diffèrent d'une unité de $\Lambda$, de sorte que $T_x$ est un torseur sous le groupe $\Lambda^*$ des unités. Le déterminant $\det V = \Lambda^2 V$ est libre de rang~$1$, et l'on note $u \wedge v$ l'image de $(u, v)$ ; dans une base, $u \wedge v = u_0 v_1 - u_1 v_0$. Deux droites $x$ et $y$ sont \emph{disjointes} si $V = D_x \oplus D_y$, ce qui revient à dire que $u \wedge v$ engendre $\det V$ pour $u \in T_x$ et $v \in T_y$, ou encore que $u \wedge v$ est une unité quand on identifie $\det V$ à $\Lambda$ par une base. Sur un corps, deux droites sont disjointes dès qu'elles sont distinctes ; sur un anneau local, il faut que leurs réductions modulo l'idéal maximal le soient. \emph{L'image du triangle.} Sur $\mathbf R$, $u \wedge v$ est l'aire orientée du parallélogramme construit sur $u$ et $v$. Trois vecteurs de somme nulle sont les côtés d'un triangle parcouru dans l'ordre (figure~\ref{fig:89-triangle}). Deux côtés consécutifs engendrent alors toujours le même parallélogramme, d'aire double de celle du triangle et de même orientation : $u \wedge v = v \wedge w = w \wedge u$. La relation de la page dit que la réciproque est vraie, et qu'elle l'est sur tout anneau dès que $u$ et $v$ forment une base. \begin{figure}[htbp] \centering \begin{tikzpicture}[scale=1.1, >=stealth, every node/.style={font=\small}] \coordinate (A) at (0,0); \coordinate (B) at (3,0.4); \coordinate (C) at (1.2,2); \fill[piste!10] (A) -- (B) -- (C) -- cycle; \draw[->, very thick] (A) -- node[below] {$u$} (B); \draw[->, very thick] (B) -- node[above right] {$v$} (C); \draw[->, very thick] (C) -- node[above left] {$w$} (A); \draw[black!45, dashed] (C) -- (-1.8,1.6) -- (A); \node[black!60] at (-0.45,1.15) {\footnotesize $u \wedge v$}; \end{tikzpicture} \caption{Trois vecteurs de somme nulle, côtés d'un triangle parcouru dans l'ordre. Le parallélogramme construit sur $u$ et $v$, complété en pointillé, a pour aire orientée $u \wedge v$, le double de celle du triangle ; les paires $(v, w)$ et $(w, u)$ donnent la même.} \label{fig:89-triangle} \end{figure} \begin{encadre} \begin{enonce}[Grothendieck, page 16, la relation fondamentale] Soient $\Lambda$ un anneau commutatif, $V$ un $\Lambda$-module libre de rang~$2$, $x$ et $y$ deux droites disjointes, $z$ une droite, et $u \in T_x$, $v \in T_y$, $w \in T_z$. Alors \[ u \wedge v = v \wedge w = w \wedge u \iff u + v + w = 0 . \] \end{enonce} \end{encadre} \noindent La page ajoute que ces relations entraînent que $z$ est disjointe de $x$ et de $y$. La lecture modernisée démontre l'équivalence en écrivant $w = au + bv$ dans la base $(u, v)$ : les égalités équivalent à $a = b = -1$. La démonstration suivie ici, celle de la preuve vérifiée, passe par une identité qui vaut pour trois vecteurs quelconques. \begin{proof} On choisit une base de $V$, qui identifie $\det V$ à $\Lambda$. Pour trois vecteurs quelconques $u$, $v$, $w$ de $V$, on a l'identité de Cramer \[ (v \wedge w)\, u + (w \wedge u)\, v + (u \wedge v)\, w = 0 . \] Elle exprime que trois vecteurs d'un plan sont liés, avec pour coefficients les mineurs de rang~$2$, et se vérifie coordonnée par coordonnée : pour la première, les six termes de $(v_0 w_1 - v_1 w_0) u_0 + (w_0 u_1 - w_1 u_0) v_0 + (u_0 v_1 - u_1 v_0) w_0$ s'annulent deux à deux. Si les trois produits extérieurs valent un même $d$, l'identité devient $d\,(u + v + w) = 0$, et $d = u \wedge v$ est une unité puisque $x$ et $y$ sont disjointes, d'où $u + v + w = 0$. Réciproquement, si $w = -(u + v)$, alors $v \wedge w = -\,v \wedge u = u \wedge v$ et $w \wedge u = -\,v \wedge u = u \wedge v$. \end{proof} \begin{remarque} L'énoncé tient sous une hypothèse plus faible que celle de la page : $w$ n'a pas besoin d'engendrer une droite, et seule sert l'inversibilité de $u \wedge v$. Celle-ci ne peut être omise. Sur $\mathbf Z$, avec $u = v = w = (1, 0)$, les trois produits extérieurs sont nuls, donc égaux, alors que $u + v + w = (3, 0)$. La conséquence que la page ajoute se lit sur les égalités : si $u + v + w = 0$, alors $v \wedge w$ et $w \wedge u$ sont égaux à $u \wedge v$, donc inversibles, et $z$ est disjointe de $y$ et de $x$. Elle n'est pas vérifiée en Lean. \end{remarque} \noindent La preuve vérifiée travaille dans $R^2$, pour un anneau commutatif $R$ quelconque, avec le produit extérieur $u_0 v_1 - u_1 v_0$ (\texttt{wedge}) ; c'est le cas général, puisque $V$ est libre de rang~$2$. Elle établit l'identité de Cramer coordonnée par coordonnée (\texttt{cramer}), puis l'équivalence sous la seule hypothèse que $u \wedge v$ est une unité (\texttt{fundamental\_relation}). Les noms sont ceux de \href{\leanblobmain/Folder89.lean}{\texttt{Folder89.\allowbreak{}lean}}. Ne sont pas démontrés ici : la disjonction de $z$ que la page ajoute ; la reconstruction de $V$, sur un corps, à partir de l'ensemble de ses droites, des torseurs $T_x$, du torseur des générateurs de $\det V$, de la relation de disjonction et des isomorphismes de $T_x \wedge T_y$ sur ce dernier torseur (page~17), avec la seule propriété de ces données que la page~18 écrit ; les hexagones et les ensembles 3-3 des pages~2 à~8, leur groupe d'automorphismes d'ordre~$36$ ; les plans sur $\mathbf F_3$ des pages~9 à~14 ; les polygones combinatoires des pages~19 et~20. \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 11 à 16, polarisations hodgiennes\piste{10-hodgian-polarisations-torsor}]\nonverifie Soient $G$ un groupe algébrique réel muni d'homomorphismes $\mathbb G_m \xrightarrow{i} G \xrightarrow{\varepsilon} \mathbb G_m$, $\eta = i(-1)$ et $G' = \mathrm{Ker}\,\varepsilon$. Deux éléments $C, C'$ de $G'(\mathbb R)$ de carré $\eta$ qui définissent des polarisations de $\mathrm{Rep}(G)$ sont, après conjugaison par $G'(\mathbb R)^\circ$, liés par $C' = zC$ avec $z$ central d'ordre divisant~$2$, et $z \neq 1$ donne une autre polarisation : les polarisations hodgiennes forment un torseur sous un groupe d'éléments centraux de $2$-torsion. Sur toute $\otimes$-catégorie graduée sur $K \subset \mathbb R$, les $\otimes$-automorphismes $z$ de l'identité tels que $z^2 = 1$, triviaux sur $K(1)$, opèrent librement sur les polarisations. \end{theoreme*} \end{encadre} {\small Les feuillets en esquissent une démonstration incomplète (pages 15 et 16). La conjugaison de la page~15 tient en trois lignes abrégées où quatre mots sont illisibles, et le groupe qui opère, la $2$-torsion de $Z \cap G'$, est le choix de l'édition. Mathlib n'a pas les catégories tannakiennes ni leurs polarisations. On se reportera aux notes de Grothendieck (\lot{10}{1}{11}).\par} \begin{encadre} \begin{theoreme*}[Grothendieck, pages 62 à 65, caractère numérique et tore de rang un\piste{10-numerical-character-rank-one-torus}]\nonverifie Une catégorie tannakienne sur un corps $k$ dont le lien est un tore de dimension~$1$ est déterminée à équivalence près par son caractère numérique : l'ensemble des classes d'objets simples, les constantes de structure de $K(\mathcal M)$, les centres $Z_\sigma$ des algèbres d'endomorphismes avec leurs classes de Brauer, et le rang. Pour le tore $G$ des éléments de norme~$1$ d'une extension quadratique $Z/k$, l'application $H^2(k, G) \to H^2(k, R_{Z/k}\mathbb G_m) = \mathrm{Br}(Z)$ est en effet injective, par Hilbert~90. \end{theoreme*} \end{encadre} {\small La page passe par \q{on vérifie aussitôt} l'équivalence entre le caractère numérique et les données $(G, u_\sigma(\xi))$. Mathlib n'a pas les catégories tannakiennes ni leurs gerbes. On se reportera aux notes de Grothendieck (\lot{10}{4}{62}).\par} \begin{encadre} \begin{theoreme*}[Grothendieck, pages 10 à 12, groupe de Picard de l'espace de Grothendieck--Springer\piste{123-grothendieck-springer-pic-twisted-torus}]\nonverifie Soient $S$ un schéma normal intègre, $G$ un $S$-schéma en groupes réductif dont le tore maximal abstrait $T$ n'est pas déployé, et $\Gamma$ l'image de $\pi_1(S)$ dans $\mathrm{Aut}\,X^*(T)$. L'application $\mathrm{Pic}(\mathrm{Bor}) \to \mathrm{Pic}(\tilde G)$ est injective, de conoyau contenu dans $H^1(\Gamma, X^*(T))$, et bijective quand ce $H^1$ est nul. Un fibré en droites sur $\mathrm{Bor}$ est ample si et seulement si son image réciproque sur $\tilde G$ l'est, sans hypothèse de normalité sur~$S$. \end{theoreme*} \end{encadre} {\small La condition $H^1(\Gamma, X^*(T)) = 0$ vient d'une marge et de la page~12, lues avec plusieurs mots incertains ou illisibles ; la réciproque pour $S$ régulier, que la marge annonce, n'est pas reprise ici. Mathlib n'a pas les schémas en groupes réductifs ni leurs schémas de Borel. On se reportera aux notes de Grothendieck (\lot{123}{1}{10}).\par} \begin{encadre} \begin{theoreme*}[Grothendieck, pages 21, 28, 30 et 34, rigidifications de Kostant\piste{123-kostant-rigidifications-count}]\nonverifie Soient $G$ un groupe simple adjoint de nombre de Coxeter $h$ premier à la caractéristique, et $z$ l'ordre du groupe $\mathfrak z$ tel que $N(T) \cap N(T')$ soit extension de $(\mathbf Z/h)^*$ par $\mathbf Z/h \times \mathfrak z$. Le groupe $G$ opère librement sur les quadruplets $(T, B, T', B')$ formés de tores maximaux $T, T'$ en apposition au sens de Kostant et de sous-groupes de Borel $B \supset T$, $B' \supset T'$. Le quotient est fini étale de rang $\mathrm{card}(W)^2/(h\,z\,\varphi(h))$, et de rang $\mathrm{card}(W)^2/(h\,z)$ quand on se donne aussi un générateur de $T \cap N(T') \simeq \mu_h$. \end{theoreme*} \end{encadre} {\small La lettre à Kostant du 22~octobre~1969 (page~21) et la page~34 donnent ce compte sans démonstration. L'édition le déduit de la théorie de Kostant et de Springer \cite{kostant1959,springer1974}, par un argument que Lean ne vérifie pas. Soit $x = \rho^\vee(e^{2i\pi/h})$ l'élément principal de $T$ ; un $t \in T$ qui normalise $T'$ envoie l'élément cyclique $E'$ sur un multiple de lui-même, d'où $\alpha_i(t) = \theta(t)^{-1} = \lambda$ avec $\lambda^h = 1$, et $T \cap N(T') = \langle x \rangle$. L'image de $N(T) \cap N(T')$ dans $W$ est formée des $w$ tels que $w(x) \in \langle x \rangle$ : le stabilisateur de $x$ est le groupe $\Omega \simeq P^\vee/Q^\vee$, d'ordre $z$, car le centralisateur de $x$ dans le groupe adjoint n'est pas connexe, et $x$ n'est conjugué à $x^k$ que pour $k$ premier à $h$ ; chacun de ces $w$ se relève, par la conjugaison des sous-espaces de Cartan des $\mathfrak g^{\zeta^j}$ sous $Z_G(x)^\circ = T$. D'où l'ordre $h\,z\,\varphi(h)$, et le compte, puisque le stabilisateur d'un quadruplet est $T \cap T' = 1$. Un comptage par ordinateur sur $\mathbf F_q$ donne 2, 4 et 12 orbites pour $A_2$, $B_2$ et $G_2$. Reste la question que la lettre pose à Kostant : $B$ et $B'$ sont-ils toujours en position générale ? C'est vrai pour $A_2$, où les vecteurs propres de $E'$ sont les vecteurs de Fourier. Mathlib n'a pas les tores maximaux ni les sous-groupes de Borel des groupes algébriques. On se reportera aux notes de Grothendieck (\lot{123}{2}{21}).\par} \begin{encadre} \begin{enonce}[Le nombre annoncé aux pages 21 et 34, en petit rang, vérification de l'édition]\verifie[\leanblobmain]{Folder123Kostant} Soient $W$ le groupe de Weyl d'un type simple, $h$ son nombre de Coxeter et $z$ l'ordre du centre du groupe simplement connexe. Pour les types $A_1$ à $A_8$, $B_2$ à $B_8$, $C_3$ à $C_8$, $D_4$ à $D_8$, $E_6$, $E_7$, $E_8$, $F_4$ et $G_2$, l'entier $h\,z\,\varphi(h)$ divise $\mathrm{card}(W)^2$. Le quotient vaut $1$, $2$, $4$ et $12$ pour $A_1$, $A_2$, $B_2$ et $G_2$. \end{enonce} \end{encadre} {\small \emph{Démonstration.} Les données sont les valeurs classiques : $\bigl((n+1)!,\, n+1,\, n+1\bigr)$ pour $(\mathrm{card}\,W, h, z)$ en type $A_n$, $(2^n n!,\, 2n,\, 2)$ en types $B_n$ et $C_n$, $(2^{n-1} n!,\, 2n - 2,\, 4)$ en type $D_n$, et $(51\,840, 12, 3)$, $(2\,903\,040, 18, 2)$, $(696\,729\,600, 30, 1)$, $(1152, 12, 1)$, $(12, 6, 1)$ pour $E_6$, $E_7$, $E_8$, $F_4$, $G_2$. Pour $A_2$, par exemple, $36/(3 \cdot 3 \cdot \varphi(3)) = 36/18 = 2$, et pour $G_2$, $144/(6 \cdot 1 \cdot 2) = 12$. Lean décide que chaque reste est nul (\texttt{integral\_A}, \texttt{integral\_B}, \texttt{integral\_C}, \texttt{integral\_D}, \texttt{integral\_exceptional}) et calcule les quatre valeurs (\texttt{small\_cases}). Les données sont entrées à la main et ne sont pas tirées des systèmes de racines. L'intégralité est une condition nécessaire pour que le nombre soit un nombre d'orbites, et les valeurs pour $A_2$, $B_2$ et $G_2$ sont celles du comptage sur $\mathbf F_q$ rappelé plus haut. Lean ne vérifie ni l'action libre de $G$ sur les quadruplets, ni le compte lui-même, et l'encadré précédent reste non vérifié. Les noms sont ceux de \href{\leanblobmain/Folder123Kostant.lean}{\texttt{Folder123Kostant.\allowbreak{}lean}}.\par} \begin{encadre} \begin{theoreme*}[Grothendieck, pages 10 à 13, pas de résolution de Steinberg sans changement de base\piste{123-steinberg-no-resolution-picard}]\nonverifie Sur une base $S$, il n'existe pas de résolution du morphisme de Steinberg $G \to T/W$ qui soit un isomorphisme au-dessus de $G^{\mathrm{reg}}$ et dont le lieu exceptionnel soit de codimension $\geq 2$ fibre par fibre : son groupe de Picard serait fini modulo $\mathrm{Pic}(S)$, alors que celui de l'espace de Grothendieck--Springer $\tilde G$ contient le réseau des poids et son cône ample. Le changement de base $T \to T/W$ est ainsi rendu nécessaire par une comparaison de groupes de Picard, et non par la monodromie. \end{theoreme*} \end{encadre} {\small Les feuillets en esquissent une démonstration incomplète (pages 10 à 13). La phrase de conclusion s'interrompt, et l'argument demande une résolution régulière et projective sur $G$, hypothèses que la page ne formule pas. Mathlib n'a pas les schémas en groupes réductifs ni leurs groupes de Picard. On se reportera aux notes de Grothendieck (\lot{123}{1}{10}).\par} \begin{encadre} \begin{theoreme*}[Grothendieck, pages 71 à 77, catégorie de Picard de Brandt\piste{15-brandt-picard-category}]\nonverifie Soit $C$ une catégorie de Deuring sur un anneau de Dedekind, équivalente à celle des modules inversibles sur un ordre $\mathfrak o$ d'une algèbre $E$ dont tous les automorphismes sont intérieurs et dont les bimodules inversibles contenus dans $E$ commutent entre eux. Le $2$-groupe $\mathrm{Eqv}(C)$ des autoéquivalences porte une structure symétrique strictement commutative, indépendante de l'objet choisi pour l'identifier aux bimodules. Les catégories de Deuring d'un même type sont donc des catégories-torseurs sous une même catégorie de Picard stricte, la catégorie de Picard de Brandt. \end{theoreme*} \end{encadre} {\small C'est l'édition qui affirme, d'après Auslander--Goldman et Reiner, que la condition de commutation vaut pour les ordres maximaux. Mathlib n'a pas les catégories de Picard ni les catégories-torseurs. On se reportera aux notes de Grothendieck (\lot{15}{4}{71}).\par} \begin{encadre} \begin{theoreme*}[Grothendieck, pages 116 à 118, foncteurs fibres réels\piste{15-real-fibre-functor-criterion}]\nonverifie Soit une catégorie motivique sur $\mathbf Q$ de lien commutatif $G$, de caractère de Tate $\varepsilon$ et de cocaractère des poids $j$ avec $\varepsilon j(\lambda) = \lambda^2$, et soit $U = \mathrm{Ker}(\varepsilon|_{G^\circ})$, où $U^\circ$ est un tore compact. La catégorie admet un foncteur fibre à valeurs dans les espaces vectoriels réels si et seulement si $U$ est connexe ; sinon $U \simeq U^\circ \times \mu_2$. Sa sous-catégorie de poids pairs, de groupe $G/j(\mu_2)$, en admet donc toujours un. \end{theoreme*} \end{encadre} {\small Les feuillets en esquissent une démonstration incomplète (page 116). La condition intermédiaire~(ii) des deux propositions est en partie illisible, l'édition la rétablit, et l'implication qui y passe est la sienne. Mathlib n'a pas les catégories tannakiennes ni les foncteurs fibres. On se reportera aux notes de Grothendieck (\lot{15}{6}{116}).\par} \begin{encadre} \begin{theoreme*}[Grothendieck, pages 27 à 36, semi-continuité des rangs\piste{27-semicontinuity-proof}]\nonverifie Pour un schéma en groupes lisse, séparé et de présentation finie sur une base quelconque, la dimension de la partie affine et les rangs nilpotent, affine-nilpotent et unipotent sont semi-continus supérieurement ; le rang abélien, le rang abélien plus réductif et le rang semi-simple sont semi-continus inférieurement. \end{theoreme*} \end{encadre} {\small SGA~3, X~8.7, énonce ces inégalités sans démonstration. La réduction à un trait suppose les invariants localement constructibles, propriété que ni la page ni la lecture ne vérifient, et l'équivalence entre les inégalités (3) et (9) que la page affirme n'est pas justifiée. Mathlib n'a pas les schémas en groupes lisses ni leur décomposition de Chevalley. On se reportera aux notes de Grothendieck (\lot{27}{2}{27}).\par} \begin{encadre} \begin{theoreme*}[Grothendieck, pages 10 à 14, liens sur un corps de Tsen\piste{45-bands-tsen-field}]\nonverifie Sur un corps $C_1$, tout lien algébrique, lisse ou non, provient d'un $k$-schéma en groupes, et $H^2(k, L)$ se réduit alors à sa classe neutre. \end{theoreme*} \end{encadre} {\small Les feuillets en esquissent une démonstration incomplète (pages 11 à 14), par deux principes de réduction pour les gerbes de réalisations. Le deuxième cas suppose une conjugaison des sous-groupes de Cartan infinitésimaux qui n'est pas établie, et le troisième n'est pas lu. Mathlib n'a pas les liens ni la cohomologie non abélienne de degré~$2$. On se reportera aux notes de Grothendieck (\lot{45}{1}{10}).\par} \begin{encadre} \begin{theoreme*}[D'après les pages 3 à 10, forme corrigée par l'édition, surjectivité en $H^1$ en dimension un\piste{45-h1-surjectivity-dim-one}]\nonverifie Soit $k$ un corps tel que $\mathrm{Br}(k') = 0$ pour toute extension finie séparable $k'/k$. Pour tout épimorphisme $G \to G'$ de schémas en groupes algébriques sur $k$, non nécessairement lisses ni linéaires, à noyau non nécessairement commutatif, l'application $H^1(k, G) \to H^1(k, G')$ de cohomologie plate est surjective. \end{theoreme*} \end{encadre} {\small La page suppose $\mathrm{cd}(k) \leq 1$ ; l'hypothèse sur les groupes de Brauer, la dimension $\leq 1$ au sens de Serre, est de l'édition. Les feuillets en esquissent une démonstration incomplète (pages 3 à 9). Le lemme~4 invoque une conjugaison des sous-algèbres de Cartan qui n'est pas établie et qui tombe en défaut en général en caractéristique~$p$, et l'énoncé de la page~9 conclut que $H^1(k,G) \to H^1(k,G')$ est un épimorphisme pour tout épimorphisme $G \to G'$ de groupes algébriques sur~$k$. Mathlib n'a pas la cohomologie plate des schémas en groupes. On se reportera aux notes de Grothendieck (\lot{45}{1}{3}).\par} \begin{encadre} \begin{theoreme*}[Grothendieck, page 13, principe d'identité et lemme~B\piste{55-lemma-b-identity-principle}]\nonverifie Soit $X$ un espace annelé quasi-compact, de faisceau structural cohérent et d'anneaux locaux noethériens, qui vérifie un principe d'identité : pour tout Idéal cohérent $J$ et tout point $y$ de $Y = \mathrm{Supp}(\mathcal O/J)$ où $\mathcal O_{Y,y}$ est intègre, il existe un voisinage ouvert $U$ de $y$ dans $Y$ sur lequel toute section nulle près de $y$ est nulle. Alors toute suite croissante de sous-faisceaux cohérents d'un faisceau cohérent est stationnaire, et $\Gamma(X, \mathcal O_X)$ est noethérien. \end{theoreme*} \end{encadre} {\small La page énonce le lemme~B et son corollaire sans démonstration, et propose les polycylindres analytiques compacts comme cas d'application ; le passage au corollaire par le lemme~A est de la lecture. Mathlib n'a pas les faisceaux cohérents sur un espace annelé, et le pas central, celui où sert le principe d'identité, n'est pas vérifié en Lean ; l'édition ne vérifie pas non plus que les conditions de la page suffisent sur un espace annelé quelconque. Lean vérifie ce qui entoure ce pas, énoncé ci-dessous. On se reportera aux notes de Grothendieck (\lot{55}{1}{13}).\par} \begin{encadre} \begin{theoreme*}[D'après la page 13, forme réduite par l'édition, le lemme~B moins le principe d'identité\piste{55-lemma-b-identity-principle}]\verifie{Folder55} Soient $X$ un espace quasi-compact et $(S_k)_{k \in \mathbf N}$ une suite croissante de sous-faisceaux d'un préfaisceau d'ensembles sur $X$. On suppose qu'en chaque point $x$ les germes des $S_k$ se stabilisent, et que cette stabilisation se propage uniformément : pour tout $x$ et tout $k$, il existe un voisinage ouvert $W$ de $x$ tel que tout $S_l$, $l \geq k$, qui a en $x$ les mêmes germes que $S_k$, coïncide avec $S_k$ sur $W$. Alors la suite $(S_k)$ est stationnaire. Sans l'hypothèse d'uniformité, la conclusion tombe en défaut. Enfin, si les idéaux de type fini $I$ d'un anneau $A$ s'envoient de façon croissante sur des objets $\widetilde I$ d'une classe où toute suite croissante est stationnaire, avec $\Gamma(\widetilde I) = I$, alors $A$ est noethérien. \end{theoreme*} \end{encadre} {\small \emph{Démonstration.} Un sous-faisceau est ici une famille d'ensembles de sections, stable par restriction et locale : une section y appartient dès qu'elle y appartient localement. En chaque point $x$, on prend l'indice $k_x$ où les germes se stabilisent, puis le voisinage $W_x$ que donne l'uniformité pour $k_x$ : sur $W_x$, tous les $S_l$, $l \geq k_x$, coïncident avec $S_{k_x}$. Par quasi-compacité, un nombre fini de $W_x$ recouvrent $X$ ; soit $K$ le plus grand des $k_x$ correspondants. Pour $l \geq K$, une section de $S_l$ sur un ouvert $U$ appartient, sur chaque $U \cap W_x$, à $S_l = S_{k_x} \subset S_K$, donc à $S_K$ par localité : la suite est stationnaire à partir de $K$. La stabilisation des germes est ce que donne l'hypothèse~(iv) : la fibre d'un faisceau cohérent est un module de type fini sur l'anneau noethérien $\mathcal O_{X,x}$, où toute suite croissante de sous-modules est stationnaire. Pour le contre-exemple, on prend le compactifié d'Alexandrov $\mathbf N \cup \{\infty\}$, le faisceau de toutes les fonctions à valeurs dans $\{0, 1\}$, et pour $S_k$ les fonctions qui ne valent $1$ qu'aux points $0, \ldots, k-1$. En un entier $n$, les germes sont constants à partir de $k = n + 1$ ; en $\infty$, une section de $S_k$ est nulle sur le voisinage ouvert obtenu en retirant les points $0, \ldots, k-1$, et les germes sont tous ceux de $S_0$. Pourtant la fonction indicatrice de $\{k\}$ est dans $S_{k+1}$ et pas dans $S_k$ : les sous-faisceaux s'accumulent en $\infty$, ce que le principe d'identité est là pour interdire. Pour le corollaire, une suite croissante d'idéaux de type fini $I_k$ donne la suite croissante des $\widetilde{I_k}$, stationnaire, et $I_k = \Gamma(\widetilde{I_k})$ l'est aussi ; la condition des chaînes ascendantes sur les idéaux de type fini suffit à rendre $A$ noethérien. Les noms sont \texttt{stationary\_of\_locally\_stationary} (le pas de quasi-compacité), \texttt{stationary\_of\_germs} (le lemme~B sous l'hypothèse d'uniformité), \texttt{germs\_stabilize\_of\_noetherian} (le rôle de (iv)), \texttt{not\_stationary\_without\_uniformity} (le contre-exemple) et \texttt{isNoetherianRing\_of\_tilde} (le corollaire), dans \href{\leanblob/Folder55.lean}{\texttt{Folder55.\allowbreak{}lean}}. Ne sont pas démontrés : que le principe d'identité~(v) entraîne l'hypothèse d'uniformité, ce qui demanderait les faisceaux cohérents, les supports des $\mathcal O/\mathcal J$ et une décomposition primaire dans les fibres, et que le lemme~A fournisse $I \mapsto \widetilde I$ avec $\Gamma(\widetilde I) = I$. Le principe~(v) ne parle que des sections sur un voisinage $U$ fixé, pas sur les ouverts plus petits où vivent les sous-faisceaux qui s'accumulent ; l'édition ne sait pas s'il suffit sur un espace annelé quelconque.\par}