\section[Cote 93 : la différence schwarzienne en dérivées divisées]{Cote 93 : la différence schwarzienne en dérivées divisées\protect\verifie{Folder93}}\label{sec:93}

La cote 93, du groupe \q{Géométrie et topologie combinatoire}, étudie la dérivée schwarzienne et les connexions projectives sur une courbe lisse $X$ au-dessus d'une base $S$. Pour deux uniformisantes $t$, $s$, la lecture note $G(t,s) = \bigl(-2\,s'''/s' + 3\,(s''/s')^2\bigr)\,dt^2$. Page~72, la page remplace les dérivées par les opérateurs $D^{(i)}_t = \frac{1}{i!}\frac{d^i}{dt^i}$ sur une base variable, les dérivées de Hasse (Hasse et Schmidt, 1937 \cite{hasseschmidt1937}), observe que les coefficients $2$ et $3$ de $G$ l'interdisent, et prend $G_0 = \frac{1}{12}G$ ; elle fixe le signe par la valeur test $G_0(t, t^3) = \frac{2}{3t^2}\,dt^2$, après un premier essai sur $G_0(t, t^2)$ (\lot{93}{4}{72}). Pages~115 à~117, la mise au net énonce l'invariance par les homographies~(1) et la relation de cocycle~(2) (\lot{93}{6}{115}). Page~120, elle écrit $G(t,s) = 12\,G_0(t,s)$ avec $G_0(t,s) = -D^{(3)}_t s/D^{(1)}_t s + (D^{(2)}_t s/D^{(1)}_t s)^2$ (\lot{93}{6}{120}). Une marge de la page~121, marquée \q{OK}, dit que les fonctions annulées par $D^{(1)}$, $D^{(2)}$, $D^{(3)}$ forment $\mathcal O^{(p)}$ si $p \neq 2, 3$ et $\mathcal O^{(p^2)}$ sinon ; la Proposition des pages~121 à~123 en tire la rigidité locale (\lot{93}{7}{121}, \lot{93}{7}{123}). On démontre ici le noyau algébrique de ces pages dans le modèle local $R[X]$, sur un anneau commutatif quelconque : la formule $G = 12\,G_0$, la relation de cocycle, l'invariance par les homographies, les deux valeurs tests, la description de la marge de la page~121, le fait qu'en caractéristique $2$ et $3$ une translation par une puissance $p$-ième change $G_0$, et la rigidité de la Proposition des pages~121 à~123 dans l'anneau tronqué $A[T]/(T^n)$, c'est-à-dire pour $\alpha = 0$.

Le titre d'inventaire du dossier est \emph{Connexions de Gauss-Manin et équations de Picard-Fuchs. Opération de Cartier}, et la cote ouvre ici l'axe des connexions, de la $p$-courbure et de la monodromie. Une connexion $\nabla$ sur un fibré $E$ est une règle pour dériver ses sections le long d'un champ de vecteurs~$D$. Sur les nombres complexes, elle est à courbure nulle quand $E$ admet localement une base de sections de dérivée nulle ; prolongées le long d'un lacet, ces sections reviennent transformées, et cette transformation est la monodromie. Sur une famille de variétés, la cohomologie des fibres porte une connexion canonique, celle de Gauss--Manin : les pages~161 à~166 la construisent d'après Katz et Oda (1968) \cite{katzoda1968}, et les pages~218 à~220 en tracent un plan. En caractéristique $p$, le composé de $D$ avec lui-même $p$ fois est encore une dérivation, notée $D^{[p]}$, et la $p$-courbure mesure l'écart entre $\nabla(D)^p$ et $\nabla(D^{[p]})$. La page~188 énonce que les connexions de courbure et de $p$-courbure nulles sont celles qui proviennent d'un module sur le quotient de Frobenius~$X'$ : c'est la descente de Cartier, sous la forme que lui donne Katz (1970) \cite{katz1970}, §5. Les pages~193 et~194 demandent si une connexion définie sur les entiers, de $p$-courbure nulle pour presque tout~$p$, a une monodromie finie ; c'est la conjecture de Grothendieck--Katz, démontrée par Katz (1972) \cite{katz1972} pour les connexions de Gauss--Manin et ouverte en général. La descente de Cartier n'est formalisée que sur le fibré trivial, quand l'anneau a une coordonnée ; la remarque des pages~193 et~194 l'est en rang un, avec la formule de Jacobson qui calcule la $p$-courbure, puis, à titre d'illustration, sur le fibré trivial de rang quelconque, avec trois exemples calculés en rang deux ; la conjecture est énoncée plus bas. Les autres énoncés démontrés portent sur les connexions projectives d'une courbe : une connexion projective désigne les coordonnées locales qui se déduisent les unes des autres par des homographies, et la différence schwarzienne $G(t, s)$ mesure l'écart entre les structures définies par $t$ et par~$s$. S'y ajoute le morphisme dérivé des pages~233 à~235, qui compare les complexes de De~Rham de deux relèvements.

Le même axe traverse trois cotes sans section propre. La cote~162-5 (partie \q{Catégories et foncteurs}) place les connexions intégrables et les groupes formels dans le cadre des catégories formelles, et y compare un complexe de De~Rham à un complexe de Hochschild dans la catégorie dérivée. La cote~60 (partie \q{Cohomologie étale et $\ell$-adique}) lit la monodromie locale d'un faisceau $\ell$-adique sur une courbe dans sa représentation de Weil--Deligne. La cote~34 (partie \q{Groupes fondamentaux et théorie de Galois}) décrit la monodromie modérée d'une famille dégénérée en caractéristique résiduelle~$p$, sur une base de dimension quelconque.

\noindent\emph{Conventions.} $R$ est un anneau commutatif et $X$ joue le rôle de l'uniformisante $t$. Pour $f \in R[X]$, $D^{(k)} f$ est la dérivée de Hasse, définie sans division par $k!$ par $D^{(k)} X^n = \binom nk X^{n-k}$ ; on a $k!\,D^{(k)} f = f^{(k)}$. On pose
\[
N(f) = (D^{(2)} f)^2 - D^{(3)} f \cdot D^{(1)} f, \qquad G_0(f) = N(f)\,(D^{(1)} f)^{-2},
\]
où l'inverse est pris quand $D^{(1)} f$ est inversible (Lean utilise \texttt{Ring.\allowbreak{}inverse}, qui vaut $0$ sinon). Ainsi $G_0(f)$ est le coefficient de $dt^2$ dans $G_0(t, f)$, et $N(f)$ est ce coefficient débarrassé de son dénominateur. On note de même $N_{\mathrm{cl}}(f) = 3\,(f'')^2 - 2\,f''' f'$ et $G(f) = N_{\mathrm{cl}}(f)\,(f')^{-2}$. Pour $s, u \in R[X]$, $s \circ u$ est le polynôme composé. On dit que $f$ est \emph{tué} si $D^{(1)} f = D^{(2)} f = D^{(3)} f = 0$. On note $f_i$ le coefficient de $X^i$ dans $f$.

\begin{enonce}[Page 120, le facteur $12$\piste{93-integral-schwarzian-level-p2}]
Pour tout $f \in R[X]$, $N_{\mathrm{cl}}(f) = 12\,N(f)$ et $G(f) = 12\,G_0(f)$.
\end{enonce}

\begin{proof}
On a $f' = D^{(1)} f$, $f'' = 2\,D^{(2)} f$ et $f''' = 6\,D^{(3)} f$ (par un lemme de mathlib sur les dérivées de Hasse). Donc $3\,(f'')^2 - 2\,f''' f' = 12\,(D^{(2)} f)^2 - 12\,D^{(3)} f\,D^{(1)} f$. La seconde égalité s'en déduit en multipliant par $(f')^{-2}$.
\end{proof}

\begin{lemme}\label{lem:93-chaine}
Pour $s, u \in R[X]$, en notant $s_i = (D^{(i)} s) \circ u$ et $u_i = D^{(i)} u$ :
\[
D^{(1)}(s \circ u) = s_1 u_1, \quad
D^{(2)}(s \circ u) = s_1 u_2 + s_2 u_1^2, \quad
D^{(3)}(s \circ u) = s_1 u_3 + 2\,s_2 u_1 u_2 + s_3 u_1^3 .
\]
\end{lemme}

\begin{proof}
Les trois identités sont additives en $s$ et valent pour $s$ constant. On les démontre ensemble par récurrence sur les monômes, en passant de $s$ à $Xs$. On a $(Xs) \circ u = u \cdot (s \circ u)$, et la formule de Leibniz $D^{(k)}(fg) = \sum_{i+j=k} D^{(i)} f\, D^{(j)} g$ donne, avec $D^{(1)}X = 1$ et $D^{(2)}X = D^{(3)}X = 0$, $D^{(1)}(Xs) = s + X D^{(1)}s$, $D^{(2)}(Xs) = D^{(1)}s + X D^{(2)}s$, $D^{(3)}(Xs) = D^{(2)}s + X D^{(3)}s$. On développe les deux membres par Leibniz et l'hypothèse de récurrence ; ils coïncident comme polynômes en $u$, les $u_i$, $s \circ u$ et les $s_i$.
\end{proof}

\begin{enonce}[Pages 115 à 117, la relation de cocycle\piste{93-integral-schwarzian-level-p2}]
Pour $s, u \in R[X]$ :
\begin{enumerate}
\item $N(s \circ u) = N(s) \circ u \cdot (D^{(1)} u)^4 + \bigl((D^{(1)} s) \circ u\bigr)^2 N(u)$, sans hypothèse ;
\item si $D^{(1)} s$ et $D^{(1)} u$ sont inversibles, $G_0(s \circ u) = G_0(s) \circ u \cdot (D^{(1)} u)^2 + G_0(u)$.
\end{enumerate}
De plus $N(X) = 0$, donc $G_0(X) = 0$.
\end{enonce}

\begin{proof}
(1) On reporte les formules du lemme~\ref{lem:93-chaine} dans $N(s \circ u)$. Avec les notations du lemme,
\[
(s_1 u_2 + s_2 u_1^2)^2 - (s_1 u_3 + 2 s_2 u_1 u_2 + s_3 u_1^3)\, s_1 u_1 = u_1^4 (s_2^2 - s_3 s_1) + s_1^2 (u_2^2 - u_3 u_1),
\]
les termes croisés $\pm 2 s_1 s_2 u_1^2 u_2$ se compensant. (2) On a $D^{(1)}(s \circ u) = s_1 u_1$ ; $s_1$ est inversible comme image de l'inversible $D^{(1)} s$ par l'homomorphisme $f \mapsto f \circ u$, qui envoie l'inverse de $(D^{(1)} s)^2$ sur l'inverse de $s_1^2$. On divise~(1) par $(s_1 u_1)^2$.
\end{proof}

\begin{remarque}
Là où $6$ est inversible, la relation de cocycle et l'invariance par les homographies sont les propriétés classiques de la dérivée schwarzienne, qui porte le nom de H.~A.~Schwarz. Dans~(2), $G_0(s) \circ u \cdot (D^{(1)} u)^2$ est le coefficient de $dt^2$ dans $G_0(u, s \circ u)$, puisque $du = D^{(1)}u\,dt$ ; l'énoncé est donc la relation $G_0(t, r) = G_0(t, u) + G_0(u, r)$ pour $r = s \circ u$. La forme~(1) n'utilise aucune hypothèse d'inversibilité : la relation de cocycle est une identité entre polynômes des coefficients, valable sur $\mathbf Z$ et donc sur toute base, en caractéristique~$2$ et~$3$ comprises. L'inversibilité ne sert qu'à diviser.
\end{remarque}

\begin{enonce}[Page 115, invariance par les homographies\piste{93-integral-schwarzian-level-p2}]
Soient $s, p, q \in R[X]$ avec $s\,q = p$ et $D^{(2)} p = D^{(3)} p = D^{(2)} q = D^{(3)} q = 0$. Alors $q^2 N(s) = 0$. En particulier, si $a, b, c, d \in R[X]$ sont tués, si $cX + d$ est inversible et si $s\,(cX + d) = aX + b$, alors $G_0(s) = 0$ ; c'est le cas pour $a, b, c, d \in R$.
\end{enonce}

\begin{proof}
On applique $D^{(2)}$ et $D^{(3)}$ à $s\,q = p$ par Leibniz : $D^{(2)}s\,q + D^{(1)}s\,D^{(1)}q = 0$ et $D^{(3)}s\,q + D^{(2)}s\,D^{(1)}q = 0$. Alors
\[
q^2 N(s) = D^{(2)}s\,q\,\bigl(D^{(2)}s\,q + D^{(1)}s\,D^{(1)}q\bigr) - D^{(1)}s\,q\,\bigl(D^{(3)}s\,q + D^{(2)}s\,D^{(1)}q\bigr) = 0 .
\]
Si $a$ est tué, Leibniz donne $D^{(2)}(aX) = D^{(1)}a = 0$ et $D^{(3)}(aX) = D^{(2)}a = 0$ ; les hypothèses valent donc pour $p = aX + b$ et $q = cX + d$. Si $q$ est inversible, $N(s) = 0$, d'où $G_0(s) = 0$. Les constantes sont tuées.
\end{proof}

\begin{enonce}[Page 72, les valeurs tests]
Dans $R[X]$, $N(X^2) = 1$ et $D^{(1)}(X^2) = 2X$ ; $N(X^3) = 6X^2$ et $D^{(1)}(X^3) = 3X^2$. Donc $G_0(t, t^2) = \frac{1}{4t^2}\,dt^2$ là où $2$ est inversible, et $G_0(t, t^3) = \frac{2}{3t^2}\,dt^2$ là où $3$ est inversible.
\end{enonce}

\begin{proof}
$D^{(k)} X^n = \binom nk X^{n-k}$. Pour $X^2$ : $D^{(2)} = 1$, $D^{(3)} = 0$. Pour $X^3$ : $D^{(1)} = 3X^2$, $D^{(2)} = 3X$, $D^{(3)} = 1$, et $9X^2 - 3X^2 = 6X^2$.
\end{proof}

\begin{enonce}[Marge de la page 121, les fonctions tuées\piste{93-integral-schwarzian-level-p2}]
Soit $R$ de caractéristique $p$ première.
\begin{enumerate}
\item $f \in R[X]$ est tué si et seulement si, pour tout $n$ tel que le coefficient de $X^n$ dans $f$ soit non nul, $p$ divise $n$ si $p > 3$, $4$ divise $n$ si $p = 2$, $9$ divise $n$ si $p = 3$.
\item Si $u$ est tué, tout polynôme $f \circ u$ est tué ; c'est le cas des polynômes en $X^p$ ($p > 3$), en $X^4$ ($p = 2$), en $X^9$ ($p = 3$).
\item Si $p = 2$, $D^{(1)}(X^2) = 0$, $D^{(1)}(X + X^2) = 1$ et $G_0(X + X^2) = 1$.
\item Si $p = 3$, $D^{(1)}(X^3) = D^{(2)}(X^3) = 0$, $D^{(3)}(X^3) = 1$, $D^{(1)}(X + X^3) = 1$ et $G_0(X + X^3) = -1$.
\end{enumerate}
\end{enonce}

\begin{proof}
(1) Le coefficient de $X^n$ dans $D^{(k)} f$ est $\binom{n+k}{k}$ fois celui de $X^{n+k}$ dans $f$ ; donc $D^{(k)} f = 0$ si et seulement si $\binom nk a_n = 0$ pour tout $n$, où $a_n$ est le coefficient de $X^n$. Dans un anneau de caractéristique $p$, un entier $c$ non divisible par $p$ est inversible, car il l'est dans $\mathbf F_p$ ; donc $\binom nk a_n = 0$ équivaut à $p \mid \binom nk$ ou $a_n = 0$. Ainsi $f$ est tué si et seulement si $p$ divise $n$, $\binom n2$ et $\binom n3$ pour tout $n$ tel que $a_n \neq 0$. Le théorème de Lucas (\texttt{Choose.\allowbreak{}choose\_modEq\_choose\_mod\_mul\_choose\_div\_nat} de Mathlib) donne $\binom nk \equiv \binom{n \bmod p}{k \bmod p}\binom{\lfloor n/p\rfloor}{\lfloor k/p\rfloor} \pmod p$. Si $p > 3$ et $p \mid n$, cela vaut $\binom 0k = 0$ pour $k = 2, 3$ : la condition se réduit à $p \mid n$. Si $p = 2$ : $\binom n2 \equiv \lfloor n/2\rfloor$ quand $n$ est pair, donc $2 \mid n$ et $2 \mid \binom n2$ équivalent à $4 \mid n$, et alors $\binom n3 \equiv \binom 01 \lfloor n/2 \rfloor = 0$. Si $p = 3$ : $\binom n3 \equiv \lfloor n/3\rfloor$ quand $3 \mid n$, donc $3 \mid n$ et $3 \mid \binom n3$ équivalent à $9 \mid n$, et alors $\binom n2 \equiv \binom 02 = 0$. (2) Par le lemme~\ref{lem:93-chaine}, les trois dérivées de $f \circ u$ sont des combinaisons de $u_1$, $u_2$, $u_3$, nuls ; et $X^m$ est tué par~(1). (3) et (4) sont des calculs de coefficients binomiaux : $N(X + X^2) = 1$ sur tout anneau et $D^{(1)}(X + X^2) = 1 + 2X$ ; $N(X + X^3) = 6X^2 - 1$ et $D^{(1)}(X + X^3) = 1 + 3X^2$.
\end{proof}

\begin{remarque}
La vérification confirme la page~120 sans hypothèse sur la base : $G = 12\,G_0$ est une identité sur $\mathbf Z$, et $G_0$ est défini partout, en caractéristique~$2$ et~$3$ comprises. La relation de cocycle vaut sous la forme~(1), sans dénominateur ; l'invariance par les homographies ne demande que $D^{(2)}$ et $D^{(3)}$ nuls sur le numérateur et le dénominateur, ce qui couvre les homographies à coefficients dans $\mathcal O'$, les fonctions tuées, en toute caractéristique. La valeur test de la page~72 est confirmée, $G_0(t, t^3) = \frac{2}{3t^2}\,dt^2$, ainsi que la correction de la lecture pour le premier essai : $G_0(t, t^2) = \frac{1}{4t^2}\,dt^2$, là où la page écrit $\frac{1}{2t}\,dt^2$. Dans le modèle local, la marge de la page~121 est exacte : les fonctions tuées sont les polynômes en $X^p$ si $p > 3$, en $X^4$ si $p = 2$, en $X^9$ si $p = 3$. Les points~(3) et~(4) montrent que ce niveau $p^2$ est nécessaire pour l'invariance : en caractéristique~$2$, $t^2$ a une différentielle nulle mais la translation $t \mapsto t + t^2$ donne $G_0 = dt^2$ ; en caractéristique~$3$, $t \mapsto t + t^3$ donne $G_0 = -dt^2$. Le groupe qui laisse $G_0$ invariant n'est donc pas celui des homographies à coefficients dans $\mathcal O^{(p)}$ pour $p = 2, 3$. Ces énoncés portent sur l'invariance ; la rigidité réciproque est traitée plus bas dans l'anneau tronqué. Le cadre est $R[X]$ : les unités de $R[X]$ sont rares, et l'hypothèse \q{$D^{(1)}$ inversible} n'y est satisfaite que pour des $f$ particuliers ; les formes sans dénominateur, (1) du cocycle et $q^2 N(s) = 0$, n'ont pas cette limite. Le passage aux séries formelles, à $A[T]/(T^{p^N} - \alpha)$ pour $\alpha \neq 0$ ou à une courbe lisse n'est pas formalisé.
\end{remarque}

\noindent\emph{Le modèle tronqué.} La Proposition des pages~121 à~123 porte sur $B = A[T]/(T^{p^N} - \alpha)$, et la page se ramène d'abord à $\alpha = 0$ (\lot{93}{7}{122}). On travaille dans $B_n = A[T]/(T^n)$, en écrivant ses éléments comme classes de polynômes $s \in A[X]$. Comme $t$ est nilpotent dans $B_n$, un élément de $B_n$ est inversible si et seulement si son terme constant l'est ; $D^{(1)} s$ est donc inversible dans $B_n$ si et seulement si $s_1 \in A^*$. Le lemme suivant dit que, pour $n = p^N > 3$ en caractéristique $p$, la condition $G_0(t, s) = 0$ dans $B_n$ s'écrit $X^n \mid N(s)$. L'énoncé de rigidité est formulé dans $A[X]$ avec ces deux traductions.

\begin{lemme}\label{lem:93-tronque}
Soit $A$ de caractéristique $p$ première et $n = p^N$. Pour $k < n$ et $g \in A[X]$, $D^{(k)}(X^n g) = X^n D^{(k)} g$. Si $n > 3$, $X^n$ divise $N(s + X^n g) - N(s)$ pour tous $s, g \in A[X]$.
\end{lemme}

\begin{proof}
La première assertion est l'énoncé général rappelé à la suite de la démonstration : par Leibniz, elle revient à la nullité des $D^{(i)}(X^n)$ pour $0 < i < p^N$. Si $n > 3$, on l'applique à $k = 1, 2, 3$ : $D^{(k)}(s + X^n g) = D^{(k)} s + X^n D^{(k)} g$, et en développant, $N(s + X^n g) - N(s)$ est $X^n$ fois $2\,D^{(2)}s\,D^{(2)}g + X^n (D^{(2)}g)^2 - D^{(3)}s\,D^{(1)}g - D^{(3)}g\,D^{(1)}s - X^n D^{(3)}g\,D^{(1)}g$.
\end{proof}
\general{HasseDerivXPowMul}

\begin{enonce}[Page 122, le premier terme non affine\piste{93-integral-schwarzian-level-p2}]
Soient $A$ un anneau commutatif, $s \in A[X]$, $a, b, c, d \in A$, $q = cX + d$ et $r = s\,q$.
\begin{enumerate}
\item $q\,N(s) = D^{(2)} s \cdot D^{(2)} r - D^{(1)} s \cdot D^{(3)} r$.
\item Si $X^{j+3}$ divise $r - (aX + b)$, le coefficient de $X^j$ dans $q\,N(s)$ est $-\binom{j+3}{3}\, s_1\, r_{j+3}$.
\end{enumerate}
\end{enonce}

\begin{proof}
(1) On a $D^{(1)} q = c$ et $D^{(2)} q = D^{(3)} q = 0$, donc par Leibniz $D^{(2)} r = D^{(2)}s\,q + c\,D^{(1)}s$ et $D^{(3)} r = D^{(3)}s\,q + c\,D^{(2)}s$. Alors $D^{(2)} s \cdot D^{(2)} r - D^{(1)} s \cdot D^{(3)} r = q\,\bigl((D^{(2)}s)^2 - D^{(3)}s\,D^{(1)}s\bigr)$, les termes en $c$ se compensant. (2) Soit $e = r - (aX + b)$. Les dérivées $D^{(2)}$ et $D^{(3)}$ tuent $aX + b$, donc $D^{(k)} r = D^{(k)} e$ pour $k = 2, 3$. Le coefficient de $X^i$ dans $D^{(k)} e$ est $\binom{i+k}{k} e_{i+k}$, nul si $i + k < j + 3$. Donc $X^{j+1}$ divise $D^{(2)} e$ et $X^j$ divise $D^{(3)} e$, dont le coefficient de $X^j$ est $\binom{j+3}{3} e_{j+3} = \binom{j+3}{3} r_{j+3}$, puisque $j + 3 \geq 2$. Dans~(1), le premier produit n'a pas de terme en $X^j$, et le terme en $X^j$ du second est $(D^{(1)}s)_0 \binom{j+3}{3} r_{j+3} = s_1 \binom{j+3}{3} r_{j+3}$.
\end{proof}

\begin{enonce}[Pages 121 à 123, la rigidité\piste{93-integral-schwarzian-level-p2}]
Soient $A$ un anneau commutatif et $n$ un entier tel que $\binom k3$ soit inversible dans $A$ pour $3 \leq k < n$. Soit $s \in A[X]$ avec $s_1 \in A^*$, et supposons nuls les coefficients de $X^m$ dans $N(s)$ pour $m + 3 < n$ (c'est le cas si $X^n \mid N(s)$). Posons $c = -s_2/s_1$, $b = s_0$, $a = s_1 + c\,s_0$. Alors $a - bc = s_1$ et $X^n$ divise $s\,(cX + 1) - (aX + b)$ : dans $B_n$, $s = (at + b)/(ct + 1)$. En particulier :
\begin{enumerate}
\item si $A$ est de caractéristique $p$ première et $n = p$, sans autre hypothèse sur $A$ ; et si de plus $p > 3$, pour $s_1 \in A^*$, $X^p \mid N(s)$ équivaut à l'existence de $a, b, c \in A$ avec $X^p \mid s\,(cX + 1) - (aX + b)$ ;
\item pour $n = 4$, sur tout anneau $A$ (niveau $p^2$ pour $p = 2$) ;
\item si $A$ est de caractéristique $3$ et $n = 9$ (niveau $p^2$ pour $p = 3$) ;
\item si $A$ est une $\mathbf Q$-algèbre, dans $A[X]$ même : $N(s) = 0$ et $s_1 \in A^*$ entraînent $s\,(cX + 1) = aX + b$.
\end{enumerate}
Plus généralement, si $A$ est de caractéristique $p$, $n = p^N > 3$, $d \in A^*$ et $X^n \mid s\,(cX + d) - (aX + b)$, alors $X^n \mid N(s)$.
\end{enonce}

\begin{proof}
Soit $r = s\,(cX + 1)$, de coefficients $r_0 = s_0 = b$, $r_1 = s_1 + c\,s_0 = a$ et $r_2 = s_2 + c\,s_1 = 0$ ; on a $a - bc = s_1$. On montre par récurrence sur $i < n$ que le coefficient de $X^i$ dans $r - (aX + b)$ est nul. Pour $i \leq 2$ c'est le calcul précédent. Pour $i = j + 3 < n$, l'hypothèse de récurrence dit que $X^{j+3}$ divise $r - (aX + b)$. Les coefficients de $N(s)$ de degré $\leq j$ sont nuls, donc aussi le coefficient de $X^j$ dans $(cX + 1)\,N(s)$ ; par l'énoncé précédent, $\binom{j+3}{3} s_1 r_{j+3} = 0$, et $r_{j+3} = 0$ puisque $\binom{j+3}3$ et $s_1$ sont inversibles. (1) Pour $3 \leq k < p$, $p$ ne divise pas $\binom k3$ : sinon il diviserait $\binom k3 \cdot 3!\,(k-3)! = k!$, d'où $p \leq k$. Un entier premier à $p$ est inversible dans $A$, car il l'est dans $\mathbf F_p$. (2) Seul $k = 3$ intervient, et $\binom 33 = 1$. (3) Pour $k = 3, \dots, 8$, $\binom k3 = 1, 4, 10, 20, 35, 56$, premiers à $3$. (4) $\binom k3 \neq 0$ pour $k \geq 3$, donc inversible dans $\mathbf Q$ et dans $A$ ; les hypothèses valent pour tout $n$, et on prend $n$ plus grand que le degré de $f = s\,(cX + 1) - (aX + b)$ : tous les coefficients de $f$ sont nuls. Pour la dernière assertion, écrivons $s\,q = aX + b + X^n g$ avec $q = cX + d$. Par l'énoncé précédent et le lemme~\ref{lem:93-tronque}, $q\,N(s) = D^{(2)}s \cdot X^n D^{(2)} g - D^{(1)}s \cdot X^n D^{(3)} g$, divisible par $X^n$. Le polynôme $q$, de terme constant $d$ inversible, est premier à $X$, donc à $X^n$ (énoncé général rappelé à la suite de la démonstration) ; donc $X^n$ divise $N(s)$. La réciproque de~(1) en est le cas $N = 1$, $d = 1$.
\end{proof}
\general{PolynomialIsCoprimeX}

\begin{encadre}
\begin{contrexemple}[Page 121, le déterminant\piste{93-integral-schwarzian-level-p2}]
Si $u \in A$ et si $X^3$ divise $uX\,(cX + d) - (aX + b)$ avec $ad - bc = 1$, alors $u$ est un carré dans $A$. En particulier, dans $\mathbf F_5[T]/(T^5)$, $s = 2t$ vérifie $N(s) = 0$ et $D^{(1)} s = 2 \in \mathbf F_5^*$, et $s = (2t + 0)/(0 \cdot t + 1)$, mais $s$ n'est égal à aucune homographie $(at + b)/(ct + d)$ avec $a, b, c, d \in \mathbf F_5$ et $ad - bc = 1$.
\end{contrexemple}
\end{encadre}

\begin{proof}
Les coefficients de $X^0$, $X^1$ donnent $b = 0$ et $a = ud$. Alors $u = u\,(ad - bc) = u^2 d^2 = (ud)^2$. Dans $\mathbf F_5$, $2$ n'est pas un carré (les carrés sont $0$, $1$, $4$), et $X^5 \mid \cdot$ entraîne $X^3 \mid \cdot$. $N(2X) = 0$ car $D^{(2)}$ et $D^{(3)}$ tuent $2X$.
\end{proof}

\begin{remarque}
Dans le modèle tronqué avec $\alpha = 0$, la Proposition des pages~121 à~123 est confirmée sur tout anneau de caractéristique $p$ : l'hypothèse \q{$A$ local, plus généralement $\mathrm{Pic}(A) = 0$} ne sert pas, l'homographie se normalise par $d = 1$ et son déterminant est $s_1$. Cette hypothèse ne sert qu'au passage de $\alpha$ à $0$, démontré plus bas. La démonstration suit la page, avec une différence : au lieu de normaliser $s$ en $t + a t^d + \cdots$ en composant par des homographies, on multiplie $s$ par $cX + 1$ et l'on suit les coefficients de $r = s\,(cX + 1)$ ; l'égalité $q\,N(s) = D^{(2)} s\,D^{(2)} r - D^{(1)} s\,D^{(3)} r$ remplace la relation de cocycle, et le coefficient $a\binom d3$ de la page devient $s_1 \binom{j+3}3 r_{j+3}$ avec $d = j + 3$. Seuls les coefficients de $N(s)$ de degré $< n - 3$ servent. Pour $p = 2$ seul $\binom 33 = 1$ intervient, comme le dit la page~123, et l'énoncé vaut alors sur tout anneau ; pour $p = 3$, les restes $\binom k3 \bmod 3 = 1, 1, 1, 2, 2, 2$ pour $k = 3, \dots, 8$ confirment la colonne de droite de la page~123. L'hypothèse $p > 3$ du point~(1) ne sert pas à l'implication directe, vide pour $n = p \leq 3$ ; elle sert à ce que $D^{(3)}$ passe au quotient $B_p$, ce qui demande $p > 3$, d'où le niveau $p^2$ pour $p = 2, 3$. La normalisation \q{avec $ad - bc = 1$}, ajoutée sur la page~121, est fausse en général : le déterminant est une unité, carré seulement si $s_1$ l'est, et l'énoncé correct porte sur $\mathrm{PGL}_2(A)$. En caractéristique nulle, la conclusion dans $A[X]$ permet $c$ nilpotent : sur $A = \mathbf Q[\varepsilon]/(\varepsilon^2)$, $s = X + \varepsilon X^2$ vérifie $s\,(1 - \varepsilon X) = X$ ; si $A$ est intègre, $c = 0$ et $s$ est affine.
\end{remarque}

{\sloppy\noindent Ces énoncés sont, dans \href{\leanblob/Folder93.lean}{\texttt{Folder93.\allowbreak{}lean}} : \texttt{Ncl\_eq} et \texttt{G\_eq} pour le facteur~$12$ ; \texttt{chain}, \texttt{N\_comp} et \texttt{G0\_comp} pour la relation de cocycle ; \texttt{N\_homography}, \texttt{G0\_homography} et \texttt{G0\_homography\_const} pour l'invariance ; \texttt{N\_X\_sq} et \texttt{N\_X\_cube} pour les valeurs tests ; \texttt{killed\_iff}, \texttt{killed\_iff\_of\_gt}, \texttt{killed\_iff\_two}, \texttt{killed\_iff\_three}, \texttt{Killed.\allowbreak{}comp}, \texttt{char\_two} et \texttt{char\_three} pour la marge de la page~121 ; \texttt{hasseDeriv\_X\_pow\_mul} et \texttt{N\_add\_X\_pow\_mul} pour le lemme~\ref{lem:93-tronque} ; \texttt{N\_mul\_lin} et \texttt{step} pour la page~122 ; \texttt{rigidity\_core}, \texttt{rigidity}, \texttt{rigidity\_of\_gt}, \texttt{rigidity\_four}, \texttt{rigidity\_nine}, \texttt{rigidity\_char\_zero}, \texttt{N\_of\_homography\_trunc} et \texttt{rigidity\_iff\_of\_gt} pour la rigidité ; \texttt{det\_one\_square} et \texttt{det\_one\_counterexample} pour le déterminant.\par}

La marge de la page~121 est le seul point où ces énoncés rejoignent la descente de Cartier. En caractéristique $p$, les fonctions de dérivée nulle forment $\mathcal O^{(p)}$, le faisceau des fonctions du quotient de Frobenius, que la descente de Cartier prend pour faisceau de constantes ; la marge demande en outre $D^{(2)}$ et $D^{(3)}$ nuls, et trouve $\mathcal O^{(p^2)}$ pour $p = 2, 3$. Lean le vérifie dans $R[X]$, sans faisceau ni Frobenius relatif.

\subsection*{La $p$-courbure en rang un et la question de la page~193}

Les pages~193 et~194 partent d'une remarque et posent une question (\lot{93}{10}{193}). La remarque : si une connexion définie sur les entiers a une monodromie finie, sa réduction modulo~$p$ est de $p$-courbure nulle pour presque tout~$p$. La question : la réciproque est-elle vraie ? On démontre ici la remarque dans le cas le plus simple, celui d'un fibré de rang un trivial, avec le calcul qui la sous-tend, la formule de Jacobson. La question reste ouverte ; on l'énonce à la fin.

\noindent\emph{Le cadre.} Soient $A$ un anneau commutatif et $D$ une dérivation de $A$, c'est-à-dire une application additive telle que $D(xy) = x\,Dy + y\,Dx$ ; on peut penser à $A = k[x]$ ou $k(x)$ et à $D = d/dx$. On note $\mu_c$ la multiplication par $c \in A$, vue comme un opérateur sur $A$. Une connexion sur le fibré trivial de rang un, dont les sections sont les éléments de $A$, se donne par une $1$-forme $\omega$ : elle dérive une section $f$ le long de $D$ par $\nabla_D f = Df + \omega(D)\,f$. On écrit $a = \omega(D)$, de sorte que $\nabla_D = D + \mu_a$. Une section $y$ est \emph{horizontale} si $\nabla_D y = 0$, soit $Dy + ay = 0$. Sur les nombres complexes, avec $D = d/dx$, les solutions sont les multiples de $\exp(-\int a)$ ; elles sont algébriques quand la monodromie est finie, par exemple pour $a = -\frac{1}{2x}$, où $y = \sqrt x$.

\noindent\emph{Pourquoi la caractéristique $p$.} En itérant la règle de Leibniz, $D^n(xy) = \sum_k \binom nk D^k x\,D^{n-k} y$. Pour $n = p$ premier, les coefficients $\binom pk$ avec $0 < k < p$ sont divisibles par~$p$ ; si $p = 0$ dans $A$, il ne reste que $D^p(xy) = x\,D^p y + y\,D^p x$, et $D^p$ est encore une dérivation. La connexion sait donc dériver le long de $D^p$, par $\nabla_{D^p} = D^p + \mu_{\omega(D^p)}$, et l'on peut comparer cet opérateur à la puissance $p$-ième $(\nabla_D)^p$. La différence
\[
\psi(D) = (\nabla_D)^p - \nabla_{D^p}
\]
est la \emph{$p$-courbure}. Elle commute aux multiplications : c'est une multiplication par un élément de $A$, et non plus un opérateur différentiel. Elle joue le rôle d'un commutateur. La courbure $[\nabla_D, \nabla_{D'}] - \nabla_{[D, D']}$ mesure le défaut de $\nabla$ à respecter le crochet des champs de vecteurs ; $\psi$ mesure son défaut à respecter la puissance $p$-ième. Si $E$ a localement une base de sections horizontales, $\psi$ les annule ; comme elle est linéaire, elle est nulle. C'est l'idée de la remarque de la page~194.

\begin{enonce}[$D^p$ est une dérivation, classique]
Si $A$ est de caractéristique $p$ premier, pour tous $x, y \in A$, $D^p(xy) = x\,D^p y + y\,D^p x$.
\end{enonce}

\begin{enonce}[Formule de Jacobson en rang un, classique]
Si $A$ est de caractéristique $p$ premier, pour tout $a \in A$, on a l'égalité d'opérateurs sur $A$
\[
(D + \mu_a)^p = D^p + \mu_{a^p + D^{p-1}(a)} .
\]
\end{enonce}

La formule est un cas particulier de celle de Jacobson (1941) \cite{jacobson1941} pour la puissance $p$-ième d'une somme dans une algèbre de caractéristique~$p$. Elle donne la $p$-courbure en rang un : $\psi(D) = \mu_{a^p + D^{p-1}(a) - \omega(D^p)}$. Pour $D = d/dx$ sur $k[x]$ ou $k(x)$, on a $D^p = 0$ (la dérivée $p$-ième de $x^n$ contient le facteur $n(n-1)\cdots(n-p+1)$, divisible par~$p$), et il reste $\psi = a^p + a^{(p-1)}$. Le premier terme est $p$-linéaire en $a$, le second linéaire. C'est la forme que la page~208 donne à la $p$-courbure d'une connexion $d + \omega$ sur $\mathcal O$, $K_0(\omega) = \omega^{\otimes p} - F^*_{X/S}(\widetilde C\omega)$, \q{somme d'une opération $p$-linéaire et d'une opération linéaire} (\lot{93}{11}{208}). L'identification du terme linéaire à l'opérateur de Cartier n'est pas vérifiée en Lean.

\begin{proof}[Idée de la démonstration]
Écrivons $L = D + \mu_a$. La règle de Leibniz dit que $L\,\mu_c = \mu_c\,L + \mu_{Dc}$ : faire passer $L$ à droite d'une multiplication coûte une dérivée. Par récurrence, $L^n \mu_c = \sum_k \binom nk \mu_{D^k c}\,L^{n-k}$, d'où, en caractéristique~$p$, $D^p \mu_c = \mu_c D^p + \mu_{D^p c}$ : c'est le premier énoncé, appliqué à $y$. Pour le second, on introduit une variable $t$ qui commute à tout et l'on considère $(D + t\mu_a)^p$, polynôme en $t$ à coefficients opérateurs. Son terme constant est $D^p$ et son coefficient de $t^p$ est $\mu_a^p = \mu_{a^p}$. Sa dérivée en $t$ est $\sum_{i<p} L_t^i\,\mu_a\,L_t^{p-1-i}$, avec $L_t = D + t\mu_a$ ; la même règle de commutation et l'identité $\sum_{i<n}\binom ik = \binom n{k+1}$ la ramènent à $\sum_k \binom p{k+1} \mu_{D^k a} L_t^{p-1-k}$, où seul le terme $k = p - 1$ survit : la dérivée vaut $\mu_{D^{p-1} a}$ et ne dépend pas de $t$. Le coefficient de $t$ est donc $\mu_{D^{p-1}a}$, et ceux de $t^i$ pour $2 \leq i \leq p-1$ sont nuls, puisque $i$ fois chacun d'eux est nul et que $i$ est inversible modulo~$p$. On fait $t = 1$.
\end{proof}

\begin{encadre}
\begin{theoreme}[Grothendieck, pages 193 et 194, la remarque]\nonverifie
Soient $S$ intègre, de type fini et dominant sur $\mathrm{Spec}\,\mathbf Z$, de point générique $\eta$, $X$ lisse sur $S$ et $E$ localement libre sur $X$ muni d'une connexion relative à courbure nulle. Si $E_\eta$ devient trivial sur un revêtement fini étale de $X_\eta$, il existe un voisinage $U$ de $\eta$ tel que, pour tout $s \in U$ de caractéristique $p > 0$, la $p$-courbure de $E_s$ sur $X_s/k(s)$ soit nulle.
\end{theoreme}
\end{encadre}

La page l'affirme sans démonstration. En voici le cas que Lean vérifie ; c'est un énoncé de l'édition.

\begin{enonce}[Le sens facile en rang un, modèle de l'édition]
Soient $A$ de caractéristique $p$ premier, $y \in A$ inversible d'inverse $z$, et $a \in A$ avec $Dy + ay = 0$. Pour la connexion de forme $\omega = -dy/y$, qui vérifie $\omega(D) = a$ et $\omega(D^p) = -D^p(y)\,z$, la $p$-courbure est nulle :
\[
(D + \mu_a)^p = D^p + \mu_{-D^p(y)\,z} .
\]
Avec la formule de Jacobson, $a^p + D^{p-1}(a) = -D^p(y)\,z$ ; si de plus $D^p = 0$, comme pour $d/dx$ sur $\mathbf F_p(x)$, alors $a^p + D^{p-1}(a) = 0$.
\end{enonce}

\begin{proof}
La section $y$ trivialise la connexion. Pour toute $f$, $y\,D(zf) = Df + y\,D(z)\,f$, et $y\,D(z) = -z\,Dy = a$ en dérivant $yz = 1$ ; donc $D + \mu_a = \mu_y\, D\, \mu_z$. En élevant à la puissance $p$, les facteurs $\mu_z\mu_y = 1$ se simplifient : $(D + \mu_a)^p = \mu_y\, D^p\, \mu_z = D^p + \mu_{y\,D^p(z)}$, par la règle de commutation de $D^p$. Enfin $D^p$ est une dérivation et $D^p(1) = 0$, donc $y\,D^p(z) + z\,D^p(y) = D^p(yz) = 0$. Pour la seconde affirmation, on compare les deux expressions de $(D + \mu_a)^p$ en les appliquant à~$1$.
\end{proof}

Pour $d/dx$ sur $\mathbf F_p(x)$ et $y = x^m$ avec $m$ entier, on a $a = -m/x$. Le calcul direct le confirme : $a^{(p-1)} = -m\,(p-1)!\,x^{-p} = m\,x^{-p}$ par le théorème de Wilson, $a^p = -m^p x^{-p}$, et la somme $(m - m^p)\,x^{-p}$ est nulle par le petit théorème de Fermat. Sur $\mathbf Q$, la connexion $d/dx - c/x$ avec $c$ rationnel a pour solution $x^c$, qui est algébrique ; modulo tout $p$ qui ne divise pas le dénominateur de $c$, $c$ devient un élément de $\mathbf F_p$, donc la classe d'un entier $m$, et la $p$-courbure est nulle par ce calcul.

{\sloppy\noindent Ces énoncés sont, dans \href{\leanblob/Folder93.lean}{\texttt{Folder93.\allowbreak{}lean}}, espace \texttt{PCurvature} : \texttt{iterate\_leibniz} et \texttt{pDerivation} pour le premier, sur un anneau commutatif $A$ avec \texttt{CharP A p} et une dérivation \texttt{D : Derivation ℤ A A} ; \texttt{jacobson} pour la formule de Jacobson, dans \texttt{Module.\allowbreak{}End ℤ A} ; \texttt{pCurvature\_eq\_zero}, \texttt{jacobson\_logDeriv} et \texttt{jacobson\_logDeriv\_of\_pow\_eq\_zero} pour le sens facile. Les règles de commutation sont démontrées dans un anneau quelconque, pour un élément $L$ et une famille $M_c$ avec $L M_c = M_c L + M_{Dc}$ (\texttt{pow\_mul\_eq\_sum}, \texttt{pow\_char\_mul}, \texttt{sum\_pow\_mul\_pow}) ; la variable $t$ est celle des polynômes à coefficients dans l'anneau non commutatif des opérateurs.\par}

Ici Lean ne vérifie que le rang un, sur le fibré trivial, et pour un seul champ $D$ ; la sous-section suivante passe au rang quelconque sur le fibré trivial. Ni la $p$-courbure d'un fibré non trivial, ni sa $p$-linéarité en $D$ et l'existence du tenseur demandé page~208, ni le passage d'une connexion sur $X/S$ à ses réductions $E_s$ ne sont formalisés. Le théorème encadré, en rang quelconque et avec un revêtement fini étale, ne l'est pas non plus.

\begin{conjecture*}[Question de la page 193, conjecture de Grothendieck--Katz]
Soient $K$ un corps de nombres, $X$ une variété lisse sur $K$ et $(E, \nabla)$ un fibré vectoriel sur $X$ muni d'une connexion intégrable. On choisit un modèle de $(X, E, \nabla)$ sur un anneau $\mathcal O_K[1/N]$. Si, pour presque tout idéal premier $\mathfrak p$, la réduction de $(E, \nabla)$ modulo $\mathfrak p$ est de $p$-courbure nulle, alors $(E, \nabla)$ a une monodromie finie : de façon équivalente, $E$ admet une base de sections horizontales algébriques, ou encore $(E, \nabla)$ devient trivial sur un revêtement fini étale de $X$.
\end{conjecture*}

Katz l'a démontrée pour les connexions de Gauss--Manin (1972) \cite{katz1972}. Le cas où la monodromie est résoluble, qui contient le rang un, a été établi par D.~et G.~Chudnovsky pour les courbes (1985) \cite{chudnovsky1985}, puis par J.-B.~Bost (2001) \cite{bost2001} et Y.~André (2004) \cite{andre2004}. Le cas général est ouvert, et Lean ne le démontre pas. Il l'énonce seulement, sur un ouvert de la droite affine, sous le nom \texttt{PCurvatureConjecture}. On y prend $A = R[x][1/g]$, où $R$ est intègre, de type fini sur $\mathbf Z$ et de caractéristique nulle, avec $D = d/dx$ et $\nabla = D + \Gamma$ sur $A^n$. L'hypothèse demande que, pour presque tout $p$, la matrice $\Gamma_p$ de la sous-section suivante ait ses coefficients dans $pA$ : comme $D^p$ s'annule modulo~$p$, c'est exactement dire que la $p$-courbure de la réduction est nulle. La conclusion est celle de Katz, une base de solutions algébriques dans une extension de corps où $D$ se prolonge. L'énoncé est une proposition et non un axiome, de sorte qu'aucune preuve n'en dépend.

\subsection*{La $p$-courbure en rang deux, illustration de l'édition}

La page~193 pose sa question pour une connexion de rang quelconque. On reprend donc le calcul du rang un sur le fibré trivial de rang~$n$, et l'on calcule trois exemples en rang deux. Rien de ceci n'est écrit sur la page : ce sont des énoncés de l'édition, qui illustrent la notion dont la page parle.

\noindent\emph{Le cadre.} Les sections sont les vecteurs $v = (v_1, \dots, v_n)$ de $A^n$, et $D$ agit coordonnée par coordonnée. Une connexion est donnée par une matrice $\Gamma \in M_n(A)$, la valeur de la forme de connexion sur $D$, et elle dérive une section par $\nabla v = Dv + \Gamma v$. Une section horizontale est une solution du système différentiel $Dv = -\Gamma v$. Pour $D = d/dx$ et $n = 2$, un tel système équivaut à une équation du second ordre : avec $\Gamma = \bigl(\begin{smallmatrix} 0 & 1 \\ x & 0 \end{smallmatrix}\bigr)$, il s'écrit $v_1' = -v_2$, $v_2' = -x v_1$, d'où $v_1'' = x v_1$, l'équation d'Airy.

\noindent\emph{Pourquoi $\nabla^p$ est linéaire.} Faire passer $\nabla$ à droite d'une multiplication par $c \in A$ coûte, comme en rang un, la dérivée de $c$ : $\nabla(cv) = c\,\nabla v + (Dc)\,v$, car la matrice $\Gamma$ commute à la multiplication par~$c$. En itérant, $\nabla^k(cv) = \sum_j \binom kj (D^j c)\,\nabla^{k-j} v$, et pour $k = p$ les coefficients binomiaux intermédiaires sont nuls modulo~$p$ : il reste $\nabla^p(cv) = c\,\nabla^p v + (D^p c)\,v$. Le même calcul vaut pour $D$ seul, qui est la connexion de matrice nulle. Dans la différence $\psi = \nabla^p - D^p$, les deux termes $(D^p c)\,v$ se compensent, et $\psi(cv) = c\,\psi(v)$. Sur les nombres complexes, $\nabla^p - D^p$ serait un opérateur différentiel d'ordre $p - 1$ ; en caractéristique~$p$, c'est une matrice. Lorsque $D^p = 0$, comme pour $d/dx$ sur $\mathbf F_p[x]$, la connexion dérive le long de $D^p$ par l'opérateur nul, et $\psi$ est exactement la $p$-courbure $\nabla(D)^p - \nabla(D^p)$ ; sinon les deux diffèrent de la matrice $\omega(D^p)$, qui ne change pas la linéarité.

\noindent\emph{La mesure d'un défaut de solutions.} En caractéristique~$p$, l'équation $Dv = -\Gamma v$ est bien plus contrainte que sur $\mathbf C$ : la dérivée de $x^p$ est nulle, les \q{constantes} forment l'anneau $\mathbf F_p[x^p]$, et l'on peut se demander si le système a une base de solutions, c'est-à-dire une matrice inversible $Y$ dont les colonnes sont horizontales. La $p$-courbure est l'obstruction : s'il existe une telle base, $\psi$ est nulle. La réciproque, qui est le théorème de Cartier de la page~188, fait l'objet de la sous-section suivante.

\begin{enonce}[La $p$-courbure du fibré trivial de rang $n$, illustration de l'édition]
Soient $A$ de caractéristique $p$ premier, $D$ une dérivation de $A$, $\Gamma \in M_n(A)$ et $\nabla = D + \Gamma$ sur $A^n$.
\begin{enumerate}
\item L'opérateur $\psi = \nabla^p - D^p$ est $A$-linéaire : $\psi(cv) = c\,\psi(v)$.
\item On pose $\Gamma_0 = 1$ et $\Gamma_{k+1} = D(\Gamma_k) + \Gamma\,\Gamma_k$, où $D$ agit sur chaque coefficient. Alors $\psi(v) = \Gamma_p\,v$ pour tout $v$.
\item Si $Y \in M_n(A)$ vérifie $D(Y) + \Gamma Y = 0$, alors $\Gamma_p Y = -D^p(Y)$. Si de plus $Y$ est inversible et $D^p = 0$, alors $\Gamma_p = 0$.
\end{enumerate}
\end{enonce}

\begin{proof}
(1) est le calcul ci-dessus, écrit dans l'anneau des opérateurs additifs sur $A^n$ avec la règle de commutation déjà employée en rang un. (2) Par récurrence, $\nabla^k e_j$ est la $j$-ième colonne de $\Gamma_k$ : appliquer $\nabla$ à la colonne $j$ d'une matrice $M$ donne la colonne $j$ de $D(M) + \Gamma M$. Comme $D^p e_j = 0$ (les coordonnées de $e_j$ sont $0$ et $1$), $\psi(e_j)$ est la colonne $j$ de $\Gamma_p$, et l'on conclut par linéarité en écrivant $v = \sum_j v_j e_j$. (3) Chaque colonne $y_j$ de $Y$ est horizontale, donc $\nabla^p y_j = 0$ et $\psi(y_j) = -D^p y_j$ ; par~(2), c'est la colonne $j$ de $\Gamma_p Y$. Si $D^p = 0$, $\Gamma_p Y = 0$, et l'on multiplie à droite par l'inverse de~$Y$.
\end{proof}

La récurrence de~(2) donne un moyen pratique de calculer la $p$-courbure d'un système différentiel : on dérive la matrice $p - 1$ fois en la corrigeant à chaque pas.

\begin{enonce}[Trois exemples en rang deux, illustration de l'édition]
Soit $A$ de caractéristique $p$ premier, avec une dérivation $D$.
\begin{enumerate}
\item Si $\Gamma = \mathrm{diag}(a, b)$, alors $\Gamma_p = \mathrm{diag}\bigl(a^p + D^{p-1}a,\ b^p + D^{p-1}b\bigr)$ : la $p$-courbure est faite des deux $p$-courbures de rang un.
\item Si $\Gamma = \bigl(\begin{smallmatrix} 0 & f \\ 0 & 0 \end{smallmatrix}\bigr)$, alors $\Gamma_p = \bigl(\begin{smallmatrix} 0 & D^{p-1} f \\ 0 & 0 \end{smallmatrix}\bigr)$. Sur $\mathbf F_p[x]$, avec $D = d/dx$ et $f = x^{p-1}$, on trouve $\Gamma_p = \bigl(\begin{smallmatrix} 0 & -1 \\ 0 & 0 \end{smallmatrix}\bigr) \neq 0$, et il n'existe aucune matrice inversible de sections horizontales.
\item Si $Dx = 1$ et $\Gamma = \bigl(\begin{smallmatrix} 0 & 1 \\ x & 0 \end{smallmatrix}\bigr)$ (Airy), alors
\[
\Gamma_3 = \begin{pmatrix} -1 & x \\ x^2 & 1 \end{pmatrix} \text{ en caractéristique } 3, \qquad
\Gamma_5 = \begin{pmatrix} x & x^2 \\ x^3 - 1 & -x \end{pmatrix} \text{ en caractéristique } 5 .
\]
\end{enumerate}
\end{enonce}

\begin{proof}
(1) La récurrence reste diagonale, et sur chaque coefficient elle calcule $(D + \mu_a)^k(1)$ ; la formule de Jacobson donne la valeur pour $k = p$. (2) Comme $\Gamma^2 = 0$ et que $\Gamma$ annule toute matrice de la forme $\bigl(\begin{smallmatrix} 0 & g \\ 0 & 0 \end{smallmatrix}\bigr)$, on a $\Gamma_{k+1} = \bigl(\begin{smallmatrix} 0 & D^k f \\ 0 & 0 \end{smallmatrix}\bigr)$ par récurrence. Pour $f = x^{p-1}$, $D^{p-1} f = (p-1)! = -1$ par le théorème de Wilson ; comme $D^p = 0$ sur $\mathbf F_p[x]$, l'énoncé précédent interdit une base de sections horizontales. (3) Sur un anneau quelconque, la récurrence donne
\[
\Gamma_2 = \begin{pmatrix} x & 0 \\ 1 & x \end{pmatrix}, \quad
\Gamma_3 = \begin{pmatrix} 2 & x \\ x^2 & 1 \end{pmatrix}, \quad
\Gamma_4 = \begin{pmatrix} x^2 & 2 \\ 4x & x^2 \end{pmatrix}, \quad
\Gamma_5 = \begin{pmatrix} 6x & x^2 \\ x^3 + 4 & 4x \end{pmatrix},
\]
et l'on réduit modulo $3$ et modulo $5$.
\end{proof}

Le deuxième exemple montre une $p$-courbure qui ne se lit pas sur les morceaux de rang un. La droite engendrée par $e_1$ et le quotient sont des connexions triviales, de $p$-courbure nulle, mais l'extension ne l'est pas. Les sections horizontales vérifient $v_2' = 0$ et $v_1' = -f v_2$ : il faut une primitive de $f$, et $x^{p-1}$ n'en a pas dans $\mathbf F_p[x]$, puisque la primitive attendue $x^p/p$ n'a pas de sens. C'est l'analogue du logarithme, primitive de $1/x$ qui n'est pas algébrique sur $\mathbf C$. La $p$-courbure, ici nilpotente, détecte exactement ce défaut.

Dans le troisième exemple, la trace de $\Gamma_p$ est nulle et son déterminant vaut $-1 - x^3 = -(1 + x)^3$ pour $p = 3$ et $-x^5$ pour $p = 5$ : le polynôme caractéristique, $T^2 - (1+x)^3$ ou $T^2 - x^5$, a ses coefficients dans $\mathbf F_p[x^p]$. Ce fait général n'est pas démontré en Lean. Sur $\mathbf C$, les fonctions d'Airy ne sont pas algébriques ; la conjecture de Grothendieck--Katz prévoit donc une $p$-courbure non nulle pour une infinité de~$p$, et le calcul le constate pour $p = 3$ et $p = 5$.

{\sloppy\noindent Ces énoncés sont, dans \href{\leanblob/Folder93.lean}{\texttt{Folder93.\allowbreak{}lean}}, espace \texttt{PCurvature} : \texttt{nabla}, \texttt{nabla\_comm}, \texttt{pCurvature} et \texttt{pCurvature\_smul} pour la linéarité ; \texttt{curvMat} et \texttt{pCurvature\_apply} pour la récurrence ; \texttt{curvMat\_mul\_horizontal} et \texttt{curvMat\_eq\_zero\_of\_horizontal} pour le sens facile ; \texttt{curvMat\_diagonal\_char}, \texttt{curvMat\_unipotent\_char}, \texttt{curvMat\_unipotent\_X\_pow}, \texttt{not\_horizontal\_unipotent\_X\_pow}, \texttt{curvMat\_airy}, \texttt{curvMat\_airy\_three} et \texttt{curvMat\_airy\_five} pour les exemples. Les trois premiers énoncés sont en rang $n$ quelconque, sur $A^n$ vu comme \texttt{Fin n → A}, et réemploient la règle de commutation \texttt{pow\_char\_mul} du rang un.\par}

Ne sont pas formalisés : la $p$-linéarité de $\psi$ en $D$, le fait que le polynôme caractéristique de $\psi$ a ses coefficients dans $A^p$, et les fibrés non triviaux.

\subsection*{La réciproque de Cartier sur le fibré trivial}

Une base de sections horizontales force la $p$-courbure à s'annuler. La page~188 affirme la réciproque, sous la forme de la descente de Cartier : une connexion de courbure et de $p$-courbure nulles provient d'un module sur le quotient de Frobenius, et elle a donc localement une base de sections horizontales (\lot{93}{10}{188}). On la démontre ici dans le cas le plus simple, celui du fibré trivial $A^n$ sur un anneau qui a une coordonnée.

\noindent\emph{Le cadre.} L'anneau $A$ est commutatif, de caractéristique $p$, muni d'une dérivation $D$ telle que $D^p = 0$ et d'un élément $x$ tel que $Dx = 1$. C'est le cas de $d/dx$ sur $\mathbf F_p[x]$, sur $\mathbf F_p(x)$ et sur $\mathbf F_p[[x]]$. Pour $k < p$, l'entier $k!$ n'est pas divisible par $p$ et il est inversible dans $A$ : on peut écrire $x^k/k!$, et c'est tout ce dont on aura besoin. Comme $D^p = 0$, la $p$-courbure de $\nabla = D + \Gamma$ est $\psi = \nabla^p$, et elle est nulle si et seulement si $\nabla^p v = 0$ pour tout $v$.

\noindent\emph{L'idée : la formule de Taylor.} Sur les nombres réels, une fonction se retrouve à partir de ses dérivées en $0$ : $f(x) = \sum_k f^{(k)}(0)\, x^k/k!$. En caractéristique $p$, on ne peut pas diviser par $p!$, et la série s'arrête d'elle-même au rang $p - 1$ ; l'hypothèse $\nabla^p = 0$ dit justement que les termes suivants seraient nuls. Cartier en tire un opérateur qui fabrique des sections horizontales,
\[
P = \sum_{k=0}^{p-1} \frac{(-x)^k}{k!}\, \nabla^k .
\]
On peut le lire comme \q{la valeur en $x = 0$} : $P(v)$ est la section horizontale qui coïncide avec $v$ au point $x = 0$, quand ce point a un sens.

\noindent\emph{Pourquoi $P(v)$ est horizontal.} La règle de Leibniz $\nabla(c\,w) = c\,\nabla w + (Dc)\,w$ et le calcul $D\bigl((-x)^k/k!\bigr) = -(-x)^{k-1}/(k-1)!$ donnent
\[
\nabla P(v) = \sum_{k=0}^{p-1} \frac{(-x)^k}{k!}\, \nabla^{k+1} v \;-\; \sum_{k=1}^{p-1} \frac{(-x)^{k-1}}{(k-1)!}\, \nabla^{k} v = \frac{(-x)^{p-1}}{(p-1)!}\, \nabla^p v = 0 .
\]
Les deux sommes se compensent terme à terme, sauf le dernier terme de la première, qui est nul par hypothèse.

\noindent\emph{Pourquoi les $P(\nabla^j v)$ suffisent.} La formule de Taylor se retourne :
\[
v = \sum_{j=0}^{p-1} \frac{x^j}{j!}\, P(\nabla^j v) .
\]
En développant, le membre de droite vaut $\sum_{j,k} \frac{x^j (-x)^k}{j!\,k!}\, \nabla^{j+k} v$. Les termes où $j + k \geq p$ sont nuls, puisque $\nabla^p = 0$. Pour $m = j + k < p$, le coefficient de $\nabla^m v$ est $\sum_{j+k=m} \frac{x^j(-x)^k}{j!\,k!} = \frac{(x - x)^m}{m!}$ par la formule du binôme : il vaut $1$ pour $m = 0$ et $0$ sinon. C'est l'identité $e^{xT} e^{-xT} = 1$, tronquée modulo $T^p$, où elle a un sens sans dénominateur divisible par~$p$.

\begin{encadre}
\begin{enonce}[D'après la page 188, réciproque de Cartier sur le fibré trivial]
Soient $A$ un anneau commutatif de caractéristique $p$ premier, $D$ une dérivation de $A$ telle que $D^p = 0$, et $x \in A$ tel que $Dx = 1$.
\begin{enumerate}
\item Si la connexion $\nabla = D + \Gamma$ sur $A^n$ est de $p$-courbure nulle, tout $v \in A^n$ s'écrit $v = \sum_{j<p} \frac{x^j}{j!}\, w_j$ avec $\nabla w_j = 0$ : les sections horizontales engendrent $A^n$.
\item Si $A$ est local (un corps comme $\mathbf F_p(x)$, ou $\mathbf F_p[[x]]$), la connexion $D + a$ de rang un a une base horizontale, c'est-à-dire un inversible $y$ tel que $Dy + ay = 0$, si et seulement si sa $p$-courbure $a^p + D^{p-1}(a)$ est nulle.
\end{enumerate}
\end{enonce}
\end{encadre}

\begin{proof}
Le premier point est le calcul qui précède, avec $w_j = P(\nabla^j v)$. Pour le second, le sens direct est la remarque démontrée plus haut. Réciproquement, la formule de Jacobson donne $(D + a)^p = D^p + a^p + D^{p-1}(a) = 0$, et le premier point appliqué à $v = 1$ écrit $1 = \sum_j \frac{x^j}{j!}\, y_j$ avec des $y_j$ horizontaux. Dans un anneau local, les non-inversibles forment l'idéal maximal, et une somme de non-inversibles n'est pas inversible ; l'un des $y_j$ est donc inversible.
\end{proof}

L'exemple $a = -m/x$ sur $\mathbf F_p(x)$, vu plus haut, en est le cas typique : sa $p$-courbure est nulle, et la réciproque retrouve la solution $x^m$. Sur $\mathbf F_p[x]$, en revanche, le second point dégénère. Les inversibles de $\mathbf F_p[x]$ sont les constantes non nulles, de dérivée nulle, et une base horizontale force $a = 0$. Inversement, si $a^p + a^{(p-1)} = 0$, le premier point fournit une section horizontale non nulle $y$, qui vérifie $y' = -ay$, et la comparaison des degrés impose $a = 0$ : en rang un sur $\mathbf F_p[x]$, la $p$-courbure n'est nulle que pour la connexion triviale. Le premier point, lui, dit quelque chose sur $\mathbf F_p[x]$ en tout rang.

\begin{sloppypar}
\noindent\emph{Portée de la vérification.} Lean démontre ces énoncés dans \href{\leanblob/Folder93.lean}{\texttt{Folder93.\allowbreak{}lean}}, espace \texttt{PCurvature} : \texttt{exp\_mul\_exp} pour l'identité tronquée, \texttt{proj}, \texttt{mul\_proj} et \texttt{taylor} pour le projecteur et la formule de Taylor, écrits dans un anneau d'opérateurs quelconque où $[\nabla, c] = Dc$, \texttt{horizontal\_generate} et \texttt{horizontal\_span} pour le premier point en rang un et en rang $n$, \texttt{horizontal\_unit\_iff} pour le second, et \texttt{horizontal\_unit\_iff\_Fp} pour le cas de $\mathbf F_p[x]$. Ne sont pas démontrés : le fait que les sections horizontales forment un module libre de rang $n$ sur $A^{D} \supseteq \mathbf F_p[x^p]$, avec $A^n = A \otimes M^\nabla$, qui est la descente de Cartier proprement dite, les fibrés non triviaux et les anneaux sans coordonnée globale.
\end{sloppypar}

Hors du fibré trivial traité plus haut, en rang un et en rang quelconque, aucun énoncé du dossier sur la connexion de Gauss--Manin ou sur la $p$-courbure n'est démontré ici : ni la filtration du complexe de De~Rham relatif et la connexion qu'elle définit (pages~161 à~166), ni la descente de Cartier de la page~188 au-delà du fibré trivial, ni les foncteurs de Picard relatifs à connexion et l'existence d'un tenseur de $p$-courbure en rang quelconque (pages~205 à~212), ni le plan des pages~218 à~220. Ne sont pas démontrés non plus : l'unicité de l'homographie au scalaire près (\q{uniques \dots\ scalaire}, page~121) ; la rigidité dans $A[X]$ ou dans les séries formelles en caractéristique $p$, avec des coefficients tués non constants, et sur une courbe lisse en caractéristique $p$ ; l'injectivité espérée page~121 du quotient de $\mathcal P_{X/S}$ par les homographies à coefficients dans $\mathcal O'_X$ dans $\mathrm{Conn}^0_{X/S}$ ; la construction des torseurs $\mathrm{Conn}_{X/S}$ et $\mathrm{Conn}_{0,X/S}$ ; l'unicité de $G_0$ au signe près sur $\mathbf Z$ (page~72) et l'unicité en caractéristique $p$ de la remarque~3 (page~73).

Les pages~233 à~235 cherchent à comparer les complexes de De~Rham de deux relèvements $X'$, $X''$ d'un même $X_0$ sur un épaississement de carré nul (\lot{93}{12}{233}, \lot{93}{12}{234}). Localement on dispose d'isomorphismes $p : X' \to X''$, qui forment un torseur $\mathcal P$ sous un faisceau abélien $\mathcal G$ : deux d'entre eux diffèrent d'un $g \in \mathcal G$. Chaque $p$ donne un isomorphisme de complexes $u(p)$, et changer $p$ en $p + g$ modifie $u(p)$ par une homotopie explicite $k(g)$ :
\[
u(p + g) - u(p) = d\,k(g) + k(g)\,d .
\]
Si $\mathcal P$ avait une section globale, on prendrait $u(p)$ et l'on aurait fini, puisque deux choix sont homotopes. Il n'y en a pas en général, et la page veut éviter les recouvrements. Elle introduit pour cela l'extension $0 \to \mathcal G \to \bar{\mathcal G} \xrightarrow{j} \mathbf Z \to 0$ telle que $j^{-1}(1) = \mathcal P$, le complexe $\mathcal L = [\mathcal G \to \bar{\mathcal G}]$, quasi-isomorphe à $\mathbf Z$, et l'application $\varphi : \mathcal L \to \underline{\mathrm{Hom}}^\bullet(K', K'')$ égale à $k$ en degré $-1$ et à $u$ sur $\mathcal P$. Elle s'arrête sur \q{un homom.\ de la cat.\ dérivée}.

On formalise la version où $\mathcal P$ est un torseur sous un groupe abélien $G$, et non sous un faisceau. Ici $K'$ et $K''$ sont des complexes d'une catégorie additive, $\underline{\mathrm{Hom}}^n(K', K'')$ est le groupe des familles de flèches de degré $n$, et $\delta$ sa différentielle, $\delta(k) = dk + kd$ en degré $-1$.

\begin{encadre}
\begin{theoreme}[D'après les pages 234 et 235, cas d'un groupe abélien\piste{93-derived-morphism-homotopy-torsor}]
Soient $\mathcal P$ un torseur sous un groupe abélien $G$, $k : G \to \underline{\mathrm{Hom}}^{-1}(K', K'')$ additive et $u : \mathcal P \to \underline{\mathrm{Hom}}^0(K', K'')$, avec $u(p + g) - u(p) = \delta(k(g))$ et chaque $u(p)$ morphisme de complexes. L'extension $\bar G$ de $\mathbf Z$ par $G$ avec $j^{-1}(1) = \mathcal P$ se construit sans choisir de point, et $[G \to \bar G]$ est quasi-isomorphe à $\mathbf Z$. Il existe $\varphi^0 : \bar G \to \underline{\mathrm{Hom}}^0(K', K'')$ additif, égal à $u$ sur $\mathcal P$ et à $\delta \circ k$ sur $G$ ; $(k, \varphi^0)$ est un morphisme de complexes. La classe de $u(p)$ dans la catégorie d'homotopie, et dans la catégorie dérivée, ne dépend pas de $p$.
\end{theoreme}
\end{encadre}

\noindent L'énoncé tient : voir \texttt{j\_eq\_zero\_iff}, \texttt{j\_eq\_one\_iff}, \texttt{$\delta$\_$\varphi$0}, \texttt{quotient\_map\_eq} et \texttt{derived\_map\_eq} dans \href{\leanblob/Folder93.lean}{\texttt{Folder93.\allowbreak{}lean}}. On prend pour $\bar G$ le quotient de $G \times \mathbf Z^{(\mathcal P)}$ par les relations $[p + g] - [p] = g$. L'homotopie entre $u(p')$ et $u(p)$ est $k(p' - p)$.

Pour un groupe, le torseur a toujours un point, et l'énoncé se réduit à l'indépendance du choix. Ce que les pages visent, un torseur sous un faisceau sans section globale, n'est pas formalisé, pas plus que l'application aux complexes de De~Rham. La chemise de ces pages annonce la connexion canonique en cohomologie de De~Rham ; y voir une construction de la connexion de Gauss--Manin est une inférence de la lecture, que les pages n'écrivent pas, et Lean n'en vérifie rien.

\begin{encadre}
\begin{theoreme}[Grothendieck, pages 71 à 73 et 120 à 123, schwarzien à dérivées divisées\piste{93-integral-schwarzian-level-p2}]
La différence schwarzienne écrite avec les dérivées divisées $D^{(i)} = \frac{1}{i!}\frac{d^i}{dt^i}$, $G_0(t,s) = -D^{(3)}s/D^{(1)}s + (D^{(2)}s/D^{(1)}s)^2 = G/12$, est un cocycle à valeurs dans $\omega^{\otimes 2}$ défini sur toute base, caractéristiques $2$ et $3$ comprises. Sur un anneau local $A$ de caractéristique~$p$ (on a alors $\mathrm{Pic}(A) = 0$), pour tout $\alpha \in A$, un $s \in A[T]/(T^{p^N} - \alpha)$ avec $D^{(1)}s$ inversible et $G_0(t,s) = 0$ s'écrit $(at+b)/(ct+d)$ avec $a, b, c, d \in A$ et $ct + d$ inversible, pour $N = 1$ si $p > 3$ et pour $N = 2$ si $p = 2$ ou $3$.
\end{theoreme}
\end{encadre}

\begin{enonce}[Grothendieck, pages 121 à 123, anneau non local\piste{93-integral-schwarzian-level-p2}]
La même conclusion vaut sur tout anneau $A$ de caractéristique~$p$ tel que $\mathrm{Pic}(A) = 0$.
\end{enonce}
\begin{demopage}[pages 120 à 123]
Le facteur $12$, la relation de cocycle et la rigidité pour $\alpha = 0$ sont démontrés plus haut ; la page écrit $G = 12\,G_0$ sans le calcul (p.~120). Elle se ramène à $\alpha = 0$ (\q{OPS}) sans argument, puis, par deux changements de variable homographiques, à $s \equiv t \bmod t^3$ (p.~122). Si $s = t + at^d + \cdots$ avec $d \geq 3$, la comparaison de $D^{(3)}s\,D^{(1)}s$ et de $(D^{(2)}s)^2$ modulo $t^{d-2}$ donne $a\binom d3 = 0$, d'où $a = 0$ pour $p > 3$ (p.~122) ; pour $p = 2$ ou $3$, avec $T^{p^2}$, la page conclut par le critère de Lucas, le cas $p = 3$ refait en marge (p.~123). L'unicité de $G_0$ au signe près (p.~72) n'est pas démontrée.
\end{demopage}

\begin{proof}[Réduction à $\alpha = 0$]
Posons $q = p^N$ et $B = A[T]/(T^q - \alpha)$, et notons $\beta$ la classe de $T$. Sur $B$ lui-même, $T^q - \alpha = (T - \beta)^q$ par Frobenius : l'extension $A \to B$ est celle qui rend le cas $\alpha = 0$ applicable. L'application de Taylor $\theta(f) = f(\beta + Y)$, de $A[T]$ dans $B[Y]$, a pour coefficients les classes des $D^{(k)}f$, commute aux dérivées divisées et envoie $T^q - \alpha$ sur $Y^q$. Le polynôme $\theta(s)$ vérifie donc, sur la base $B$ et modulo $Y^q$, les hypothèses du cas $\alpha = 0$, et la rigidité démontrée plus haut donne
\[
\theta(s)\,(cY + 1) \equiv aY + s \pmod{Y^q}, \qquad c = -\frac{D^{(2)}s}{D^{(1)}s}, \quad a = D^{(1)}s + cs ,
\]
avec $a, c \in B$ : c'est l'homographie osculatrice en $\beta$, de vecteur de coefficients $v = (a,\ s - aT,\ c,\ 1 - cT)$ en la variable $T$, et l'on a $s\,(v_3 T + v_4) = v_1 T + v_2$ identiquement. Reste à descendre $v$ de $B$ à $A$. En dérivant la congruence une et deux fois en $Y$, on obtient pour chaque coordonnée
\[
(cY + 1)\,\theta(v_j) \equiv v_j \pmod{Y^q},
\]
ce qui dit que l'homographie osculatrice en $\beta + Y$ est la même, à un scalaire près. Pour $\ell = \lambda c + \mu (1 - cT)$, $\lambda, \mu \in A$, le produit $x = \ell^{q-1} v_j$ vérifie alors $(cY + 1)^q\,\theta(x) \equiv x$, et $(cY + 1)^q = 1 + c^q Y^q$ : $\theta(x) \equiv x$, c'est-à-dire $D^{(k)} x = 0$ dans $B$ pour $0 < k < q$. Un élément de $B$ ainsi tué est dans $A$ (on le voit sur le représentant de degré $< q$). Le vecteur $\ell^{q-1} v$ est donc dans $A^4$, et donne $s = (aT + b)/(cT + d)$ avec $cT + d = \ell^{q-1}$ ; de même $\ell^q \in A$. Il reste à choisir $\ell$ inversible. Avec $\gamma = c^q \in A$, on a $(1 - cT)^q = 1 - \gamma\alpha$. Si $A$ est local, $\gamma$ ou $1 - \gamma\alpha$ est inversible, et l'on prend $\ell = c$ ou $\ell = 1 - cT$.

Si l'on suppose seulement $\mathrm{Pic}(A) = 0$, on considère le sous-$A$-module $I$ de $B$ formé des $x = c'T + d$ ($c', d \in A$) tels que $s\,x = a'T + b'$ avec $a', b' \in A$ : ce sont les dénominateurs des homographies égales à $s$. Le coefficient de $Y^2$ dans $\theta(s)\,\theta(x) \equiv a'(\beta + Y) + b' \pmod{Y^q}$, où $q > 2$, donne $D^{(2)}s\cdot x + D^{(1)}s\cdot c' = 0$, donc $c\,x = c' \in A$ et $(1 - cT)\,x = d \in A$ : le module $J = Ac + A(1 - cT)$ vérifie $IJ \subseteq A$. Par ce qui précède, $c^{q-1}$ et $(1 - cT)^{q-1}$ sont dans $I$, et $\alpha\,c^{q-1}\cdot c + (1 - cT)^{q-1}(1 - cT) = \alpha\gamma + 1 - \gamma\alpha = 1$, donc $IJ = A$. Le module $I$ est un sous-$A$-module inversible de $B$, et sa classe dans $\mathrm{Pic}(A)$ est triviale : il est alors de la forme $Au$ avec $u$ inversible dans $B$ (suite exacte $A^\times \to B^\times \to \{\text{sous-modules inversibles}\} \to \mathrm{Pic}(A)$). Comme $u \in I$, on a $u = cT + d$ et $s\,u = aT + b$ avec $a, b, c, d \in A$.
\end{proof}

\noindent\emph{Portée de la vérification.} Lean démontre la réduction dans \href{\leanblob/Folder93.lean}{\texttt{Folder93.\allowbreak{}lean}}, espace \texttt{Alpha}, avec $B$ = \texttt{AdjoinRoot}$(T^q - \alpha)$ : \texttt{$\theta$\_coeff}, \texttt{$\theta$\_D}, \texttt{$\theta$\_P} pour l'application de Taylor, \texttt{descent} pour la descente, \texttt{rigidity\_alpha} pour l'énoncé sur un anneau quelconque de caractéristique $p$ où $\binom k3$ est inversible pour $3 \leq k < q$, avec $\ell$ quelconque, et \texttt{rigidity\_alpha\_local}, \texttt{rigidity\_alpha\_of\_gt}, \texttt{rigidity\_alpha\_four}, \texttt{rigidity\_alpha\_nine} pour l'anneau local et les cas $p > 3$, $p = 2$, $p = 3$, puis \texttt{rigidity\_alpha\_pic}, \texttt{rigidity\_alpha\_pic\_of\_gt}, \texttt{rigidity\_alpha\_pic\_four}, \texttt{rigidity\_alpha\_pic\_nine} pour un anneau tel que $\mathrm{Pic}(A) = 0$ (hypothèse \texttt{Subsingleton (CommRing.Pic A)}), par le sous-module inversible $I$ et \texttt{Submodule.ker\_unitsToPic} de Mathlib. Le passage au faisceau sur une courbe, où $t$ n'est qu'une coordonnée locale, n'est pas formalisé.

\begin{remarque}
La caractérisation des polynômes tués par les dérivées de Hasse d'ordre $0 < k < p^e$ en caractéristique~$p$ (ce sont les polynômes en $X^{p^e}$) vaut sous cette forme générale, avec le critère de divisibilité qu'elle utilise, tiré du théorème de Lucas (1878) \cite{lucas1878} sur les coefficients binomiaux modulo~$p$. Pour $p = 3$ elle porte sur les ordres $k < 9$, quand la marge n'emploie que $D^{(1)}$, $D^{(2)}$, $D^{(3)}$.
\end{remarque}

\begin{remarque}
Deux lemmes servent à la démonstration de la rigidité : le passage des dérivées de Hasse d'ordre $< p^e$ à travers la multiplication par $X^{p^e}$, et le critère selon lequel un polynôme $P$ est premier à $X - a$ si et seulement si $P(a)$ est inversible. Pour $a = 0$, il dit qu'un polynôme de terme constant inversible est premier à $X$, donc à $X^n$, ce qu'emploie la démonstration.
\end{remarque}
\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{exemple*}[Grothendieck, pages 30 à 32 et 35, carte des structures spéciales de $M_{0,5}$\piste{148-m05-special-structures-chart}]\nonverifie
Comme points de base et générateurs d'une présentation du groupoïde de Teichmüller de cinq points sur la sphère, construite à partir de pièces de dimension modulaire $\leq 1$, la cote propose une carte de $542$ structures spéciales en neuf orbites sous $\mathfrak S_5$ sur trois niveaux ($12$ pentagonales, $20$ bitétraédriques et $30$ pyramidales ; $60 + 60 + 120$ ; $60 + 120 + 60$), reliées par $1620$ flèches en quatorze orbites.
\end{exemple*}
\end{encadre}
{\small Les relations sont annoncées et jamais écrites. Pour trois types de flèches, les sources et buts dessinés ne correspondent pas aux facteurs du décompte, que l'édition reproduit sans le vérifier, et \q{1620} surcharge un \q{1580} barré. Mathlib n'a pas le groupoïde de Teichmüller. On se reportera aux notes de Grothendieck (\lot{148}{2}{30}).\par}

\begin{encadre}
\begin{enonce}[Grothendieck, pages 30 et 32, les décomptes de la carte]\verifie[\leanblobmain]{Folder148Chart}
Si chacun des neuf types de structures spéciales de la page~30 compte $120/|G|$ structures, où $G$ est son groupe d'automorphismes holomorphes, d'ordres $10$, $6$ et $4$ au niveau~$2$, $2$, $2$ et $1$ au niveau~$1$, $2$, $1$ et $2$ au niveau~$0$, les trois niveaux portent $62$, $240$ et $240$ structures, $542$ en tout. Les quatorze types de flèches de la page~32, comptés comme la lecture les tabule, forment trois groupes de $180$, $420$ et $1020$ flèches, $1620$ en tout.
\end{enonce}
\end{encadre}
{\small \emph{Démonstration.} Le groupe $\mathfrak S_5$, d'ordre $120$, permute les structures d'un même type, et $G$ est le stabilisateur de l'une d'elles ; d'où les $120/|G|$ structures du type, que la page inscrit dans son tableau. Ces nombres sont $12$, $20$, $30$ ; $60$, $60$, $120$ ; $60$, $120$, $60$ (\texttt{counts\_eq}), de sommes $62$, $240$ et $240$ par niveau et $542$ en tout (\texttt{vertices}). Les flèches de la page~32 se comptent par groupes : $60 + 120 = 180$ pour les flèches entre structures de niveau~$2$, $60 + 120 + 60 + 60 + 120 = 420$ et $120 + 120 + 120 + 120 + 360 + 120 + 60 = 1020$ pour les deux autres, soit quatorze types et $1620$ flèches (\texttt{arrows\_eq}). Lean décide ces égalités d'entiers. Il ne vérifie ni la liste des neuf types, ni leurs groupes d'automorphismes, ni le nombre de flèches de chaque type. Le $360$ du septième type du dernier groupe est celui que la lecture restitue sous une ligne surchargée, et pour trois types les sources et buts du tableau ne s'accordent pas avec les facteurs du décompte ; la carte elle-même reste donc non vérifiée. Les noms sont ceux de \href{\leanblobmain/Folder148Chart.lean}{\texttt{Folder148Chart.\allowbreak{}lean}}.\par}

\begin{encadre}
\begin{definition*}[Grothendieck, pages 40 et 49 à 60, groupoïde de Teichmüller multimarqué\piste{148-multimarked-teichmuller-groupoid}]
Dans le groupoïde de Teichmüller des surfaces découpées, chaque cercle de découpe ou de bord $a$ porte un nombre quelconque $r(a) \geq 0$ de points marqués, qui forment un torseur sous le groupe tordu $\mathbf Z_a/r(a)$. Les opérations élémentaires sont, outre le découpage et le recollement, l'effacement partiel uniforme, restriction au sous-groupe d'ordre $r'$ divisant $r$, et le surmarquage uniforme, extension le long de $\mathbf Z/r \to \mathbf Z/dr$. Le recollement de deux cercles est défini à isomorphisme unique près dès qu'ils portent le même nombre de points et qu'on se donne un anti-isomorphisme de leurs torseurs.
\end{definition*}
\end{encadre}
{\small La définition du surmarquage uniforme et la phrase qui ramène le recollement à $r(a) = r(a')$ contiennent des mots illisibles, et la restriction au sous-groupe d'ordre $r'$ corrige la page. Mathlib n'a pas le groupoïde de Teichmüller des surfaces découpées, et Lean ne vérifie pas la définition elle-même. Il vérifie l'unique énoncé qu'elle contient, l'unicité du recollement, dont la page affirme qu'il est \q{bien déterminé} sans dire pourquoi (encadré suivant). On se reportera aux notes de Grothendieck (\lot{148}{2}{40} et \lot{148}{3}{58}).\par}

\begin{encadre}
\begin{theoreme*}[Grothendieck, pages 55 à 58, unicité du recollement\piste{148-multimarked-teichmuller-groupoid}]\verifie[\leanblobmain]{Folder148}
Soient $a$ et $a'$ deux cercles orientés portant chacun $r \geq 1$ points marqués, ceux de $a$ formant un torseur $R_a$ sous $\mathbf Z/r$, et soit $u : R_a \to R_{a'}$ un anti-isomorphisme de torseurs. L'espace des homéomorphismes $a \to a'$ qui renversent l'orientation et induisent $u$ sur les points marqués est non vide et contractile. En particulier deux recollements le long de $u$ sont isotopes parmi les recollements le long de~$u$.
\end{theoreme*}
\end{encadre}
{\small Lean vérifie l'énoncé dans le modèle des relèvements. Le cercle est $\mathbf R/\mathbf Z$, orienté par $\mathbf R$ ; ses points marqués sont donnés par leurs relèvements $p : \mathbf Z \to \mathbf R$, strictement croissants avec $p(k + r) = p(k) + 1$, à des positions quelconques (\texttt{Marking}). Le point $p(k)$ porte l'étiquette $k \bmod r$, et le générateur de $\mathbf Z/r$ fait passer au point suivant dans le sens de l'orientation. Un anti-isomorphisme $u$ vérifie $u(x + 1) = u(x) - 1$, donc $u(x) = c - x$ (\texttt{antiIso\_eq}). Un homéomorphisme renversant l'orientation se relève en $F : \mathbf R \to \mathbf R$ continue, strictement décroissante, avec $F(x + 1) = F(x) - 1$ ; deux relèvements diffèrent d'un entier, et on normalise par $F(p(k)) = q(c - k)$ pour tout $k$, où $c \in \mathbf Z$ relève $u$. L'espace $\mathcal G(p, q, c)$ de ces $F$, muni de la topologie compacte-ouverte, est l'espace de l'énoncé (\texttt{gluings}). Il est non vide (\texttt{gluings\_nonempty}). On interpole $p$ de façon affine par morceaux, en un homéomorphisme croissant $h_p$ de $\mathbf R$ avec $h_p(k) = p(k)$ et $h_p(y + r) = h_p(y) + 1$ (\texttt{Marking.\allowbreak{}interpHomeomorph}), de même pour $q$, et $F = h_q \circ (c - \cdot) \circ h_p^{-1}$ convient. Il est convexe (\texttt{convex\_gluings}) : si $F$ et $G$ conviennent et $s + t = 1$ avec $s, t \geq 0$, alors $sF + tG$ est encore strictement décroissante, vérifie $(sF + tG)(x + 1) = (sF + tG)(x) - 1$ et prend en $p(k)$ la valeur $q(c - k)$. C'est l'argument de la lecture, qui raisonne arc par arc : la convexité vaut sur chaque arc entre deux points marqués consécutifs. Un convexe non vide est contractile par l'homotopie rectiligne (\texttt{contractibleSpace\_gluings}), donc connexe par arcs (\texttt{isPathConnected\_gluings}). Chaque élément est un homéomorphisme de $\mathbf R$ (\texttt{toHomeomorph}). Enfin, tout homéomorphisme décroissant qui envoie les points marqués de $a$ sur ceux de $a'$ induit un anti-isomorphisme $k \mapsto c - k$ (\texttt{exists\_antiIso}), de sorte que les espaces $\mathcal G(p, q, c)$ épuisent les recollements qui respectent les marquages. Lean vérifie ensuite l'énoncé sur le cercle lui-même, $\mathbf R/\mathbf Z$ (\texttt{AddCircle 1}). Un homéomorphisme du cercle y renverse l'orientation s'il admet un relèvement continu strictement décroissant, et l'espace de l'énoncé est celui des bijections continues ayant un tel relèvement et envoyant $p(k)$ sur $q(c - k)$ (\texttt{circleGluings}), muni de la topologie compacte-ouverte. Passer au quotient est un homéomorphisme de $\mathcal G(p, q, c)$ sur cet espace (\texttt{gluingsHomeomorph}), qui est donc contractile (\texttt{contractibleSpace\_circleGluings}). Trois points font la preuve. Un relèvement strictement décroissant d'un homéomorphisme est de degré $-1$ : $F(x + 1) - F(x)$ est un entier constant $n < 0$, et si $n \leq -2$ le théorème des valeurs intermédiaires donne $t \in [0, 1]$ avec $F(t) = F(0) - 1$, contre l'injectivité (\texttt{lift\_add\_one}). Les entiers $F(p(k)) - q(c - k)$ ne dépendent pas de $k$, puisque deux consécutifs diffèrent de moins de $1$, et on normalise en retranchant leur valeur (\texttt{exists\_gluing\_of\_mem}). Enfin si deux relèvements normalisés ont des images à distance uniforme $< \varepsilon \leq 1/2$, leur différence, nulle en $p(0)$ et partout à moins de $\varepsilon$ d'un entier, reste par connexité à moins de $\varepsilon$ de $0$ (\texttt{abs\_sub\_lt\_of\_dist\_lt}) ; c'est la continuité de l'inverse. Lean ne vérifie pas le groupoïde. Les noms sont ceux de \href{\leanblobmain/Folder148.lean}{\texttt{Folder148.\allowbreak{}lean}}.\par}

\begin{encadre}
\begin{theoreme*}[Grothendieck, page 49, recollement de cercles sans points marqués\piste{148-multimarked-teichmuller-groupoid}]\verifie[\leanblobmain]{Folder148}
L'espace des homéomorphismes du cercle qui renversent l'orientation a le type d'homotopie du cercle, et son groupe fondamental est $\mathbf Z$. L'espace des recollements de deux cercles sans points marqués n'est donc pas contractible, contrairement au cas $r \geq 1$.
\end{theoreme*}
\end{encadre}
{\small La page prend $r(a) = 0$ sans commentaire, avec le groupe $\mathbf Z_a/0 = \mathbf Z$ ; l'énoncé est celui de la lecture. Lean le vérifie sur \texttt{AddCircle 1}, avec la même définition de l'orientation (\texttt{circleReversing}). L'application $f \mapsto (f(0), f - f(0))$ est un homéomorphisme sur le produit du cercle par l'espace des homéomorphismes renversants qui fixent $0$ (\texttt{circleReversingHomeomorph}). Ce dernier est l'espace de l'encadré précédent pour $r = 1$, $p = q = \mathrm{id}$ et $c = 0$, donc contractile, d'où l'équivalence d'homotopie avec le cercle (\texttt{circleReversingHomotopyEquiv}) et, par le groupe fondamental du cercle de Mathlib (\texttt{AddCircle.\allowbreak{}windingNumberIso}), l'isomorphisme $\pi_1 \simeq \mathbf Z$ (\texttt{circleReversing\_\allowbreak{}fundamentalGroup}). Lean ne vérifie pas que le générateur, la rotation complète d'un des deux bords, est le twist de Dehn le long du cercle de recollement, ni que le recollement devient unique une fois donné un torseur de cadrages sous $\mathbf Z$ ; ces deux points sont ceux de la lecture.\par}