\section[Cote 5 : l'algèbre artinienne universelle à puissances divisées]{Cote 5 : l'algèbre artinienne universelle à puissances divisées\protect\verifie{Folder5}}\label{sec:5} La cote 5, \emph{Cristaux et cohomologie de De Rham : généralités, correspondances Deligne et Berthelot}, que l'inventaire date de 1965--1969, porte sur les puissances divisées et les sites cristallins. À la page~4, l'algèbre locale artinienne universelle sur $W(k)$ dont l'idéal maximal porte des puissances divisées nulles en degrés $\geq p^{\nu+1}$ est présentée comme $W[\Lambda_0, \dots, \Lambda_\nu]/(\Lambda_i^p - q_i\Lambda_{i+1}, \Lambda_\nu^p, \Lambda_0 - p)$, où $\Lambda_i = \gamma_{p^i}(p)$ et $q_i = (p^{i+1})!/((p^i)!)^p$ (\lot{5}{1}{4}) ; la relation est $\gamma_{p^i}(x)^p = q_i\, \gamma_{p^{i+1}}(x)$. Une note de la lecture s'appuie sur $v_p(q_\nu) = 1$. \begin{theoreme}[Énoncé de l'édition, d'après la page 4\piste{5-universal-artinian-pd-normal-form}] Pour tout entier $p$ et tout $i$, $((p^i)!)^p\, q_i = (p^{i+1})!$ : $q_i$ est un entier, le coefficient multinomial de $p$ blocs de taille $p^i$. Si $p$ est premier, $(p-1)\, v_p((p^i)!) = p^i - 1$ et $v_p(q_i) = 1$. \end{theoreme} \noindent L'énoncé tient. La valuation vient de la formule de Legendre sous la forme $v_p((pm)!) = v_p(m!) + m$ ; voir les théorèmes \texttt{factorial\_eq\_mul\_q}, \texttt{q\_eq\_multinomial} et \texttt{padicValNat\_q} de \href{\leanblob/Folder5.lean}{\texttt{Folder5.\allowbreak{}lean}}. \noindent\emph{L'universalité (page~4).} La page place l'énoncé d'universalité entre crochets, sans démonstration ; la lecture en esquisse une par l'enveloppe à puissances divisées. La vérification en donne une autre, qui n'utilise que mathlib. On travaille sur un anneau intègre $W$ de caractéristique nulle où les entiers premiers à $p$ sont inversibles : c'est le cas de $W(k)$ et de $\mathbf Z_p$ (\texttt{padicInt\_isUnit\_natCast}). On pose \[ A^{(\nu)} = W[\Lambda_0, \ldots, \Lambda_\nu] \big/ \bigl(\Lambda_i^{p} - q_i\Lambda_{i+1}\ (i < \nu),\ \Lambda_\nu^{p}\bigr), \qquad W^{(\nu)} = A^{(\nu)}/(\Lambda_0 - p), \] qui est bien le quotient de $W[\Lambda]$ par toutes les relations de la page (\texttt{presentation}), et $J = (\Lambda_0, \ldots, \Lambda_\nu) \subset W^{(\nu)}$. \begin{theoreme}[Grothendieck, page 4, universalité de la présentation\piste{5-universal-artinian-pd-normal-form}] L'idéal $J$ de $W^{(\nu)}$ porte une structure de puissances divisées $\delta$ telle que $\delta_{p^i}(p) = \Lambda_i$ pour $0 \leq i \leq \nu$ et $\delta_n(y) = 0$ pour $y \in J$ et $n \geq p^{\nu+1}$. Pour toute $W$-algèbre $T$ munie d'un idéal $I$ à puissances divisées $\gamma$ tel que $p \in I$ et $\gamma_n(p) = 0$ pour $n \geq p^{\nu+1}$, il existe un unique morphisme de $W$-algèbres $W^{(\nu)} \to T$ compatible aux puissances divisées ; il envoie $\Lambda_i$ sur $\gamma_{p^i}(p)$. \end{theoreme} \begin{proof} \emph{Un plongement.} Soit $K$ le corps des fractions de $W$ et $B = K[X]/(X^{p^{\nu+1}})$. L'application $\psi : \Lambda_i \mapsto X^{p^i}/(p^i)!$ respecte les relations, puisque $((p^i)!)^p q_i = (p^{i+1})!$, et définit $\psi : A^{(\nu)} \to B$. Elle est injective. D'une part les monômes $\Lambda^a$ à exposants $0 \leq a_i < p$ engendrent $A^{(\nu)}$ comme $W$-module : leur $W$-module est stable par multiplication par chaque $\Lambda_j$, grâce à la retenue de la page~8 ($\Lambda_j^{p} = q_j\Lambda_{j+1}$, ou $0$ si $j = \nu$). D'autre part $\psi(\Lambda^a)$ est un multiple non nul de $X^{\sum a_i p^i}$, et ces exposants sont distincts et $< p^{\nu+1}$ (écriture en base $p$). Un élément $\sum w_a \Lambda^a$ de noyau nul a donc tous ses $w_a$ nuls. \emph{Les puissances divisées de $A^{(\nu)}$.} Comme $B$ est une $\mathbf Q$-algèbre, tout idéal de $B$ porte les puissances divisées $x^n/n!$. On les ramène sur $\bar I = (\Lambda_0, \ldots, \Lambda_\nu) \subset A^{(\nu)}$ par $\psi$ : il suffit que $\gamma_n(\psi(y))$ soit dans $\psi(\bar I)$ pour $y \in \bar I$. Par les formules de la somme et du produit, il suffit de le voir pour $y = \Lambda_i$, et comme $\gamma_n(\gamma_{p^i}(X))$ est un multiple entier de $\gamma_{np^i}(X)$, il suffit que chaque $\gamma_k(X) = X^k/k!$ vienne de $A^{(\nu)}$. C'est une récurrence sur $k$ : si $p^e$ est la plus grande puissance de $p$ divisant $k$, on a $\binom{k}{p^e}\gamma_k = \gamma_{p^e}\,\gamma_{k-p^e}$, et $\binom{k}{p^e} \equiv k/p^e \not\equiv 0 \pmod p$ par le théorème de Lucas, donc inversible dans $W$ ; et $\gamma_{p^e}(X) = \psi(\Lambda_e)$ si $e \leq \nu$, tandis que $\gamma_k(X) = 0$ si $k \geq p^{\nu+1}$. \emph{Passage au quotient.} L'augmentation $\varepsilon : A^{(\nu)} \to W$, $\Lambda_i \mapsto 0$, a pour noyau $\bar I$. Si $(\Lambda_0 - p)a \in \bar I$, alors $-p\,\varepsilon(a) = 0$, donc $a \in \bar I$ ; et $\gamma_n((\Lambda_0 - p)a) = (\Lambda_0 - p)^n\gamma_n(a)$. Ainsi $(\Lambda_0 - p) \cap \bar I$ est un sous-idéal à puissances divisées, et celles-ci passent à $J = \bar I\,W^{(\nu)}$. On a $\delta_{p^i}(p) = \delta_{p^i}(\Lambda_0) = \Lambda_i$ par injectivité de $\psi$, et $\delta_n(y) = 0$ pour $n \geq p^{\nu+1}$ parce que $\psi(y)$ est un multiple de $X$. \emph{L'universalité.} Le morphisme $\Lambda_i \mapsto \gamma_{p^i}(p)$ respecte les relations : $\gamma_{p^i}(p)^p = q_i\,\gamma_{p^{i+1}}(p)$ (\texttt{dpow\_pow\_eq\_q}), $\gamma_{p^\nu}(p)^p = q_\nu\gamma_{p^{\nu+1}}(p) = 0$ et $\gamma_1(p) = p$. Il commute aux $\delta_k(p)$ par la même récurrence sur $k$, et donc aux puissances divisées des générateurs $\Lambda_i$, ce qui suffit. Un morphisme compatible envoie nécessairement $\Lambda_i = \delta_{p^i}(p)$ sur $\gamma_{p^i}(p)$, d'où l'unicité. \end{proof} \noindent L'énoncé tient, sous une forme plus forte que celle de la page : ni la locali\-té, ni l'artinianité, ni le corps résiduel n'interviennent, et l'hypothèse sur $T$ ne porte que sur les $\gamma_n(p)$. Lean : \texttt{universal}, \texttt{dpWν}, \texttt{dpWν\_p}, \texttt{dpWν\_eq\_zero}, \texttt{presentation} ; pour les étapes, \texttt{boxSpan\_eq\_top} (la retenue), \texttt{deg\_injective}, \texttt{psi\_injective}, \texttt{dpow\_split} et \texttt{choose\_pow\_mul\_pow\_modEq} (Lucas), \texttt{psi\_hmem}, \texttt{dpIbar}, \texttt{isSubDPIdeal\_Kp}, dans \href{\leanblob/Folder5.lean}{\texttt{Folder5.\allowbreak{}lean}}. \begin{theoreme}[Grothendieck, pages 5 et 6, la suffisance du lemme\piste{5-universal-artinian-pd-normal-form}] Soient $\lambda_0, \ldots, \lambda_\nu \in W$ avec $\lambda_0 = p$ et $\lambda_i^p = q_i\lambda_{i+1}$ (ainsi $\lambda_i = p^{p^i}/(p^i)!$), et $\Theta_i = \Lambda_i - \lambda_i$. Dans $W^{(\nu)}$, on a $p^i\Theta_i = 0$ pour $0 \leq i \leq \nu$ et $p^\nu\lambda_\nu^p = 0$ ; si $\lambda_\nu = p^m u$ avec $u$ inversible, $p^{\nu + pm} = 0$. \end{theoreme} \begin{proof} Récurrence sur $i$, comme à la page~6 : $\Theta_0 = \Lambda_0 - p = 0$. Si $p^i\Theta_i = 0$, la différence $\Lambda_i^p - \lambda_i^p = q_i\Theta_{i+1}$ est un multiple de $\Lambda_i - \lambda_i = \Theta_i$, donc $p^i q_i \Theta_{i+1} = 0$ ; comme $q_i = p\,r_i$ avec $r_i$ premier à $p$ ($v_p(q_i) = 1$), $p^{i+1}\Theta_{i+1} = 0$. Pour $i = \nu$, $\Lambda_\nu^p = 0$ donne de même $p^\nu\lambda_\nu^p = 0$. On n'a pas besoin de développer le binôme. \end{proof} \noindent Pour $\lambda_\nu = p^{p^\nu}/(p^\nu)!$, $m = p^\nu - (p^\nu - 1)/(p-1)$ (par \texttt{sub\_one\_mul\_padicValNat\_factorial\_pow}) et $\nu + pm = c(\nu)$ : c'est le \q{$p^{c(\nu)} \in I$} de la page~6. Lean : \texttt{p\_pow\_mul\_Θ\_mem}, \texttt{p\_pow\_mul\_lam\_pow\_mem}, \texttt{p\_pow\_mem\_Kp}, énoncés comme appartenances à l'idéal $(\Lambda_0 - p)$ de $A^{(\nu)}$. La nécessité, que la page laisse \q{au lecteur} avec un point d'exclamation en marge, est démontrée elle aussi. Pour un exposant $a = (a_0, \ldots, a_\nu)$, $0 \leq a_i < p$, notons $\operatorname{ord}(a)$ l'indice du premier exposant non nul de $a$, et $\operatorname{ord}(0) = c(\nu) = \nu + pm$. \begin{theoreme}[Grothendieck, pages 5 et 6, le lemme et son corollaire\piste{5-universal-artinian-pd-normal-form}] Soient $\lambda_i$ comme ci-dessus, avec $\lambda_\nu = p^m u$, $u$ inversible, et $\Theta_i = \Lambda_i - \lambda_i$. \begin{enumerate} \item Les monômes $\Theta^a$, $0 \leq a_i < p$, forment une base du $W$-module $A^{(\nu)}$. \item \emph{(Le lemme de la page 5.)} $\sum_a w_a\Theta^a$ appartient à $(\Lambda_0 - p)$ si et seulement si $p^{\operatorname{ord}(a)}$ divise $w_a$ pour tout $a$ : $w_a \in p^iW$ si $a_i$ est le premier exposant non nul, et $w_0 \in p^{c(\nu)}W$. \item \emph{(Le corollaire de la page 6.)} $W^{(\nu)} \simeq \bigoplus_a W/p^{\operatorname{ord}(a)}W$ comme $W$-module. \item Si $p$ n'est pas inversible dans $W$, $p^k = 0$ dans $W^{(\nu)}$ si et seulement si $k \geq c(\nu)$ : l'ordre de $1$ est exactement $p^{c(\nu)}$. \item Si $W$ est un anneau de valuation discrète d'uniformisante $p$, $W^{(\nu)}$ est de longueur $\sum_a \operatorname{ord}(a) = p + p^2 + \cdots + p^\nu + pm$. \end{enumerate} \end{theoreme} \begin{proof} \emph{La retenue dans les $\Theta_i$.} En développant $\Lambda_i^p = (\Theta_i + \lambda_i)^p$ et en utilisant $\lambda_i^p = q_i\lambda_{i+1}$, on trouve \[ \Theta_i^p = q_i\Theta_{i+1} - \sum_{0 r$, et $w_0 \in p^{c(\nu)-r}W$. \end{theoreme*} \end{encadre} {\small La forme normale de $W^{(\nu)}$ est démontrée ci-dessus. Pour les quotients $W^{(\nu,r)}$, l'édition n'a fait qu'une vérification à la machine, pour quelques $(p, \nu)$.\par} \begin{encadre} \begin{theoreme*}[Grothendieck, pages 49 et 50, dualité étale pour les sites annelés\piste{5-deligne-letter-ringed-duality}]\nonverifie Soient $f : (X, B) \to (Y, A)$ un morphisme lisse compactifiable de sites annelés, $A$ un faisceau d'anneaux sur $Y$ tué par un entier $n$ premier aux caractéristiques résiduelles, et $B$ un faisceau d'anneaux muni de $f^{-1}(A) \to B$. La dualité étale vaut pour $f$, avec $f^!(K) = R\mathrm{Hom}_{f^{-1}(A)}(B, f^{-1}(K) \otimes T_{X/Y}[2d])$, et se ramène aux cas $f^{-1}(A) \simeq B$ et $f = \mathrm{id}$. La lettre du 10~décembre~1965 l'énonce sans démonstration. \end{theoreme*} \end{encadre} {\small Mathlib n'a pas la dualité étale. On se reportera aux notes de Grothendieck (\lot{5}{3}{49}).\par} \bigskip \noindent Autres pistes de l'onglet Findings pour ce thème, non démontrées ici : \begin{itemize}\small\setlength{\itemsep}{0pt} \item Cote~8 : quand $\pi A$ a des puissances divisées, le relèvement de Lubin--Tate existe et est unique par la seule théorie des déformations cristallines ; sans puissances divisées, l'argument donne l'unicité à isogénie près. La lecture de la page est à vérifier sur le fac-similé. Mathlib n'a pas la théorie des déformations cristallines. On se reportera aux notes de Grothendieck (\lot{8}{3}{43}).\piste{8-lubin-tate-via-hodge-filtration} \item Cote~8 : deux groupes de Barsotti--Tate de dimension un et de hauteur $[K : \mathbf Q_p]$ sur $\mathbf F_q$, munis d'une action de $A$, sont isogènes si et seulement si $\varpi = \varpi'$, et $\mathrm{Hom}_A(G_0, G'_0)$ est alors explicite. La lecture de la page est à vérifier sur le fac-similé. Mathlib n'a pas les groupes de Barsotti--Tate. On se reportera aux notes de Grothendieck (\lot{8}{2}{39}).\piste{8-dim-one-A-module-homs} \end{itemize} \begin{encadre} \begin{theoreme*}[Grothendieck, pages 1 et 4 à 7, valeurs propres unités de la cohomologie évanescente\piste{4-vanishing-unit-root-bound}]\nonverifie On admet le théorème de Lefschetz faible cristallin avec torsion. Pour une section hyperplane lisse $Y$ d'une variété projective lisse $X$ de dimension $n$ sur un corps parfait de caractéristique $p$, le nombre de valeurs propres du Frobenius qui sont des unités $p$-adiques sur la cohomologie cristalline évanescente est au moins le rang $F$-semi-simple de la cohomologie cohérente évanescente $\operatorname{Coker}(H^{n-1}(X, \mathcal O_X) \to H^{n-1}(Y, \mathcal O_Y))$, le défaut étant mesuré par la $p$-torsion de $H^n_{\mathrm{cris}}(X)$. \end{theoreme*} \end{encadre} {\small Les feuillets en esquissent une démonstration incomplète (pages 1 et 4 à 6). Le titre dit l'estimation \q{heuristique}, et l'énoncé~8.4.4~a) de la page~1 y est sans argument. Mathlib n'a pas la cohomologie cristalline. On se reportera aux notes de Grothendieck (\lot{4}{1}{1}).\par} \begin{encadre} \begin{theoreme*}[Grothendieck, pages 52 à 56, modules des variétés abéliennes ordinaires\piste{6-ordinary-moduli-complete-intersection}]\nonverifie Pour une polarisation de degré quelconque, divisible par $p$ compris, l'anneau local en un point du schéma de modules des variétés abéliennes ordinaires polarisées en caractéristique~$p$ (degré de polarisation fixé, structure de niveau de Jacobi) est d'intersection complète et localement irréductible, et le schéma réduit est lisse : les modules formels des couples d'extensions compatibles forment le noyau d'un homomorphisme $\alpha - \beta$ de tores formels. \end{theoreme*} \end{encadre} {\small Les feuillets en esquissent une démonstration incomplète : ils donnent le noyau de $\alpha - \beta$, mais le texte des pages 52 à 56 est en grande partie illisible et reconstitué, et l'hypothèse que $M_0$ est étale est ajoutée par l'édition.\par} \begin{encadre} \begin{theoreme*}[Grothendieck, pages 49 et 50, un groupe formel hors des variétés abéliennes\piste{6-formal-group-not-in-abelian-variety}]\nonverifie Soient $k$ un corps fini et $E$ une courbe elliptique supersingulière sur $k$ dont tous les endomorphismes sont définis sur~$k$. La torsion du groupe formel de $E$ par une unité $\theta$ de $\mathrm{End}(E) \otimes \mathbf Z_p$ de norme réduite transcendante donne une forme de $G_{1,1}$ qui ne se plonge dans le groupe formel d'aucune variété abélienne sur $k$ ni sur aucune extension finie de~$k$. \end{theoreme*} \end{encadre} {\small Les feuillets en esquissent une démonstration incomplète : ils donnent l'obstruction, d'après Weil, et disent \q{facile} l'existence de~$\theta$, qu'ils ne montrent pas.\par} \begin{encadre} \begin{theoreme*}[Grothendieck, pages 47 et 48, même groupe formel, non isogènes\piste{6-same-formal-group-not-isogenous}]\nonverifie Sur un corps algébriquement clos de caractéristique~$p$, il existe des surfaces abéliennes simples de même groupe formel $\hat{\mathbf G}_m \times G_{1,1}$ qui ne sont pas isogènes. \end{theoreme*} \end{encadre} {\small Les feuillets en esquissent une démonstration incomplète : la discrétude de la classe d'isogénie n'y est pas justifiée, et la page compte une famille \q{de dim 2 au plus}, chiffre de lecture douteuse, là où il faut~$1$.\par} \begin{encadre} \begin{theoreme*}[Grothendieck, pages 39 à 44 et 48 à 56, propriété universelle des complexes libres\piste{137-perfect-complexes-universal-sigma-exact}]\nonverifie Soient $\mathcal P$ la catégorie $k$-linéaire des complexes bornés de $k$-modules libres de type fini, $\Sigma$ les suites exactes courtes scindées degré par degré et $\mathbb C^\bullet$ le complexe des disques. Pour toute catégorie $\mathcal B$ $k$-additive karoubienne munie d'une classe $\Sigma$ de suites exactes où tout morphisme a un $\Sigma$-noyau, $F \mapsto F(\mathbb C^\bullet)$ est une équivalence entre les foncteurs $k$-linéaires $\mathcal P \to \mathcal B$ qui envoient $\Sigma$ sur des suites exactes à gauche et les complexes de cochaînes de $\mathcal B$ ; les foncteurs $\Sigma$-exacts y correspondent aux $\Sigma$-résolutions. \end{theoreme*} \end{encadre} {\small L'encadré suit la forme de la page~55 ; la page~50 hésite et biffe \q{équivalence} pour \q{pleinement fidèle}. Les feuillets en esquissent une démonstration incomplète : les propositions 1 à 3 et la preuve des pages 52 à 55 sont en formules, et la page~52 note en marge \q{il faut condition de platitude ?}. La pleine fidélité, première moitié de a) et forme retenue par la page~50, est vérifiée en Lean et énoncée ci-dessous ; l'essentielle surjectivité (seconde moitié de a), là où servent les noyaux de $\mathcal B$) l'est aussi, pour $\mathcal B$ munie de noyaux et de sommes directes finies, dans le troisième encadré ; la forme karoubienne à classe $\Sigma$ de l'énoncé et b) ne le sont pas.\par} \begin{encadre} \begin{theoreme*}[Grothendieck, pages 40 et 50 à 55, la pleine fidélité\piste{137-perfect-complexes-universal-sigma-exact}]\verifie{Folder137} Soient $k$ un anneau commutatif, $\mathcal P$ la catégorie des complexes de chaînes de $k$-modules libres de type fini, en degrés $\geqslant 0$ et nuls en grand degré, $\Sigma$ la classe des suites $0 \to L' \to L \to L'' \to 0$ exactes en chaque degré, et $\mathbb C^\bullet$ le complexe des disques, $\mathbb C^n = (k \xrightarrow{\mathrm{id}} k)$ en degrés $n+1$, $n$. Alors : \begin{enumerate} \item (proposition~1, page~40) $\mathrm{End}(\mathbb C^n) = k \cdot \mathrm{id}$, $\mathrm{Hom}(\mathbb C^n, \mathbb C^{n+1}) = k \cdot d^n$, et $\mathrm{Hom}(\mathbb C^n, \mathbb C^j) = 0$ pour $j \notin \{n, n+1\}$ ; en particulier $d^{n+1} d^n = 0$ ; \item pour toute catégorie $k$-linéaire $\mathcal B$, sans hypothèse de noyaux, le foncteur $F \mapsto F(\mathbb C^\bullet)$, des foncteurs $k$-linéaires $\mathcal P \to \mathcal B$ qui envoient chaque suite de $\Sigma$ sur un diagramme noyau $0 \to F(L') \to F(L) \to F(L'')$ vers les complexes de cochaînes de $\mathcal B$, est pleinement fidèle. \end{enumerate} \end{theoreme*} \end{encadre} {\small \emph{Démonstration.} (1) Un morphisme $f : \mathbb C^n \to X$ est déterminé par l'image du générateur $1$ en degré $n+1$, sa composante de degré $n$ s'en déduisant par la différentielle ; dans $\mathbb C^j$ cette image vit dans $(\mathbb C^j)_{n+1}$, qui vaut $k$ pour $j = n$ (sommet) ou $j = n+1$ (base) et $0$ sinon. (2) Tout $L$ s'insère dans une suite de $\Sigma$ \[ \begin{gathered} 0 \to L \xrightarrow{\iota} I(L) \xrightarrow{\pi} L[1] \to 0, \qquad I(L)_m = L_m \oplus L_{m-1},\\ d(a, b) = (b, 0),\quad \iota(a) = (a, da),\quad \pi(a, b) = b - da, \end{gathered} \] où $I(L)$, le cône de l'identité, est somme finie de disques : si $(b)$ parcourt une base de chaque $L_n$, $\sum_{n, b} p_{n,b}\, e_{n,b} = \mathrm{id}_{I(L)}$, avec $e_{n,b} : \mathbb C^n \to I(L)$ envoyant le générateur sur $(0, b)$ et $p_{n,b} : I(L) \to \mathbb C^n$ donné par la coordonnée $b^*$. Soient $F$, $G$ deux foncteurs comme dans l'énoncé et $\varphi : F(\mathbb C^\bullet) \to G(\mathbb C^\bullet)$ un morphisme de complexes. Par (1), $\varphi$ commute à toute flèche entre disques, $c\cdot\mathrm{id}$, $c \cdot d^n$ ou $0$, puisque $F$ et $G$ sont $k$-linéaires. On pose $\Phi_{I(L)} = \sum_{n,b} G(e_{n,b})\,\varphi_n\,F(p_{n,b})$ ; en insérant les deux décompositions de l'identité, $\Phi$ commute à toute flèche $I(L) \to I(M)$ et à toute flèche $\mathbb C^n \to I(M)$. Comme $G$ envoie la suite ci-dessus sur un diagramme noyau, $G(\iota)$ est un monomorphisme noyau de $G(\pi)$ ; la flèche $\Phi_{I(L)} F(\iota)$ est tuée par $G(\pi)$, car après le monomorphisme $G(\iota_{L[1]})$ elle devient $\Phi_{I(L[1])} F(\iota_{L[1]} \pi \iota) = 0$. Elle se relève donc en $\eta_L : F(L) \to G(L)$. La naturalité de $\eta$ vient de $\iota_M g = I(g)\,\iota_L$, où $I(g) = g \oplus g$ ; on a $\eta_{\mathbb C^n} = \varphi_n$ en appliquant la commutation de $\Phi$ à $\iota : \mathbb C^n \to I(\mathbb C^n)$. C'est la plénitude. La fidélité suit de même : une transformation $\eta$ vaut $\Phi$ sur $I(L)$ par la décomposition, puis est déterminée sur $L$ par le monomorphisme $G(\iota)$. Le doute marginal de la page~52 (\q{il faut condition de platitude ?}) ne se pose pas pour cette moitié : on n'y utilise ni noyaux dans $\mathcal B$, ni platitude, ni la caractérisation par récurrence sur la longueur des pages 53 et 54, que la suite du cône remplace. Lean (\href{\leanblob/Folder137.lean}{\texttt{Folder137.\allowbreak{}lean}}) définit $\mathcal P$ (\texttt{Perf}), les disques (\texttt{disc}, \texttt{dmap}, \texttt{univ}), $\Sigma$ (\texttt{IsSigma}) et les foncteurs $\Sigma$-exacts à gauche (\texttt{SigmaLeftExact}, \texttt{Lex}), et démontre (1) (\texttt{disc\_endo}, \texttt{disc\_succ}, \texttt{disc\_zero}), la suite du cône et sa décomposition (\texttt{isSigma\_cone}, \texttt{total}) et (2) (\texttt{\(\rho\)FullyFaithful}, avec \texttt{discNat}, \texttt{phi\_nat}, \texttt{extend}). L'essentielle surjectivité fait l'objet de l'encadré suivant ; ne sont pas démontrés la partie b), les propositions 2 et 3 (pages 42 à 44) et la version cosimpliciale des pages 45 et 46.\par} \begin{encadre} \begin{theoreme*}[Grothendieck, pages 50 à 55, l'essentielle surjectivité\piste{137-perfect-complexes-universal-sigma-exact}]\verifie{Folder137} Avec les notations de l'encadré précédent, soit $\mathcal B$ une catégorie $k$-linéaire munie de noyaux et de sommes directes finies. Pour tout complexe de cochaînes $C^\bullet$ de $\mathcal B$, il existe un foncteur $k$-linéaire $\sigma(C^\bullet) : \mathcal P \to \mathcal B$, qui envoie chaque suite de $\Sigma$ sur un diagramme noyau, tel que $\sigma(C^\bullet)(\mathbb C^\bullet) \simeq C^\bullet$. Par conséquent $F \mapsto F(\mathbb C^\bullet)$ est une équivalence de catégories. \end{theoreme*} \end{encadre} {\small \emph{Démonstration.} Pour un objet $T$ de $\mathcal B$, $M^\bullet = \mathrm{Hom}(T, C^\bullet)$ est un complexe de $k$-modules ; soit $\Phi_T(L) \subset \prod_n L_n \otimes_k M^n$ l'ensemble des familles $(z_n)$ telles que $(1 \otimes d)\, z_n = (d \otimes 1)\, z_{n+1}$ dans $L_n \otimes M^{n+1}$. Comme $L_n \otimes M = \mathrm{Hom}_k(L_n^\vee, M)$ pour $L_n$ libre de type fini, ce sont les morphismes de complexes $L^\vee \to M^\bullet$, c'est-à-dire les cycles de degré $0$ de $\underline{\mathrm{Hom}}^\bullet_k(L^\bullet, C^\bullet)$ vus à travers $T$ ; on définit $\sigma(C^\bullet)(L)$ comme un objet qui représente $T \mapsto \Phi_T(L)$. (i) $\Phi_T$ est exact à gauche sur $\Sigma$ : une suite de $\Sigma$ est scindée en chaque degré, $L''_n$ étant libre, donc reste exacte après $- \otimes_k M^n$ ; un élément de $\Phi_T(L)$ tué dans $\Phi_T(L'')$ provient d'un unique élément de $\Phi_T(L')$, la condition de cycle se transportant par injectivité. (ii) Le disque $\mathbb C^n$ est représenté par $C^n$ : un cycle de $\mathbb C^n$ est déterminé par sa composante de degré $n$, $x \in \mathrm{Hom}(T, C^n)$, celle de degré $n+1$ valant $dx$ ; par cette identification, $d^n$ correspond à la différentielle de $C^\bullet$. (iii) $I(L)$ est représenté par la somme directe finie $\bigoplus_{n,b} C^n$, car à la relation $\sum_{n,b} p_{n,b}\, e_{n,b} = \mathrm{id}$ s'ajoute l'orthogonalité $p_{m,c}\, e_{n,b} = \delta_{(n,b),(m,c)}$. (iv) $L$ est représenté par le noyau de la flèche $\sigma(I(L)) \to \sigma(I(L[1]))$ qui représente $I(L) \xrightarrow{\pi} L[1] \xrightarrow{\iota} I(L[1])$, par (i) appliqué aux suites du cône de $L$ et de $L[1]$. Les flèches de $\sigma(C^\bullet)$ s'obtiennent par Yoneda ; la $k$-linéarité et l'exactitude à gauche sur $\Sigma$ se lisent sur $\Phi$, et $\sigma(C^\bullet)(\mathbb C^n) \simeq C^n$, compatiblement aux différentielles, parce que deux objets qui représentent le même foncteur sont isomorphes. Il n'y a pas de récurrence sur la longueur ni de platitude. Les sommes directes finies sont nécessaires en plus des noyaux que nomme la page~50 : un foncteur $k$-linéaire envoie $\mathbb C^0 \oplus \mathbb C^0$ sur une somme directe $F(\mathbb C^0) \oplus F(\mathbb C^0)$, qui n'existe pas dans la sous-catégorie pleine $\{0, k\}$ des $k$-espaces vectoriels ($k$ un corps), laquelle a des noyaux ; le complexe réduit à $k$ en degré $0$ n'y est donc pas de la forme $F(\mathbb C^\bullet)$ (argument de l'édition, non formalisé). Lean (\href{\leanblob/Folder137.lean}{\texttt{Folder137.\allowbreak{}lean}}) définit $\Phi$ (\texttt{Phi}, \texttt{PhiMap}, \texttt{PhiPre}) et la représentabilité (\texttt{Rep}), et démontre (i) (\texttt{PhiMap\_injective}, \texttt{PhiMap\_exact}), (ii) (\texttt{discRep}, \texttt{discRep\_d}), (iii) (\texttt{eDec\_pDec\_self}, \texttt{eDec\_pDec\_ne}, \texttt{coneRep}) et (iv) (\texttt{kerRep}) ; il en tire $\sigma(C^\bullet)$ (\texttt{\(\sigma\)Fun}, \texttt{\(\sigma\)\_sigmaLeftExact}, \texttt{\(\sigma\)Lex}), l'isomorphisme $\sigma(C^\bullet)(\mathbb C^\bullet) \simeq C^\bullet$ (\texttt{\(\sigma\)Iso}) et, avec \texttt{\(\rho\)FullyFaithful}, l'équivalence (\texttt{\(\rho\)Equivalence}). Ne sont pas démontrés : la forme karoubienne à classe $\Sigma$ de suites exactes de $\mathcal B$ du premier encadré, la partie b), les propositions 2 et 3 (pages 42 à 44) et la version cosimpliciale des pages 45 et 46.\par} \begin{encadre} \begin{conjecture*}[Grothendieck, pages 16 à 18, un site $p$-adique sans puissances divisées\piste{7-noninfinitesimal-site}] Soit $X_0$ un schéma sur un corps parfait $k$ de caractéristique $p$. La cohomologie du site des $W$-schémas formels affines $p$-adiquement complets $\operatorname{Spf} B$ munis d'une surjection $B \to A_0$ sur l'anneau d'un ouvert affine de $X_0$, de noyau nilpotent modulo $p$, sans puissances divisées ni surconvergence, est une cohomologie $p$-adique : elle redonne la cohomologie de Washnitzer--Monsky pour $X_0$ lisse affine, et $H_{\mathrm{DR}}(X/W)$ modulo la torsion quand $X_0$ a un relèvement propre et lisse $X$. \end{conjecture*} \end{encadre} {\small Mathlib n'a pas de cohomologie $p$-adique des schémas. On se reportera aux notes de Grothendieck (\lot{7}{1}{16}).\par} \begin{encadre} \begin{theoreme*}[Grothendieck, pages 74 à 83, catégories polynomiales\piste{137-polynomial-categories-pd-tensor-categories}]\nonverifie Les catégories polynomiales strictes, catégories à produits finis munies d'une sous-catégorie additive de flèches de degré un et d'une graduation des $\mathrm{Hom}$ par l'homogénéité sous les scalaires, sont équivalentes aux $\otimes$-pd-catégories, catégories monoïdales symétriques additives munies d'un foncteur gradué exponentiel $\Gamma^*$ et de flèches $\alpha_{p,q} : \Gamma^{pq} \to \Gamma^p\Gamma^q$ ; le passage inverse est $\mathbf P_p(X, Y) = \mathrm{Hom}(\Gamma^p X, Y)$. \end{theoreme*} \end{encadre} {\small La page~83 affirme l'équivalence sans la démontrer : \q{Les deux notions sont donc équivalentes}. Mathlib n'a aucune des deux notions. L'équivalence complète, avec les produits, l'additivité, les multidegrés, le produit tensoriel strict et la formule exponentielle, n'est pas vérifiée en Lean ; son c\oe ur, la partie qui porte le passage inverse $\mathbf P_p(X, Y) = \mathrm{Hom}(\Gamma^p X, Y)$ et la règle de composition, l'est, et il est énoncé ci-dessous. On se reportera aux notes de Grothendieck (\lot{137}{4}{74}).\par} \begin{encadre} \begin{theoreme*}[D'après les pages 77 à 83, forme réduite par l'édition, le c\oe ur de l'équivalence\piste{137-polynomial-categories-pd-tensor-categories}]\verifie{Folder137} Soit $\mathcal C$ une catégorie, celle des flèches de degré un. Appelons \emph{catégorie polynomiale sur $\mathcal C$} la donnée d'ensembles $\mathbf P_n(X, Y)$, d'une composition $\mathbf P_p(X, Y) \times \mathbf P_q(Y, Z) \to \mathbf P_{qp}(X, Z)$ associative, d'identités de degré un, et d'une bijection $\mathrm{Hom}_{\mathcal C}(X, Y) \simeq \mathbf P_1(X, Y)$ compatible à la composition ; elle est \emph{représentable} si chaque foncteur $Y \mapsto \mathbf P_n(X, Y)$ sur $\mathcal C$ est représenté par un objet $\Gamma^n X$ et une flèche universelle $\gamma_n \in \mathbf P_n(X, \Gamma^n X)$. Appelons \emph{structure à puissances divisées sur $\mathcal C$} la donnée de foncteurs $\Gamma^n : \mathcal C \to \mathcal C$, de transformations naturelles $\alpha_{p,q} : \Gamma^{pq} \to \Gamma^p\Gamma^q$, d'un isomorphisme $\varepsilon : \Gamma^1 \simeq \mathrm{id}$, satisfaisant le carré d'associativité de la page~80 et les conditions d'unité $(**)$. Alors : \begin{enumerate} \item d'une structure à puissances divisées, $\mathbf P_p(X, Y) = \mathrm{Hom}(\Gamma^p X, Y)$ avec $g \circ f = g \circ \Gamma^q(f) \circ \alpha_{q,p}$ fait une catégorie polynomiale représentable, par $\Gamma^n X$ et $\gamma_n = \mathrm{id}$ ; si $\mathcal C$ est additive, cette composition est additive en $g$ ; \item d'une catégorie polynomiale représentable, les $\Gamma^n$ sont des foncteurs, les $\alpha_{p,q}$ définis par la factorisation de $\gamma_p \circ \gamma_q$ sont naturels, $\Gamma^1 \simeq \mathrm{id}$, et le carré de la page~80 et $(**)$ sont vrais ; \item les deux passages sont inverses l'un de l'autre : le premier suivi du second redonne exactement $\Gamma$, $\alpha$ et $\varepsilon$ ; le second suivi du premier redonne la catégorie polynomiale de départ à isomorphisme près, par $\varphi \mapsto \varphi \circ \gamma_p$. \end{enumerate} \end{theoreme*} \end{encadre} {\small \emph{Démonstration.} Une structure à puissances divisées est une comonade graduée par le monoïde multiplicatif $(\mathbf N, \cdot)$, et la catégorie polynomiale qu'elle définit en est la catégorie de Kleisli. (1) L'associativité de la composition des pages~81 et~82 est ce qui demande la naturalité de $\alpha$ : dans $h \circ (g \circ f)$ et $(h \circ g) \circ f$, on fait passer $\Gamma^{rq}(f)$ à travers $\alpha_{r,q}$ par naturalité, et il reste à comparer $\alpha_{r,q} \circ \alpha_{rq,p}$ et $\Gamma^r(\alpha_{q,p}) \circ \alpha_{r,qp}$, qui est le carré de la page~80. Les unités sont $(**)$ et la naturalité de $\varepsilon$. La représentabilité est immédiate : $\varphi \circ \gamma_n = \alpha_{1,n} \circ \varepsilon \circ \varphi = \varphi$, par $(**)$. (2) Tout se lit à travers la bijection $\varphi \mapsto \varphi \circ \gamma_n$ de $\mathrm{Hom}(\Gamma^n X, Y)$ sur $\mathbf P_n(X, Y)$ : on définit $\Gamma^n(f)$ par $\Gamma^n(f) \circ \gamma_n = \gamma_n \circ f$, $\alpha_{p,q}$ par $\alpha_{p,q} \circ \gamma_{pq} = \gamma_p \circ \gamma_q$ (la page~80 : \q{ce qui revient au même}), et $\varepsilon$ par $\varepsilon \circ \gamma_1 = \mathrm{id}$. Chaque identité à démontrer, fonctorialité, naturalité, carré, unités, devient après composition avec le $\gamma$ convenable une égalité entre composés de $\gamma$, qui découle de l'associativité de $\mathbf P$ ; par exemple les deux côtés du carré deviennent $\gamma_p \circ \gamma_q \circ \gamma_r$, parenthésé de deux façons. L'inverse de $\varepsilon$ est la flèche de degré un qui correspond à $\gamma_1$. (3) Dans le premier passage, $\varphi \mapsto \varphi \circ \gamma_n$ est l'identité ; le second passage reconstruit donc $\Gamma$, $\alpha$ et $\varepsilon$ à partir de $\gamma_n = \mathrm{id}$, et les retrouve par $(**)$. Dans l'autre sens, la bijection $\varphi \mapsto \varphi \circ \gamma_p$ envoie $g \circ \Gamma^q(f) \circ \alpha_{q,p}$ sur $(g \circ \gamma_q) \circ (f \circ \gamma_p)$, par le même calcul. Rien n'utilise l'additivité, le produit tensoriel ni la formule exponentielle : le c\oe ur de l'équivalence vaut pour une catégorie $\mathcal C$ quelconque, et la règle de composition de la page~82 est forcée par la représentabilité. Les degrés sont portés par une équation $pq = n$, ce qui évite toute conversion d'indices. Lean (\href{\leanblob/Folder137.lean}{\texttt{Folder137.\allowbreak{}lean}}) définit les deux notions (\texttt{PDCategory}, \texttt{PolynomialCategory}, \texttt{PolynomialCategory.\allowbreak{}Representation}) et démontre (1) (\texttt{PDCategory.\allowbreak{}toPoly}, \texttt{PDCategory.\allowbreak{}representation}, \texttt{PDCategory.\allowbreak{}toPoly\_comp\_add}), (2) (\texttt{Representation.\allowbreak{}toPD}) et (3) (\texttt{PDCategory.\allowbreak{}toPD\_representation\_\(\Gamma\)\_map}, \texttt{PDCategory.\allowbreak{}toPD\_representation\_\(\alpha\)}, \texttt{PDCategory.\allowbreak{}toPD\_representation\_\(\varepsilon\)}, \texttt{Representation.\allowbreak{}toPDToPolyIso}) ; un modèle trivial, tous les $\Gamma^n$ égaux à l'identité, montre que les axiomes sont compatibles (\texttt{PDCategory.\allowbreak{}trivial}). Les axiomes a) à c) font l'objet de l'encadré suivant, et ce que Mathlib atteint de l'exemple des $k$-modules du second. Ne sont pas démontrés : la décomposition d) par multidegrés et l'homogénéité sous les scalaires, f) et g), la moitié $\mathbf 1 \simeq \Gamma^q(\mathbf 1)$ de $(***)$, le produit tensoriel strict, la formule exponentielle $\Gamma^*(X \oplus Y) \simeq \Gamma^*X \otimes \Gamma^*Y$ et, dans l'exemple des $k$-modules, le théorème de Roby.\par} \begin{encadre} \begin{theoreme*}[D'après la page 74, forme graduée par l'édition, les axiomes a) à c)\piste{137-polynomial-categories-pd-tensor-categories}]\verifie{Folder137} Soit $\mathbf P$ une catégorie polynomiale représentable sur $\mathcal C$, au sens de l'encadré précédent. Si $\mathcal C$ a des produits binaires, alors pour tout $n$ les projections, de degré un, font de $X \times Y$ un produit dans chaque $\mathbf P_n$ : $\mathbf P_n(W, X \times Y) \simeq \mathbf P_n(W, X) \times \mathbf P_n(W, Y)$, et en degré un c'est l'accouplement de $\mathcal C$ ; l'objet final de $\mathcal C$ est final dans chaque $\mathbf P_n$. Si de plus $\mathcal C$ est préadditive, la loi $f + g = m \circ (f, g)$, où $m = \mathrm{pr}_1 + \mathrm{pr}_2 : X \times X \to X$ est de degré un, est une loi de groupe abélien sur $\mathbf P_n(W, X)$, qui prolonge l'addition de $\mathcal C$ en degré un, et \[ (f + g) \circ h = f \circ h + g \circ h \] pour $h$ de degré quelconque. Pour la catégorie polynomiale d'une structure à puissances divisées, c'est l'addition de $\mathrm{Hom}(\Gamma^n W, X)$. \end{theoreme*} \end{encadre} {\small \emph{Démonstration.} Tout passe encore par la bijection $\varphi \mapsto \varphi \circ \gamma_n$ de $\mathrm{Hom}(\Gamma^n W, Y)$ sur $\mathbf P_n(W, Y)$, qui transforme la composition à droite par une flèche $u$ de degré un en $u \circ -$. (a) Les composantes de $\varphi \circ \gamma_n$ sont donc $(\mathrm{pr}_1 \varphi) \circ \gamma_n$ et $(\mathrm{pr}_2 \varphi) \circ \gamma_n$ : l'application $a \mapsto (\mathrm{pr}_1 \circ a, \mathrm{pr}_2 \circ a)$ est, à travers ces bijections, la propriété universelle du produit dans $\mathcal C$, d'où la bijection. De même pour l'objet final. (b) Par la même bijection, $m \circ (\varphi \gamma_n, \psi \gamma_n) = m (\varphi, \psi) \circ \gamma_n = (\varphi + \psi) \circ \gamma_n$ : la loi $m \circ (f, g)$ est celle de $\mathrm{Hom}(\Gamma^n W, X)$ transportée, donc une loi de groupe abélien ; en degré un, $(\iota f, \iota g) = \iota (f, g)$ et $m \circ (f, g) = f + g$. (c) Pour $h$ de degré $p$, les composantes de $(f, g) \circ h$ sont $f \circ h$ et $g \circ h$ par associativité, d'où $(f, g) \circ h = (f \circ h, g \circ h)$ par (a), puis $m \circ (f, g) \circ h = (f \circ h) + (g \circ h)$. La page tire de a) à c) que $\mathbf P(X, Y)$ est un groupe abélien, \q{fonctoriel en $X$ par des homomorphismes, mais pas en $Y$} : c'est (c), et la composition n'est pas additive en $h$ parce que $\Gamma^q$ n'est pas additif. Lean (\href{\leanblob/Folder137.lean}{\texttt{Folder137.\allowbreak{}lean}}) démontre (a) (\texttt{PolynomialCategory.\allowbreak{}pairMap\_bijective}, \texttt{pairMap\_\(\iota\)}, \texttt{terminal\_unique}), (b) (\texttt{PolynomialCategory.\allowbreak{}add\_eq}, \texttt{\(\iota\)\_add}, \texttt{PDCategory.\allowbreak{}add\_eq}) et (c) (\texttt{PolynomialCategory.\allowbreak{}comp\_add}). Le tout est démontré degré par degré : la catégorie totale $\mathbf P(X, Y) = \bigoplus_n \mathbf P_n(X, Y)$ n'est pas construite, car composer une somme de flèches de degrés différents demande $\Gamma^q$ d'une telle somme, et les multidegrés de d) ne sont pas formalisés.\par} \begin{encadre} \begin{theoreme*}[D'après les pages 80 et 84, l'exemple des $k$-modules, ce que Mathlib atteint\piste{137-polynomial-categories-pd-tensor-categories}]\verifie{Folder137} Soient $k$ un anneau commutatif, $M$ un $k$-module et $\Gamma(M)$ son algèbre à puissances divisées, engendrée par les $m^{[n]}$. Pour toute application linéaire $\varphi : \Gamma(M) \to N$, l'application $m \mapsto \varphi(m^{[n]})$ est homogène de degré $n$, $\varphi((\lambda m)^{[n]}) = \lambda^n \varphi(m^{[n]})$, et sa composée avec une application linéaire $f : M' \to M$ est $(\varphi \circ \Gamma(f))((-)^{[n]})$. L'application $m \mapsto (m^{[q]})^{[p]}$ de $M$ dans $\Gamma(\Gamma(M))$, image de $m^{[pq]}$ par $\alpha_{p,q}$, est homogène de degré $pq$. Enfin $m \mapsto m^{[1]}$ est additive. \end{theoreme*} \end{encadre} {\small \emph{Démonstration.} C'est la relation $(\lambda m)^{[n]} = \lambda^n m^{[n]}$ de $\Gamma(M)$, appliquée une fois, puis deux fois avec $(\lambda^q)^p = \lambda^{pq}$ ; la fonctorialité est $\Gamma(f)(m^{[n]}) = f(m)^{[n]}$, et l'additivité de $m \mapsto m^{[1]}$ vient de $(x + y)^{[1]} = x^{[1]} y^{[0]} + x^{[0]} y^{[1]}$. Lean (\href{\leanblob/Folder137.lean}{\texttt{Folder137.\allowbreak{}lean}}, à partir de \texttt{DividedPowerAlgebra} de Mathlib) démontre \texttt{Modules.\allowbreak{}dp\_comp\_smul}, \texttt{Modules.\allowbreak{}dp\_comp\_map}, \texttt{Modules.\allowbreak{}dp\_dp\_smul} et \texttt{Modules.\allowbreak{}dp\_one\_add}. Ne sont pas démontrés : la graduation $\Gamma(M) = \bigoplus_n \Gamma^n M$, absente de Mathlib, la flèche $\alpha_{p,q} : \Gamma^{pq} M \to \Gamma^p \Gamma^q M$ elle-même, dont la définition demande la propriété universelle de $\Gamma^{pq} M$ pour les lois polynômes, le théorème de Roby $\mathrm{Hom}(\Gamma^p M, N) \simeq$ lois polynômes homogènes de degré $p$, et donc que les $k$-modules forment une $\otimes$-pd-catégorie.\par}