\section[Cote 2 : une classe non nulle de classe de Chern totale triviale]{Cote 2 : une classe non nulle de classe de Chern totale triviale\protect\verifie{Folder2}}\label{sec:2}

Cette partie suit le groupe de Grothendieck $K(X)$ d'une variété $X$. On y range les faisceaux cohérents sous une seule règle : une suite exacte $0 \to E' \to E \to E'' \to 0$ donne $[E] = [E'] + [E'']$ ; le produit tensoriel en fait un anneau. Les classes de Chern traduisent une classe de $K(X)$ en classes de cycles : la classe de Chern totale $c(x) = 1 + c_1(x) + c_2(x) + \cdots$, dans l'anneau de Chow $A(X)$, vérifie $c(x + y) = c(x)\,c(y)$ et vaut $1 + c_1(L)$ pour un fibré en droites~$L$. Le théorème de Riemann--Roch de Grothendieck dit comment se comporte par image directe le caractère de Chern, version additive de $c$ qui demande des coefficients rationnels. La cote~2 garde les classes de Chern entières, et le prix se lit dans le facteur $(r-1)!$ des énoncés ci-dessous. La cote~47 (partie \q{Variétés abéliennes et schémas de Picard}) applique le théorème à l'addition $m_A$ et à la projection $\mathrm{pr}_2$ d'un schéma abélien, à côté de l'inversion de Fourier relative, qui est le théorème~1.1 de Mukai (1987) \cite{mukai1987}. La cote~153 (section~\ref{sec:153}) revient aux $\lambda$-anneaux, le cadre algébrique de $K(X)$ et de ses opérations, par les polynômes à valeurs entières. Le théorème de Riemann--Roch lui-même n'est vérifié en Lean nulle part dans cette annexe : mathlib n'a ni $K(X)$ ni les classes de Chern, et les sections~\ref{sec:2} et~\ref{sec:153} démontrent l'algèbre de quelques calculs, dans des modèles explicites.

La cote 2, \emph{Théorème de Riemann-Roch}, notes que l'inventaire dit antérieures à 1958, calcule aux pages~9 à~13 la classe de Chern de l'image directe par l'immersion $i : X \to X \times \mathbf P^r$ d'une section constante (\lot{2}{1}{9}). Dans $K(\mathbf P^r) = \mathbf Z[\xi]/(\xi^{r+1})$, $\xi = 1 - L^{-1}$, la classe d'un point est $\xi^r = \sum_i (-1)^i \binom ri L^{-i}$, et $c(L^{-i}) = 1 - i\eta$, où $\eta$ est la classe d'un hyperplan. Lean démontre l'algèbre des deux pages, dans le modèle du principe de scindage que suit la lecture : $i_!(\mathcal O_Y) = \sum_i (-1)^i\binom ri\bigl([L^{-i}] - [L^{-i} \otimes \mathcal O(-Y)]\bigr)$ et $c(L^{-i} \otimes \mathcal O(-Y)) = 1 - y - i\eta$, avec $y = x'$. Une congruence modulo $\eta^{r+1}$ dans $A[[\eta]]$ est une égalité dans $A[\eta]/(\eta^{r+1})$.

Le premier énoncé calcule la classe de Chern totale du faisceau d'un point de $\mathbf P^r$. Pour $r = 1$ on trouve $1 + \eta$, pour $r = 2$, $1 - \eta^2$, et pour $r = 3$, $1 + 2\eta^3$ : le coefficient $(r-1)!$ grandit avec la dimension. Le second en tire une conséquence : si la classe $y$ du diviseur $Y$ est tuée par $(r-1)!$, le terme correctif disparaît, et l'image directe $i_!(\mathcal O_Y)$ a pour classe de Chern totale~$1$. Si cette classe est non nulle dans $K$, elle échappe entièrement aux classes de Chern entières ; c'est l'énoncé encadré plus bas, dont la non-nullité n'est pas vérifiée. Pour $r \leq 2$, le coefficient vaut $\pm 1$, l'hypothèse force $y = 0$, et le phénomène ne se produit pas.

\begin{theoreme}[Grothendieck, page 9, la classe de Chern d'un point\piste{2-trivial-total-chern-class}]\label{thm:2-point}
Soient $r \geq 1$ et $A$ un anneau commutatif. Dans $A[\eta]/(\eta^{r+1})$,
\[
  \prod_{i=0}^{r} (1 - i\eta)^{(-1)^i\binom ri} \;=\; 1 + (-1)^{r-1}(r-1)!\,\eta^r .
\]
\end{theoreme}

\begin{theoreme}[D'après la page 13, la classe de Chern de $i_!(\mathcal O_Y)$]\label{thm:2-immersion}
Soient $r \geq 1$, $A$ un anneau commutatif et $y \in A$ tel que $1 - y$ soit inversible (par exemple $y$ nilpotent) et $(r-1)!\,y = 0$. Dans $A[\eta]/(\eta^{r+1})$,
\[
  \prod_{i=0}^{r} \Bigl(\frac{1 - i\eta}{1 - y - i\eta}\Bigr)^{(-1)^i\binom ri} \;=\; 1 ,
\]
c'est-à-dire $c(i_!(\mathcal O_Y)) = 1$ dans ce modèle.
\end{theoreme}

\noindent Les deux énoncés tiennent tels que la lecture les donne (\texttt{chernPoint}, \texttt{chernImmersion}, dans \href{\leanblob/Folder2.lean}{\texttt{Folder2.\allowbreak{}lean}}). Le premier est démontré sur $\mathbf Z$ par la dérivée logarithmique, au lieu du logarithme de la lecture, puis transporté à tout anneau ; le second en découle, le produit des dénominateurs étant celui des numérateurs où $\eta$ est remplacé par $\eta/(1 - y)$. La page~13 suppose $y$ dans $A^1(X)$ ; seules servent l'inversibilité de $1 - y$ et l'hypothèse $(r-1)!\,y = 0$.

Au bas de la page~13, un \emph{N.B.} donne lui-même l'exemple : $X$ une courbe elliptique d'origine $0$, $a \neq 0$ un point tel que $a + a = 0$, $x = (a) - (0)$ la classe d'un diviseur de degré zéro, et $r = 3$. La page affirme que $y = i_!(x)$ n'est pas nul, et que pourtant \q{les coefficients de la classe de Chern sont nuls}. Dans le même modèle, $x = [\mathcal O_a] - [\mathcal O_0] = [\mathcal O(-0)] - [\mathcal O(-a)]$, et l'on note $p$, $q$ les classes des points $0$ et $a$ dans $A^1(X)$. Sur une courbe, $p^2 = q^2 = 0$, et $a + a = 0$ donne $2(p - q) = 0$.

\begin{theoreme}[Grothendieck, page 13, le \emph{N.B.} : la classe de Chern de $i_!(x)$]\label{thm:2-nb}
Soient $r \geq 1$, $A$ un anneau commutatif et $p, q \in A$ tels que $p^2 = q^2 = 0$ et $r!\,(p - q) = 0$. Dans $A[\eta]/(\eta^{r+1})$,
\[
  \prod_{i=0}^{r} \Bigl(\frac{1 - p - i\eta}{1 - q - i\eta}\Bigr)^{(-1)^i\binom ri} \;=\; 1 .
\]
Pour $r = 3$, l'hypothèse $2(p - q) = 0$ suffit.
\end{theoreme}

\begin{proof}C'est encore le même calcul. Si $u$ est un élément inversible de $A$, le produit des $(u - i\eta)^{(-1)^i\binom ri}$ est celui du théorème~\ref{thm:2-point} où $\eta$ est remplacé par $\eta/u$, les exposants étant de somme nulle ; il vaut donc $1 + (-1)^{r-1}(r-1)!\,u^{-r}\eta^r$. Le quotient des deux produits, pour $u = 1 - p$ et $v = 1 - q$, vaut $1$ dès que $(r-1)!\,(u^{-r} - v^{-r}) = 0$. Comme $p^2 = 0$, $(1 - p)^{-1} = 1 + p$ et $(1 + p)^r = 1 + rp$, de sorte que $(r-1)!\,(u^{-r} - v^{-r}) = r!\,(p - q)$. Pour $r = 3$, $r! = 6 = 3 \cdot 2$.\end{proof}

\noindent Voir \texttt{chernRatio}, \texttt{chernCurve} et \texttt{chernEllipticNB} dans \href{\leanblob/Folder2.lean}{\texttt{Folder2.\allowbreak{}lean}}.

\begin{encadre}
\begin{theoreme*}[Grothendieck, page 13, une classe non nulle de classe de Chern totale~$1$]\nonverifie
Soient $X$ une courbe elliptique d'origine $0$, $a \neq 0$ un point tel que $a + a = 0$, et $x = (a) - (0) \in K(X)$. La classe $y = i_!(x)$ est non nulle dans $K(X \times \mathbf P^3)$, et sa classe de Chern totale vaut~$1$. Plus généralement, si $Y \subset X$ est un diviseur dont la classe $x' \in A^1(X)$ est non nulle mais tuée par $(r-1)!$, la classe $i_!(\mathcal O_Y)$ est non nulle et de classe de Chern totale~$1$. (L'hypothèse \q{tuée par $(r-1)!$} ne s'énonce utilement que pour $r \geq 3$, mais elle n'est pas nécessaire : le calcul de \nolinkurl{computations/chern-trivial-2} donne $c(i_!x) = 1 + (-1)^{r-1} r!\,(p-q)\,\eta^r$, si bien que pour $a$ d'ordre~$2$ la classe est déjà triviale pour $r = 2$.)
\end{theoreme*}
\end{encadre}
{\small La partie qui porte sur les classes de Chern est démontrée plus haut, dans le modèle du principe de scindage. La non-nullité des classes et la restriction $r \geq 3$ relèvent de la géométrie : $y$ n'est pas nul parce que $c^1(x) = q - p$ ne l'est pas et que $i_!$ est injectif, ce que la page affirme sans le démontrer. Le second énoncé est celui de la \q{Conséquence} qui ouvre la page ; ce bloc est encadré et barré d'une longue oblique, alors que le \emph{N.B.} ne l'est pas. Le dernier membre de la formule de la \q{Conséquence} est écrit~$0$ là où la classe totale vaut~$1$ ; le \emph{N.B.} dit la même chose en parlant des coefficients. La page nomme aussi la classe $[\mathcal O_{Y \times \mathbf P^r}]$ là où le calcul porte sur $Y \times \{\text{point}\}$. Mathlib n'a pas le groupe $K$ des faisceaux cohérents ni les classes de Chern. On se reportera aux notes de Grothendieck (\lot{2}{1}{9}).\par}

La page~21 pose une question sur deux anneaux attachés à un $\lambda$-anneau $K$ muni d'éléments \q{géométriques} (\lot{2}{2}{21}). L'anneau de Chern $CK$ est engendré par des symboles $c^i(x)$, soumis aux règles que vérifient les classes de Chern : formule de Whitney, produit, et $c^i(E) = 0$ au-delà du rang pour un élément géométrique $E$. L'anneau $GK$ est le gradué de $K$ pour la filtration $\gamma$. Une flèche $\varphi_K : CK \to GK$ envoie $c^i(x)$ sur la classe de $\gamma^i(x - \varepsilon(x))$. La page énonce que $\varphi_K$ est toujours surjective et que son noyau est un groupe de torsion, de sorte qu'elle devient bijective après tensorisation par $\mathbf Q$. Elle demande ensuite si $\varphi_K$ est toujours bijective, répond \q{Non}, et donne l'exemple de $K = K(\mathbf P^{n-1}) = \mathbf Z[L]/(L - 1)^n$, avec $L$ pour seul élément géométrique : la relation $(L-1)^n = 0$ n'impose à $CK$ que $(n-1)!\,\zeta^n = 0$ en degré~$n$, de sorte que \q{si $n - 1 > 1$, i.e.\ $n \geq 3$, $CK$ a de la torsion}, alors que $GK$ est sans torsion.

Dans cet exemple, $CK$ est engendré par $\zeta = c^1(L)$. On pose $\xi = 1 - L^{-1}$ ; comme $L$ est inversible, $\xi^n = 0$ équivaut à $(L - 1)^n = 0$. Avec $c(L^{-i}) = 1 - i\zeta$, la seule relation est $c(\xi^n) = 1$, c'est-à-dire l'annulation des composantes de degré $\geq 1$ de
\[
c(\xi^n) = \prod_{i=0}^{n} (1 - i\zeta)^{(-1)^i \binom ni} = 1 + (-1)^{n-1}(n-1)!\,\zeta^n + \cdots,
\]
le produit de la page~9 calculé plus haut. On prend donc $CK = \mathbf Z[\zeta]/I$, où $I$ est engendré par les $a_m \zeta^m$, $a_m$ le coefficient de $\zeta^m$ dans ce produit, et $GK = \mathbf Z[\zeta]/(\zeta^n)$. Les $a_m$ sont nuls pour $1 \leq m < n$, de sorte que $I \subset (\zeta^n)$ et que $\varphi_K$ est bien définie.

Pour $n = 3$, la relation de degré~$3$ est $2\zeta^3 = 0$. Pour que $CK$ ait de la torsion, il faut encore que $\zeta^3$ ne soit pas nul dans $CK$ ; la page l'affirme sans le montrer.

\begin{encadre}
\begin{theoreme}[Grothendieck, page 21, cas $n \geq 3$\piste{2-chern-ring-not-injective-pn}]
Pour $n \geq 3$, $\zeta^n$ est non nul dans $CK$ et $(n-1)!\,\zeta^n = 0$ ; $GK$ est sans torsion, et $\varphi_K$ est surjective sans être injective. Pour $n \leq 2$, $\varphi_K$ est bijective.
\end{theoreme}
\end{encadre}

\begin{proof}
L'idéal $I$ est engendré par des monômes $a_m\zeta^m$ avec $m \geq n$, et $a_n = \pm(n-1)!$, d'où $(n-1)!\,\zeta^n = 0$. Pour voir que $\zeta^n \neq 0$, on envoie $\zeta$ sur $h$ dans $T = (\mathbf Z/(n-1)!)[h]/(h^{n+1})$. Les relations y sont satisfaites : $a_m h^m = 0$ pour $m > n$ parce que $h^{n+1} = 0$, et $a_n h^n = 0$ parce que $(n-1)! = 0$ dans $T$. Or $h^n \neq 0$ dans $T$ dès que $(n-1)! > 1$, c'est-à-dire $n \geq 3$. Dans $GK$, si $k f$ est divisible par $\zeta^n$ avec $k \neq 0$, les coefficients de $f$ de degré $< n$ sont nuls. Pour $n \leq 2$, $a_n = \pm 1$, donc $\zeta^n \in I$ et $I = (\zeta^n)$.
\end{proof}

{\sloppy \noindent Voir \texttt{$\varphi$\_not\_injective}, \texttt{$\zeta$\_pow\_ne\_zero}, \texttt{factorial\_mul\_$\zeta$\_pow}, \texttt{GK\_torsionFree}, \texttt{$\varphi$\_bijective\_of\_le\_two} et \texttt{exists\_chern} dans \href{\leanblob/Folder2.lean}{\texttt{Folder2.\allowbreak{}lean}}. L'anneau $T$ répond à la question que laissait la piste : il porte un homomorphisme de Chern avec $c(L) = 1 + h$, $c(\xi^n) = 1$, $h^n \neq 0$ et $(n-1)!\,h^n = 0$. Le cas $n \leq 2$ est de l'édition ; la page n'énonce que $n \geq 3$. L'exemple dépend aussi de la famille géométrique : si l'on déclare géométrique la classe $n - L^{-1}$, de rang $n - 1$, sa classe de Chern $(1 - \zeta)^{-1}$ force $\zeta^n = 0$, et $CK = GK$. La note en diagonale, où se lisent l'idéal, $P(n-1)$ et l'anneau $\mathbf Z[\xi]/\xi^n$, dit sans doute cela ; ce point n'est pas formalisé.\par}

Lean ne vérifie pas que la présentation de $CK$ par $\zeta$ et la seule relation $c(\xi^n) = 1$ découle des relations générales de la page~28 : c'est la réduction que fait la page, reprise par l'édition. Les $\lambda$-anneaux et la filtration $\gamma$ ne sont pas construits. L'image directe $i_!$ et la formule de la page~11 qui donne $c(i_!x)$ ne sont pas formalisées non plus : Lean part du modèle de scindage que suit la lecture.

Pour la question de la page~21, la fiche de la piste relève un travail publié. Mackall (2020) \cite{mackall2020} construit un anneau gradué universel pour les théories de classes de Chern dont la première classe est additive, et le relie au gradué de $K$ pour la filtration $\gamma$ par un théorème de type Grothendieck--Riemann--Roch. Dans sa remarque~4.3 (numérotation arXiv), il donne un exemple de non-injectivité en degré~$3$, pour une approximation finie du classifiant $BO^+(2n+1)$, en s'appuyant sur un théorème de Karpenko et Merkurjev. L'exemple de $K(\mathbf P^{n-1})$ avec $L$ pour seul élément géométrique n'y figure pas. L'énoncé encadré de la page~13 n'a pas encore été confronté à la littérature : sa fiche ne relève aucune source, et l'édition n'en cite pas.
\section[IHÉS SGA\,6 2/3 : le groupe $K$ d'une catégorie triangulée, la formule d'Euler]{IHÉS SGA\,6 2/3 : le groupe $K$ d'une catégorie triangulée, et la formule d'Euler\protect\verifie[\leanblobmain]{IhesSGA6_2_3}}\label{sec:ihes-sga6-2-3}

Comme la section~\ref{sec:ihes-sga6-1-5}, cette section porte sur une pièce du fonds Grothendieck--Illusie de l'IHÉS, \texttt{FG\_IL\_5\_SGA6\_2\_3} (\href{https://repo-archives.ihes.fr/FONDS_GROTHENDIECK_ILLUSIE/}{vue~1}). Ce sont des notes manuscrites de quinze vues, intitulées \q{Groupes $K$}, qui portent en haut de la première \q{(Pour Illusie)} ; le catalogue de l'IHÉS les date \q{1965 ?}. Elles esquissent un exposé sur les groupes $K$ : le groupe d'une catégorie triangulée, sa comparaison avec celui d'une catégorie abélienne, puis une généralisation. Aucune lecture modernisée n'en a été faite : les énoncés ci-dessous sont lus sur la transcription des vues~1 à~3.

\emph{L'idée.} On cherche à mesurer les objets d'une catégorie par des nombres, ou des éléments d'un groupe abélien, de façon additive. Pour les espaces vectoriels de dimension finie, la dimension vérifie $\dim V = \dim V' + \dim V''$ pour toute suite exacte $0 \to V' \to V \to V'' \to 0$. Une \emph{fonction additive} sur une catégorie abélienne est une fonction $\chi$ des objets qui vérifie la même règle, et le groupe $K$ est le réceptacle universel de ces fonctions : le groupe abélien libre sur les objets, divisé par les relations $[V] = [V'] + [V'']$. Dans une catégorie triangulée, comme la catégorie dérivée, les \emph{triangles distingués} $X \to Y \to Z \to X[1]$ jouent le rôle des suites exactes courtes ; une suite exacte courte de complexes donne un tel triangle. Les notes posent donc : $K(\mathcal C)$ est le quotient du groupe abélien libre sur les objets de $\mathcal C$ par le sous-groupe engendré par les $[Y] - [X] - [Z]$, un pour chaque triangle distingué, et $\mathrm{cl}(X)$ est l'image de $X$ (vue~1).

Il faut rappeler ce qu'on demande aux triangles. Une catégorie \emph{prétriangulée} est une catégorie additive munie d'un foncteur de translation $X \mapsto X[1]$, inversible, et d'une classe de triangles $X \to Y \to Z \to X[1]$, dits distingués, telle que : un triangle isomorphe à un triangle distingué est distingué ; pour tout $X$, le triangle $X \xrightarrow{\mathrm{id}} X \to 0 \to X[1]$ est distingué ; tout morphisme $X \to Y$ se complète en un triangle distingué ; $X \to Y \to Z \to X[1]$ est distingué si et seulement si sa rotation $Y \to Z \to X[1] \to Y[1]$ l'est (au signe près) ; enfin un carré commutatif entre deux triangles distingués se complète en un morphisme de triangles. Une catégorie triangulée vérifie de plus l'axiome de l'octaèdre, qui ne sert pas ici.

\begin{encadre}
\begin{enonce}[Notes, vues 1 et 2]
Soit $\mathcal C$ une catégorie triangulée. Dans $K(\mathcal C)$ :
\begin{itemize}
\item $\mathrm{cl}(0) = 0$, et $\mathrm{cl}(X) = \mathrm{cl}(X')$ si $X \simeq X'$ ;
\item $\mathrm{cl}(X[n]) = (-1)^n\,\mathrm{cl}(X)$ pour tout $n \in \mathbf Z$, en particulier $\mathrm{cl}(X[1]) = -\mathrm{cl}(X)$ ;
\item $\mathrm{cl}(X \oplus Y) = \mathrm{cl}(X) + \mathrm{cl}(Y)$ ;
\item (proposition de la vue~2) tout élément de $K(\mathcal C)$ s'écrit $\mathrm{cl}(X)$ pour un objet $X$ ;
\item (fonctorialité) un foncteur exact $\varphi : \mathcal C \to \mathcal C'$ induit un homomorphisme $K(\varphi)$ tel que $K(\varphi)(\mathrm{cl}\,X) = \mathrm{cl}\,\varphi(X)$, et deux foncteurs isomorphes induisent le même.
\end{itemize}
\end{enonce}
\end{encadre}

\noindent Les notes écrivent ces propriétés pour une fonction additive $\chi$ quelconque, en partie dans une accolade ajoutée d'une encre plus foncée en marge de la vue~1 ; la propriété universelle de $K(\mathcal C)$ les transporte à $\mathrm{cl}$, et réciproquement.

\begin{proof}
Chaque égalité vient d'un triangle bien choisi. Le triangle $0 \to 0 \to 0 \to 0$ donne $\mathrm{cl}(0) = \mathrm{cl}(0) + \mathrm{cl}(0)$, d'où $\mathrm{cl}(0) = 0$. Pour un isomorphisme $e : X \to Y$, le triangle $X \xrightarrow{e} Y \to 0 \to X[1]$ est isomorphe à $X \xrightarrow{\mathrm{id}} X \to 0 \to X[1]$, donc distingué, et donne $\mathrm{cl}(Y) = \mathrm{cl}(X) + \mathrm{cl}(0)$. La rotation de $X \to X \to 0 \to X[1]$ est le triangle $X \to 0 \to X[1] \to X[1]$, qui donne $\mathrm{cl}(0) = \mathrm{cl}(X) + \mathrm{cl}(X[1])$, soit $\mathrm{cl}(X[1]) = -\mathrm{cl}(X)$. Comme $X[n+1] \simeq X[n][1]$, une récurrence sur $n$, vers le haut et vers le bas, donne $\mathrm{cl}(X[n]) = (-1)^n\,\mathrm{cl}(X)$. Le triangle scindé $X \to X \oplus Y \to Y \xrightarrow{0} X[1]$ est distingué, et donne la somme directe.

Pour la surjectivité, un élément de $K(\mathcal C)$ est une combinaison $\sum_i \mathrm{cl}(X_i) - \sum_j \mathrm{cl}(Y_j)$. Puisque $-\mathrm{cl}(Y) = \mathrm{cl}(Y[1])$, c'est une somme de classes, donc la classe d'une somme directe :
\[
  \sum_i \mathrm{cl}(X_i) - \sum_j \mathrm{cl}(Y_j) = \mathrm{cl}\Bigl(\bigoplus_i X_i \oplus \bigoplus_j Y_j[1]\Bigr).
\]
En particulier $\mathrm{cl}(X) - \mathrm{cl}(Y) = \mathrm{cl}(X \oplus Y[1])$. Enfin, un foncteur exact envoie triangles distingués sur triangles distingués, donc $X \mapsto \mathrm{cl}\,\varphi(X)$ est additive et passe au quotient ; si $\varphi \simeq \varphi'$, les objets $\varphi(X)$ et $\varphi'(X)$ sont isomorphes et ont la même classe.
\end{proof}

\begin{remarque}
La translation fait la différence avec les catégories abéliennes. À la vue~4, les notes doutent que tout élément du $K$ d'une catégorie abélienne soit une classe $\mathrm{cl}(X)$, et n'affirment que la forme $\mathrm{cl}(X) - \mathrm{cl}(Y)$. Dans une catégorie triangulée, l'objet $Y[1]$ joue le rôle de $-Y$. Pour les espaces vectoriels gradués de dimension finie, où $X[1]$ décale les degrés, la caractéristique d'Euler $\sum_i (-1)^i \dim X^i$ change de signe par translation, ce qui est l'égalité $\chi(X[1]) = -\chi(X)$.
\end{remarque}

\emph{Le critère des deux triangles.} Un corollaire de la vue~2 dit que $\mathrm{cl}(X) = \mathrm{cl}(X')$ si et seulement s'il existe deux triangles distingués $A \to B \to C \to A[1]$ et $A' \to B' \to C' \to A'[1]$ tels que
\[
  X \oplus B \oplus A[1] \oplus C[1] \;\simeq\; X' \oplus B' \oplus A'[1] \oplus C'[1].
\]
Le sens \q{si} est un calcul : la classe de $B \oplus A[1] \oplus C[1]$ est $\mathrm{cl}(B) - \mathrm{cl}(A) - \mathrm{cl}(C) = 0$. Il est démontré. Le sens \q{seulement si} est le lemme~2.4 de Thomason \cite{thomason1997}. Les notes le déduisent d'une description de $K(\mathcal C)$ comme quotient du monoïde des classes d'isomorphie d'objets par le sous-monoïde des $B \oplus A[1] \oplus C[1]$ ; ce sens n'est pas formalisé.

\emph{La formule d'Euler.} À la vue~3, pour une fonction additive $\chi$ sur une catégorie abélienne, la cinquième propriété d'une liste est
\[
  \sum_i (-1)^i \chi(X^i) = \sum_i (-1)^i \chi\bigl(H^i(X^\bullet)\bigr)
\]
pour un complexe $X^\bullet$ fini. La même égalité est en marge de la vue~2 de la pièce voisine \texttt{FG\_IL\_5\_SGA6\_2\_1}, pour la somme alternée des classes. Elle dit que la caractéristique d'Euler d'un complexe ne dépend que de sa cohomologie. En particulier, un complexe exact a une somme alternée nulle : pour $0 \to K \to K^2 \to K \to 0$ exacte, $1 - 2 + 1 = 0$. On la démontre ici pour la dimension.

\begin{encadre}
\begin{enonce}[Notes, vue~3, propriété~5, pour $\chi = \dim$]
Soit $V^0 \xrightarrow{d^0} V^1 \xrightarrow{d^1} \cdots \xrightarrow{d^{n-1}} V^n \to 0$ un complexe d'espaces vectoriels de dimension finie sur un corps, éventuellement gauche ($d^{i+1} \circ d^i = 0$). Avec $H^i = \ker d^i / \operatorname{im} d^{i-1}$,
\[
  \sum_{i=0}^{n} (-1)^i \dim V^i = \sum_{i=0}^{n} (-1)^i \dim H^i .
\]
\end{enonce}
\end{encadre}

\begin{proof}
Notons $z_i = \dim \ker d^i$ et $b_i = \dim \operatorname{im} d^{i-1}$, avec $b_0 = 0$, et $b_{n+1} = 0$ puisque $d^n = 0$. Le théorème du rang donne $\dim V^i = z_i + b_{i+1}$, et $\operatorname{im} d^{i-1} \subset \ker d^i$ donne $\dim H^i = z_i - b_i$. La différence des deux membres est donc $\sum_{i=0}^n (-1)^i (b_{i+1} + b_i)$, une somme télescopique : les termes $b_1, \dots, b_n$ s'y annulent deux à deux, et il reste $b_0 + (-1)^n b_{n+1} = 0$.
\end{proof}

\noindent\emph{Vérification en Lean.} La catégorie est prétriangulée au sens de mathlib (\texttt{Pretriangulated C}), qui n'a pas de groupe $K_0$ de catégorie triangulée ; l'axiome de l'octaèdre n'est pas supposé. Le groupe est \texttt{K₀ C}, quotient de \texttt{FreeAbelianGroup C} par le sous-groupe \texttt{relations C} qu'engendrent les relations des triangles distingués : c'est la forme que l'édition donne au $\mathbf Z^{(\mathrm{Ob}\,\mathcal C)}$ des notes. La relation d'un triangle est \texttt{cl\_obj₂}, la propriété universelle \texttt{lift}, \texttt{lift\_cl} et \texttt{hom\_ext}. Les énoncés encadrés sont \texttt{cl\_zero}, \texttt{cl\_eq\_of\_iso}, \texttt{cl\_shift\_one}, \texttt{cl\_shift}, \texttt{cl\_biprod}, \texttt{cl\_sub}, \texttt{cl\_surjective}, et, pour la fonctorialité, \texttt{map}, \texttt{map\_cl} et \texttt{map\_eq\_of\_iso}. Le sens \q{si} du critère des deux triangles est \texttt{cl\_eq\_of\_iso\_biprod}. La formule d'Euler est \texttt{sum\_finrank\_eq\_sum\_finrank\_cohomology} : le complexe est une famille $(V^i)_{i \in \mathbf N}$ d'espaces de dimension finie sur un anneau à division, avec $d^n = 0$, et la cohomologie \texttt{cohomology d i} est le quotient de $\ker d^i$ par l'image de $d^{i-1}$, vue dans $\ker d^i$. La somme télescopique est \texttt{sum\_alternating\_telescope}. Les noms sont ceux de \href{\leanblobmain/IhesSGA6_2_3.lean}{\texttt{IhesSGA6\_2\_3.\allowbreak{}lean}}.

Ne sont pas démontrés ici : le sens \q{seulement si} du critère des deux triangles, et la description de $K(\mathcal C)$ par le monoïde des classes d'isomorphie ; le fait qu'une équivalence induise un isomorphisme ; la suite exacte $K(\mathcal D) \to K(\mathcal C) \to K(\mathcal C/\mathcal D) \to 0$ pour une sous-catégorie épaisse, que la vue~3 marque \q{à vérifier} ; la comparaison $K(\mathcal C) \simeq K(D^b(\mathcal C))$ pour une catégorie abélienne, au n\textsuperscript{o}\,2 ; la formule d'Euler pour une fonction additive quelconque, ou pour les longueurs de modules.
\section[Cote 153 : polynômes à valeurs entières, co-opérations, analyseurs]{Cote 153 : polynômes à valeurs entières, co-opérations, analyseurs\protect\verifie{Folder153}}\label{sec:153}

La cote 153, \emph{Analyseurs : notes manuscrites (s.d.)}, dix pages que l'inventaire date \q{[à partir de 1982]}, cherche la structure abstraite d'un anneau d'opérations muni d'une composition, aujourd'hui appelée pléthorie, notion étudiée par Tall et Wraith en 1970 \cite{tallwraith1970} et nommée ainsi par Borger et Wieland en 2005 \cite{borgerwieland2005}. Elle y arrive par les polynômes à valeurs entières. La page~3 fixe une inclusion d'anneaux commutatifs $k_0 \subset K_0$ et l'anneau $\Omega = \{F \in K_0[T] \mid F(\lambda) \in k_0 \ \forall \lambda \in k_0\}$. Les co-opérations $F(x + y) = \sum_i G_i(x) H_i(y)$ et $F(xy) = \sum_\alpha J_\alpha(x) K_\alpha(y)$ doivent être des éléments \q{bien déterminés} de $\Omega \otimes_{k_0} \Omega$. Pour cela, la page énonce un lemme, le mot \q{Lemme} étant lu sans certitude : le sous-ensemble des $F \in K_0[T] \otimes_{k_0} M$ tels que $F(x) \in M$ pour tout $x \in k_0$ \q{s'identifie à $\Omega \otimes_{k_0} M$} (\lot{153}{1}{3}). La lecture précise : coordonnée par coordonnée dans une base de $M$.

La page~2 écrit les polynômes binomiaux $F_n = \binom{T}{n} \in \mathbf Q[T]$, affirme que $\bigoplus_n \mathbf Z F_n$ est une $\mathbf Z$-algèbre, et écrit la co-addition sous la forme générale $F_m(P + Q) = \sum \gamma^m_{ij} F_i(P) F_j(Q)$ ; la co-multiplication reste inachevée (\lot{153}{1}{2}). La page~5 définit l'analyseur, puis les constantes, et écrit sans justification $\Omega = \Omega_0 \oplus \Omega^0$ (\lot{153}{1}{5}). Les exemples $\mathrm{Appl}(A, A)$, $k[T]$ et $k[[T]]^+$ sont à la page~7, avec l'application $\Omega \to \mathrm{Appl}(\Omega_0, \Omega_0) = \Omega_{\Omega_0}$, avec le souhait \q{que $\Omega \to \Omega_{\Omega_0}$ soit injectif !} (\lot{153}{1}{7}). La page~9 donne l'exemple relatif et l'analyseur binomial de $\mathbf Z \subset \mathbf Q$ (\lot{153}{1}{9}).

\begin{definition}
Soit $K_0$ une $k_0$-algèbre commutative ; on note $\iota : k_0 \to K_0$ le morphisme structural. On pose $\Omega = \{F \in K_0[T] \mid F(\iota(\lambda)) \in \iota(k_0) \ \forall \lambda \in k_0\}$ ; c'est une sous-$k_0$-algèbre de $K_0[T]$, les valeurs d'une somme et d'un produit étant la somme et le produit des valeurs, et un polynôme constant $\iota(c)$ y appartenant. Pour un $k_0$-module $M$, $x \in k_0$ et $F \in K_0[T] \otimes_{k_0} M$, on note $F(x) \in K_0 \otimes_{k_0} M$ l'image de $F$ par $\mathrm{ev}_x \otimes \mathrm{id}_M$, où $\mathrm{ev}_x : K_0[T] \to K_0$ est l'évaluation en $\iota(x)$, et l'on dit que $F(x) \in M$ lorsque $F(x)$ est dans l'image de $M \to K_0 \otimes_{k_0} M$, $m \mapsto 1 \otimes m$. On note $\Omega_M$ l'ensemble des $F$ tels que $F(x) \in M$ pour tout $x \in k_0$. Enfin \q{$\Omega_M$ s'identifie à $\Omega \otimes_{k_0} M$} est lu : l'application canonique $\Omega \otimes_{k_0} M \to K_0[T] \otimes_{k_0} M$ est injective, et son image est $\Omega_M$.
\end{definition}

\begin{enonce}[Lemme, page 3]
Soit $M$ un $k_0$-module libre, de base $(e_i)_{i \in I}$, et écrivons tout $F \in K_0[T] \otimes_{k_0} M$ sous la forme $\sum_i F_i \otimes e_i$, les $F_i \in K_0[T]$ étant presque tous nuls.
\begin{enumerate}
\item $F \in \Omega_M$ si et seulement si $F_i \in \Omega$ pour tout $i$.
\item L'application canonique $\Omega \otimes_{k_0} M \to K_0[T] \otimes_{k_0} M$ est injective.
\item Son image est exactement $\Omega_M$.
\end{enumerate}
\end{enonce}

Dans la suite, $N$ et $P$ désignent des $k_0$-modules et $f : N \to P$ une application $k_0$-linéaire. La base $(e_i)$ donne, pour tout $N$, un isomorphisme $c_N : N \otimes_{k_0} M \to N^{(I)}$ sur les familles presque nulles d'éléments de $N$, qui envoie $n \otimes m$ sur $(m_i\, n)_i$, où les $m_i$ sont les coordonnées de $m$ ; c'est l'isomorphisme $N \otimes_{k_0} k_0^{(I)} \simeq N^{(I)}$. On appelle $c_N(t)_i$ la $i$-ième coordonnée de $t$.

\begin{lemme}\label{lem:153-nat}
Les coordonnées sont naturelles : pour $t \in N \otimes_{k_0} M$, la $i$-ième coordonnée de $(f \otimes \mathrm{id}_M)(t)$ est $f(c_N(t)_i)$.
\end{lemme}

\begin{proof}
Les deux membres sont additifs en $t$, et il suffit de le vérifier sur un tenseur pur $n \otimes m$ : la $i$-ième coordonnée de $f(n) \otimes m$ est $m_i f(n) = f(m_i n)$.
\end{proof}

\begin{lemme}\label{lem:153-image}
Un élément $t$ de $P \otimes_{k_0} M$ est dans l'image de $f \otimes \mathrm{id}_M$ si et seulement si chacune de ses coordonnées est dans l'image de $f$.
\end{lemme}

\general{TensorProductMemRangeRTensorBasis}

\begin{lemme}\label{lem:153-un}
L'image de $M \to K_0 \otimes_{k_0} M$, $m \mapsto 1 \otimes m$, est l'image de $\iota \otimes \mathrm{id}_M : k_0 \otimes_{k_0} M \to K_0 \otimes_{k_0} M$.
\end{lemme}

\begin{proof}
La première application est la composée de l'isomorphisme $M \simeq k_0 \otimes_{k_0} M$, $m \mapsto 1 \otimes m$, et de $\iota \otimes \mathrm{id}_M$.
\end{proof}

\begin{proof}[Démonstration du lemme de la page 3]
(1) Soit $x \in k_0$. Par le lemme~\ref{lem:153-un}, $F(x) \in M$ signifie que $(\mathrm{ev}_x \otimes \mathrm{id})(F)$ est dans l'image de $\iota \otimes \mathrm{id}$, c'est-à-dire, par le lemme~\ref{lem:153-image}, que chacune de ses coordonnées est dans $\iota(k_0)$. Par le lemme~\ref{lem:153-nat}, sa $i$-ième coordonnée est $\mathrm{ev}_x(F_i) = F_i(\iota(x))$. Ainsi $F \in \Omega_M$ si et seulement si $F_i(\iota(x)) \in \iota(k_0)$ pour tout $x$ et tout $i$, c'est-à-dire si et seulement si $F_i \in \Omega$ pour tout $i$.

(2) Un module libre est plat, fait classique ; le produit tensoriel par $M$ conserve donc l'injectivité de l'inclusion $\Omega \hookrightarrow K_0[T]$.

(3) Par le lemme~\ref{lem:153-image} appliqué à l'inclusion $\Omega \hookrightarrow K_0[T]$, $F$ est dans l'image de $\Omega \otimes_{k_0} M$ si et seulement si chaque $F_i$ est dans $\Omega$, c'est-à-dire, par~(1), si et seulement si $F \in \Omega_M$.
\end{proof}

\begin{remarque}
L'hypothèse de la page que $k_0 \to K_0$ soit une inclusion ne sert pas. Le lemme vaut pour toute $k_0$-algèbre commutative $K_0$, $\Omega$ étant l'ensemble des polynômes qui envoient $k_0$ dans l'image de $k_0$.
\end{remarque}

\medskip
\noindent\textit{Stabilité par composition et co-opérations (page~3).} On garde les notations de la définition ; on écrit $K_0[X, Y]$ pour l'anneau des polynômes en deux variables sur $K_0$, et, pour $F \in K_0[T]$, $\Delta_a F = F(X + Y)$ et $\Delta_m F = F(XY)$. On note $\Phi : \Omega \otimes_{k_0} \Omega \to K_0[X, Y]$ l'application $k_0$-linéaire qui envoie $G \otimes H$ sur $G(X) H(Y)$.

\begin{enonce}[Page 3, stabilité]
Si $F, G \in \Omega$, alors $F \circ G \in \Omega$.
\end{enonce}

\begin{proof}
Pour $x \in k_0$, $G(\iota(x)) = \iota(y)$ pour un $y \in k_0$, et $(F \circ G)(\iota(x)) = F(\iota(y)) \in \iota(k_0)$.
\end{proof}

\begin{enonce}[Page 3, les co-opérations]
Supposons que $K_0$ soit un localisé $S^{-1} k_0$ de $k_0$, et que $\Omega$ soit un $k_0$-module libre.
\begin{enumerate}
\item L'application $\Phi$ est injective.
\item Son image est l'ensemble des $P \in K_0[X, Y]$ tels que $P(\iota(x), \iota(y)) \in \iota(k_0)$ pour tous $x, y \in k_0$.
\item Pour $F \in \Omega$, il existe un unique $t \in \Omega \otimes_{k_0} \Omega$ tel que $\Phi(t) = F(X + Y)$, et un unique $t'$ tel que $\Phi(t') = F(XY)$.
\item Si $\Phi\bigl(\sum_i G_i \otimes H_i\bigr) = F(X + Y)$, alors $F \circ (P + Q) = \sum_i (G_i \circ P)(H_i \circ Q)$ pour tous $P, Q \in K_0[T]$ ; si $\Phi\bigl(\sum_\alpha J_\alpha \otimes K_\alpha\bigr) = F(XY)$, alors $F \circ (PQ) = \sum_\alpha (J_\alpha \circ P)(K_\alpha \circ Q)$.
\end{enumerate}
\end{enonce}

Soit $(e_j)_{j \in I}$ une base du $k_0$-module $\Omega$. Deux lemmes traduisent l'hypothèse sur $K_0$ : toute famille finie d'éléments de $K_0$ admet un dénominateur commun $s \in S$, c'est-à-dire que les $\iota(s) a$ sont dans $\iota(k_0)$, et $\iota(s)$ est inversible dans $K_0$.

\begin{lemme}\label{lem:153-indep}
Les $e_j$, vus dans $K_0[T]$, sont linéairement indépendants sur $K_0$.
\end{lemme}

\begin{proof}
Soit $\sum_j a_j e_j = 0$, les $a_j \in K_0$ presque tous nuls, et $s \in S$ un dénominateur commun : $\iota(s) a_j = \iota(d_j)$, $d_j \in k_0$. Alors $\sum_j d_j e_j = \iota(s) \sum_j a_j e_j = 0$ dans $\Omega$, donc les $d_j$ sont nuls, puis $\iota(s) a_j = 0$ et $a_j = 0$, $\iota(s)$ étant inversible.
\end{proof}

\begin{lemme}\label{lem:153-engendre}
Les $e_j$ engendrent $K_0[T]$ comme $K_0$-module.
\end{lemme}

\begin{proof}
Soit $p \in K_0[T]$. On chasse les dénominateurs des coefficients : il existe $s \in S$ et $q \in k_0[T]$ tels que $\iota(s) p$ soit l'image de $q$. Cette image envoie $\iota(x)$ sur $\iota(q(x))$, elle est donc dans $\Omega$, combinaison $k_0$-linéaire des $e_j$, et $p = \iota(s)^{-1} \cdot \iota(s) p$ est combinaison $K_0$-linéaire des $e_j$.
\end{proof}

\begin{proof}[Démonstration des co-opérations]
(1) Tout $t \in \Omega \otimes_{k_0} \Omega$ s'écrit $\sum_j G_j \otimes e_j$, les $G_j \in \Omega$ étant les coordonnées de $t$ dans la base $(e_j)$ du second facteur, et $\Phi(t) = \sum_j G_j(X) e_j(Y)$. Le coefficient de $X^m$ dans $\Phi(t)$ est $\sum_j c_m(G_j)\, e_j(Y)$, où $c_m(G_j) \in K_0$ est le coefficient de $T^m$ dans $G_j$. Si $\Phi(t) = \Phi(t')$, le lemme~\ref{lem:153-indep} donne $c_m(G_j) = c_m(G'_j)$ pour tous $j$ et $m$, donc $G_j = G'_j$ et $t = t'$.

(2) Les valeurs de $G(X) H(Y)$ en $(\iota(x), \iota(y))$ sont les produits $G(\iota(x)) H(\iota(y)) \in \iota(k_0)$, et la condition passe aux sommes. Réciproquement, soit $P$ à valeurs dans $\iota(k_0)$. Le lemme~\ref{lem:153-engendre}, appliqué aux coefficients de chaque monôme $X^n$, écrit $P = \sum_j G_j(X)\, e_j(Y)$ avec des $G_j \in K_0[T]$. Pour $x \in k_0$, le polynôme $P(\iota(x), T) = \sum_j G_j(\iota(x))\, e_j$ est dans $\Omega$, donc égal à $\sum_j \iota(\beta_j) e_j$ pour des $\beta_j \in k_0$ ; le lemme~\ref{lem:153-indep} donne $G_j(\iota(x)) = \iota(\beta_j)$. Ainsi chaque $G_j$ est dans $\Omega$, et $P = \Phi\bigl(\sum_j G_j \otimes e_j\bigr)$.

(3) Pour $F \in \Omega$, $(\Delta_a F)(\iota(x), \iota(y)) = F(\iota(x + y))$ et $(\Delta_m F)(\iota(x), \iota(y)) = F(\iota(xy))$ sont dans $\iota(k_0)$ : l'existence vient de~(2), l'unicité de~(1).

(4) Soit $\mathrm{ev}_{P,Q} : K_0[X, Y] \to K_0[T]$ le morphisme d'anneaux qui fixe $K_0$ et envoie $X$ sur $P$, $Y$ sur $Q$. Il envoie $G(X) H(Y)$ sur $(G \circ P)(H \circ Q)$, $F(X + Y)$ sur $F \circ (P + Q)$ et $F(XY)$ sur $F \circ (PQ)$ ; on l'applique à l'égalité supposée.
\end{proof}

\begin{remarque}
L'hypothèse employée est que $K_0$ soit un localisé de $k_0$ ; la lecture le donne comme exemple de son hypothèse $K_0 \otimes_{k_0} K_0 = K_0$. La démonstration ne passe pas par l'identification $K_0[X] \otimes_{k_0} K_0[Y] = K_0[X, Y]$, l'application $\Phi$ arrivant directement dans $K_0[X, Y]$. La liberté de $\Omega$, que demande la marge de la page, sert aux deux lemmes et à l'écriture $t = \sum_j G_j \otimes e_j$. L'inclusion $k_0 \subset K_0$ n'est pas supposée. Elle découle de la liberté de $\Omega$ dès que $K_0 \neq 0$, un $c \in k_0$ tel que $\iota(c) = 0$ annulant tous les $e_j$. Les règles de~(4) valent pour n'importe quel représentant et ne demandent pas l'unicité ; l'unicité fait des co-opérations des éléments \q{bien déterminés} de $\Omega \otimes_{k_0} \Omega$. La formule $F \circ \lambda T = \sum_\alpha J_\alpha(\lambda) K_\alpha$ de la page en est le cas $P = \lambda$, $Q = T$.
\end{remarque}

L'hypothèse de localisation ne sert qu'aux deux lemmes, et le second n'en a pas besoin. On le voit sur l'application $K_0$-linéaire $\beta : K_0 \otimes_{k_0} \Omega \to K_0[T]$, $a \otimes F \mapsto aF$.

\begin{enonce}[Page 3, les co-opérations sans localisation\piste{153-relative-int-coproducts}]
Soit $K_0$ une $k_0$-algèbre commutative quelconque.
\begin{enumerate}
\item L'application $\beta$ est surjective.
\item Si $\beta$ est injective et que $\Omega$ est un $k_0$-module libre, les conclusions (1) à (3) de l'énoncé précédent valent : $\Phi$ est injective, son image est l'ensemble des $P$ à valeurs dans $\iota(k_0)$ sur $k_0 \times k_0$, et $F(X + Y)$, $F(XY)$ sont, pour $F \in \Omega$, les images d'éléments uniques de $\Omega \otimes_{k_0} \Omega$.
\item L'application $\beta$ est injective lorsque $K_0$ est un localisé de $k_0$ et que $\Omega$ est libre, et lorsque $K_0$ est plat sur $k_0$ et que la multiplication $K_0 \otimes_{k_0} K_0 \to K_0$ est injective, c'est-à-dire $K_0 \otimes_{k_0} K_0 = K_0$.
\end{enumerate}
\end{enonce}

\begin{proof}
(1) Les monômes $T^n$ sont dans $\Omega$, puisqu'ils envoient $\iota(x)$ sur $\iota(x^n)$, et $\beta(a \otimes T^n) = a T^n$ ; ces polynômes engendrent $K_0[T]$.

(2) Soit $(e_j)$ une base de $\Omega$. Les $1 \otimes e_j$ forment une base du $K_0$-module $K_0 \otimes_{k_0} \Omega$, et $\beta\bigl(\sum_j a_j \otimes e_j\bigr) = \sum_j a_j e_j$. La surjectivité de $\beta$ donne donc la conclusion du lemme~\ref{lem:153-engendre}, son injectivité celle du lemme~\ref{lem:153-indep}, et la démonstration des co-opérations n'utilise rien d'autre de l'hypothèse sur $K_0$.

(3) Pour un localisé, l'injectivité est le lemme~\ref{lem:153-indep}, lu dans la base $(1 \otimes e_j)$. Dans le cas plat, $\beta$ est la composée de $\mathrm{id}_{K_0} \otimes (\Omega \hookrightarrow K_0[T])$, injective par platitude, et de $\mu : K_0 \otimes_{k_0} K_0[T] \to K_0[T]$, $a \otimes p \mapsto ap$. Comme $k_0$-module, $K_0[T]$ est isomorphe à $K_0^{(\mathbf N)}$ par les coefficients, donc $K_0 \otimes_{k_0} K_0[T]$ à $(K_0 \otimes_{k_0} K_0)^{(\mathbf N)}$, et $\mu$ devient la multiplication $K_0 \otimes_{k_0} K_0 \to K_0$ coefficient par coefficient, injective par hypothèse.
\end{proof}

\begin{remarque}
L'hypothèse de la lecture, $K_0[X] \otimes_{k_0} K_0[Y] = K_0[X, Y]$, revient à $K_0 \otimes_{k_0} K_0 = K_0$, le premier membre étant $(K_0 \otimes_{k_0} K_0)[X, Y]$. Elle suffit ici avec la platitude de $K_0$, qui couvre les localisés. Sans platitude, la démonstration demande l'injectivité de $\beta$, et l'on ne sait pas ici si $K_0 \otimes_{k_0} K_0 = K_0$ et la liberté de $\Omega$ la donnent. Ni l'inclusion $k_0 \subset K_0$ ni le passage par $K_0[X] \otimes_{k_0} K_0[Y]$ ne servent.
\end{remarque}

\medskip
\noindent\textit{Pólya et Vandermonde (page~2).} Pour $k_0 = \mathbf Z \subset K_0 = \mathbf Q$, $\Omega = \mathrm{Int}(\mathbf Z)$ ; on pose $F_n = \binom{T}{n} = T(T-1)\cdots(T-n+1)/n!$, et l'on note $\Delta f(x) = f(x+1) - f(x)$ la différence finie.

\begin{enonce}[Page 2, théorème de Pólya]
Les $F_n$ sont dans $\mathrm{Int}(\mathbf Z)$ et linéairement indépendants sur $\mathbf Z$. Tout $P \in \mathrm{Int}(\mathbf Z)$ de degré $d$ s'écrit $P = \sum_{k \le d} c_k F_k$ avec $c_k = (\Delta^k P)(0) \in \mathbf Z$. Ainsi $(F_n)_{n \in \mathbf N}$ est une base du $\mathbf Z$-module $\mathrm{Int}(\mathbf Z)$.
\end{enonce}

\general{PolynomialIntegerValued}

\begin{enonce}[Page 2, Vandermonde, et les co-opérations de $\mathrm{Int}(\mathbf Z)$]
Dans $\mathbf Q[X, Y]$, $F_m(X + Y) = \sum_{i + j = m} F_i(X) F_j(Y)$. Par suite l'unique élément de $\mathrm{Int}(\mathbf Z) \otimes_{\mathbf Z} \mathrm{Int}(\mathbf Z)$ qui représente $F_m(X + Y)$ est $\sum_{i+j=m} F_i \otimes F_j$ : les $\gamma^m_{ij}$ de la page valent $1$ si $i + j = m$ et $0$ sinon. De même $F_m(XY) = \sum_{i,j} \delta^m_{ij} F_i(X) F_j(Y)$ pour des entiers $\delta^m_{ij}$ uniquement déterminés.
\end{enonce}

\begin{proof}
L'identité est la formule de Chu--Vandermonde (Zhu Shijie, 1303 ; Vandermonde, 1772) dans un anneau binomial, $\binom{r+s}{m} = \sum_{i+j=m} \binom{r}{i}\binom{s}{j}$, que mathlib démontre (\texttt{Ring.\allowbreak{}add\_choose\_eq}) et qu'on applique dans $\mathbf Q[X, Y]$ à $r = X$, $s = Y$ ; les morphismes d'anneaux commutent aux coefficients binomiaux généralisés, d'où l'identification de $\binom{X}{i}$ à $F_i(X)$. Par le théorème de Pólya, $\mathrm{Int}(\mathbf Z)$ est libre, $\mathbf Q$ est le localisé de $\mathbf Z$ en les entiers non nuls, et l'énoncé des co-opérations s'applique : il donne l'unicité, et, pour $F_m(XY)$, l'existence ; les coefficients dans la base $(F_i \otimes F_j)$ sont les $\delta^m_{ij}$.
\end{proof}

\begin{remarque}
Les entiers $c^p_{m,n}$ et $d^p_{m,n}$ de la page s'en déduisent : $F_m F_n$ et $F_m \circ F_n$ sont dans $\mathrm{Int}(\mathbf Z)$, sous-anneau stable par composition, donc sont des combinaisons entières des $F_p$, de degré au plus $m + n$ et $mn$ ; cette conséquence n'a pas d'énoncé Lean séparé. La lecture attribue le théorème à G.~Pólya, dont l'article de 1919 étudie les bases de ce type pour les polynômes à valeurs entières sur l'anneau des entiers d'un corps de nombres \cite{polya1919} (voir aussi \cite{cahen1997}) ; la démonstration suivie ici est celle des différences finies. La structure de biring de $\mathrm{Int}(\mathbf Z)$ que définissent ces co-opérations, et sa structure de pléthorie, sont étudiées par Elliott \cite{elliott2010}.
\end{remarque}

\medskip
\noindent\textit{Constantes et décomposition (page~5).} Soit $\Omega$ un pseudo-anneau commutatif muni d'une loi $\circ$ associative, d'unité $T$, telle que $F \mapsto F \circ G$ soit un morphisme de pseudo-anneaux pour tout $G$ : ce sont les conditions~1) et~2). On note $\Omega_0 = \{\lambda \mid \lambda \circ F = \lambda \ \forall F\}$ et $\Omega^0 = \{F \mid F \circ 0 = 0\}$.

\begin{enonce}[Page 5, $\Omega = \Omega_0 \oplus \Omega^0$]
$\Omega_0$ est un sous-pseudo-anneau de $\Omega$ ; pour $F \in \Omega$ et $\lambda \in \Omega_0$, $F \circ \lambda \in \Omega_0$, et en particulier $F \circ 0 \in \Omega_0$ ; $\Omega^0$ est un sous-groupe et un idéal ; et $\Omega$ est somme directe des sous-groupes $\Omega_0$ et $\Omega^0$, par $F = F \circ 0 + (F - F \circ 0)$. L'application $F \mapsto (\lambda \mapsto F \circ \lambda)$ de $\Omega$ dans $\mathrm{Appl}(\Omega_0, \Omega_0)$ respecte la somme, le produit et la composition, envoie $T$ sur l'identité, et envoie une constante $\lambda$ sur l'application constante de valeur $\lambda$.
\end{enonce}

\begin{proof}
Comme $F \mapsto F \circ G$ est additif, $0 \circ G = 0$ et $(-F) \circ G = -(F \circ G)$ ; additivité et multiplicativité montrent que $\Omega_0$ est stable par somme, opposé et produit. Si $\lambda \in \Omega_0$, $(F \circ \lambda) \circ G = F \circ (\lambda \circ G) = F \circ \lambda$, et $0 \in \Omega_0$. Si $F \in \Omega^0$, $(GF) \circ 0 = (G \circ 0)(F \circ 0) = 0$. Une constante $\lambda$ de $\Omega^0$ vérifie $\lambda = \lambda \circ 0 = 0$ : l'intersection est nulle. Enfin $(F - F \circ 0) \circ 0 = F \circ 0 - (F \circ 0) \circ 0 = 0$, $F \circ 0$ étant une constante, ce qui donne la somme. Les propriétés de $F \mapsto (\lambda \mapsto F \circ \lambda)$ sont les conditions~2), l'associativité, $T \circ \lambda = \lambda$ et la définition des constantes.
\end{proof}

\begin{remarque}
Les conditions~3) n'interviennent pas, ni l'unité $T$ sauf pour l'image de $T$. La décomposition n'utilise que l'associativité et l'additivité de $F \mapsto F \circ G$. La multiplicativité sert seulement à faire de $\Omega_0$ un sous-pseudo-anneau et de $\Omega^0$ un idéal. La somme directe est une somme de groupes abéliens, $\Omega_0$ n'étant pas un idéal en général.
\end{remarque}

\medskip
\noindent\textit{Exemples et contre-exemples (page~7).}

\begin{enonce}[Page 7, l'exemple $\mathrm{Appl}(A, A)$]
Soit $A$ un pseudo-anneau commutatif et $\Omega_A = \mathrm{Appl}(A, A)$, avec les lois ponctuelles et la composition des applications. Il vérifie~1) et~2) ; ses constantes sont les applications constantes, et $(\Omega_A)_0 \simeq A$ comme pseudo-anneaux. Si $A$ est un anneau commutatif unitaire non nul et infini, $\Omega_A$ ne vérifie pas~3a) : l'indicatrice $\delta$ de $0$ n'admet aucune famille finie $(F'_i, F''_i)_{i < n}$ telle que $\delta \circ (G' + G'') = \sum_i (F'_i \circ G')(F''_i \circ G'')$ pour tous $G'$, $G''$.
\end{enonce}

\begin{proof}
Une constante $\lambda$ vérifie $\lambda = \lambda \circ c_0$, où $c_0$ est l'application constante de valeur $0$, donc $\lambda(x) = \lambda(0)$ pour tout $x$ ; l'isomorphisme est $\lambda \mapsto \lambda(0)$. Pour~3a), prenons $G'$ et $G''$ constantes de valeurs $x$ et $y$ : on obtiendrait $\delta(x + y) = \sum_{i < n} F'_i(x) F''_i(y)$ pour tous $x, y \in A$. Choisissons $n + 1$ éléments distincts $a_0, \dots, a_n$ de $A$ et posons $U_{ji} = F'_i(a_j)$, $V_{ik} = F''_i(-a_k)$. Alors $(UV)_{jk} = \delta(a_j - a_k)$ est la matrice identité d'ordre $n + 1$, de rang $n + 1$ sur l'anneau commutatif non nul $A$, alors que le rang de $UV$ est au plus celui de $U$, qui a $n$ colonnes.
\end{proof}

\begin{enonce}[Page 7, l'analyseur des polynômes et l'application $\Omega \to \Omega_{\Omega_0}$]
Soit $k$ un anneau commutatif et $\Omega = k[T]$ avec la composition des polynômes. Il vérifie~1) et~2), et ses constantes sont les polynômes constants. Si $k$ est un corps fini à $q$ éléments, $T^q - T$ est non nul et $(T^q - T) \circ \lambda = 0$ pour toute constante $\lambda$ : l'application $\Omega \to \mathrm{Appl}(\Omega_0, \Omega_0)$ n'est pas injective. Si $k$ est un anneau intègre infini, elle l'est. Pour $\mathrm{Int}(\mathbf Z)$, deux polynômes $F, G \in \mathbf Q[T]$ tels que $F \circ n = G \circ n$ pour tout $n \in \mathbf Z$ sont égaux.
\end{enonce}

\begin{proof}
Pour une constante $\lambda$, $\lambda = \lambda \circ 0$ est le polynôme constant $\lambda(0)$ ; réciproquement un polynôme constant est une constante. Sur un corps fini, $a^q = a$ pour tout $a$, d'où $(T^q - T) \circ a = a^q - a = 0$, et $T^q - T$ est de degré $q \geq 2$. Sur un anneau intègre infini, comme sur $\mathbf Q$ avec la partie infinie $\mathbf Z$, un polynôme est déterminé par ses valeurs, et $F \circ a$ est le polynôme constant $F(a)$.
\end{proof}

\begin{enonce}[{Page 7, $k[[T]]^+$ ne vérifie pas 3a)}]
Soit $k$ un anneau commutatif non nul et $F = \sum_{m \ge 1} T^m$. Les coefficients de $X^p Y^q$ dans $F(X + Y) = \sum_{m \ge 1} (X + Y)^m$, qui valent $\binom{p+q}{p}$ hors de $(p, q) = (0, 0)$ et $0$ en $(0, 0)$, ne sont ceux d'aucune somme finie $\sum_{i < n} a_i(X) b_i(Y)$ de séries formelles : il n'existe pas de suites $(a_{i,p})$, $(b_{i,q})$ telles que ce coefficient soit $\sum_{i < n} a_{i,p} b_{i,q}$ pour tous $p, q$.
\end{enonce}

\begin{proof}
La matrice de Pascal $P_N = \bigl(\binom{p+q}{p}\bigr)_{p, q < N}$ est de déterminant $1$, énoncé général rappelé à la suite de la démonstration. Si les coefficients étaient $\sum_{i < n} a_{i,p} b_{i,q}$, ceux de $P_{n+2}$ seraient $\sum_{i < n} a_{i,p} b_{i,q} + [p = 0][q = 0]$, et $P_{n+2}$ serait le produit d'une matrice à $n + 1$ colonnes par une matrice à $n + 1$ lignes, de rang au plus $n + 1$, alors qu'elle est inversible, de rang $n + 2$.
\end{proof}
\general{DetPascalMatrix}

\begin{remarque}
Le contre-exemple de~3a) pour $\mathrm{Appl}(A, A)$ est établi pour $A$ unitaire, commutatif, non nul et infini. La page ne parle pas de~3), et la lecture dit \q{pour $A$ infini}. Pour $k[[T]]^+$, la matrice des coefficients de $F(X + Y)$ diffère de la matrice de Pascal, que nomme la note de la lecture, par le coefficient $(0,0)$, nul puisque $F$ n'a pas de terme constant ; l'argument coûte donc un rang de plus. Le déterminant de la matrice de Pascal valant $1$ sur $\mathbf Z$, le contre-exemple vaut en toute caractéristique. L'énoncé Lean porte sur les coefficients. Le passage aux séries, où le coefficient de $X^p Y^q$ d'un produit $a(X) b(Y)$ est $a_p b_q$, est celui de la note.
\end{remarque}

Ne sont pas démontrés ici : l'isomorphisme $(\Omega_A)_0 \simeq \Gamma A$ pour un anneau d'un topos et l'exemple $\mathrm{End}(W_k(A))$ ; les constantes de $k[[T]]^+$ et les séries à terme constant nilpotent ; les co-opérations sous la seule hypothèse $K_0 \otimes_{k_0} K_0 = K_0$, sans platitude ; le contre-exemple de 3a) pour $\mathrm{Appl}(A,A)$, $A$ pseudo-anneau infini quelconque ; les analyseurs des puissances divisées et des $\lambda$-anneaux.

\begin{encadre}
\begin{theoreme}[Pages 3 et 9, co-opérations de $\mathrm{Int}$ relatif, forme corrigée par l'édition\piste{153-relative-int-coproducts}]\nonverifie
Soit $K_0$ une $k_0$-algèbre commutative telle que $K_0 \otimes_{k_0} K_0 = K_0$, et soit $\Omega = \{F \in K_0[T] \mid F(k_0) \subset k_0\}$, supposé libre comme $k_0$-module. Alors $F(X + Y)$ et $F(XY)$ sont, pour tout $F \in \Omega$, les images d'éléments uniques de $\Omega \otimes_{k_0} \Omega$, et $\Omega$ porte ainsi une co-addition et une co-multiplication, lois de composition d'un analyseur.
\end{theoreme}
\end{encadre}