\section[Cote 39 : le théorème de préparation « formel » ; fonctions implicites dans une classe de séries]{Cote 39 : le théorème de préparation « formel » ; fonctions implicites dans une classe de séries\protect\verifie{Folder39}}\label{sec:39}

La cote 39, \emph{Fonctions et structures \q{élémentaires} [Schémas formels, théorème de préparation] : notes manuscrites (s.d.)}, datée par l'inventaire \q{[vers 1960-1970]}, compte dix-neuf pages en trois ensembles séparés par des intercalaires vierges. Les deux premiers sont deux rédactions successives d'une axiomatique des classes de séries formelles (pages~2 à~7, puis~9 à~16). Le troisième, pages~18 et~19, énonce et démontre un théorème sous un titre souligné de sa main, \q{Th.\ de préparation “formel”} (\lot{39}{1}{18}). La démonstration commence par une réduction, \q{Comme $A$ est séparé et complet pour sa top.\ linéaire, on est ramené au cas où $A$ est discret}, puis précise que (i) \q{\textbf{signifie} que les $a_i$ ($0 \leq i \leq N-1$) sont nilpotents}. Un premier argument, par Nakayama et le gradué associé, est encadré et barré. Le second considère l'application $\varphi : ((b_i), Q) \mapsto \sum b_i Z^i + QF$ et conclut, par le gradué de la filtration $\mathfrak m$-adique, \q{finie}, que $\varphi$ est bijective (\lot{39}{1}{19}).

\begin{enonce}[Théorème de préparation « formel »]
Soient $A$ un anneau linéairement topologisé, séparé et complet, $Z$ une indéterminée, $F = \sum_{i \geqslant 0} a_i Z^i \in A[[Z]]$, et $N \in \mathbb N$ tel que
\begin{enumerate}
\item[(i)] $a_i$ est topologiquement nilpotent pour $0 \leqslant i \leqslant N - 1$ ;
\item[(ii)] $a_N$ est inversible.
\end{enumerate}
Alors $F$ est un élément régulier de $A[[Z]]$, et $A[[Z]]/F A[[Z]]$ est un $A$-module libre de base les images des $Z^i$, $0 \leqslant i \leqslant N-1$ : tout $G \in A[[Z]]$ s'écrit de façon unique $G = QF + \sum_{0 \leqslant i \leqslant N-1} b_i Z^i$, avec $Q \in A[[Z]]$ et $b_i \in A$.
\end{enonce}

\noindent On ne démontre ici que deux cas particuliers de cet énoncé : le cas d'un anneau complet pour une topologie $I$-adique, avec $a_i \in I$ pour $i < N$ ; et le cas discret auquel la démonstration du feuillet se ramène, avec $a_0, \dots, a_{N-1}$ nilpotents. Dans les deux cas, on écrit le reste $\sum_{i<N} b_i Z^i$ comme un polynôme $r \in A[Z]$ de degré $< N$.

On s'appuie sur le théorème classique de division de Weierstrass, sous la forme suivante : \emph{soient $A$ un anneau séparé et complet pour la topologie $I$-adique et $F \in A[[Z]]$ ; si l'image $\bar F$ de $F$ dans $(A/I)[[Z]]$ est d'ordre $N$ et si le coefficient $a_N$ de $F$ est inversible dans $A$, alors pour tout $G \in A[[Z]]$ il existe un unique couple $(Q, r)$, $Q \in A[[Z]]$, $r \in A[Z]$ de degré $< N$, tel que $G = QF + r$ ; et si $QF = r$ avec $\deg r < N$, alors $Q = 0$ et $r = 0$.}

\begin{lemme}\label{lem:39-adique}
Soient $I$ un idéal de $A$, $A$ séparé et complet pour la topologie $I$-adique, et $F = \sum a_i Z^i$ avec $a_i \in I$ pour $i < N$ et $a_N$ inversible. Alors $F$ est régulier dans $A[[Z]]$, et tout $G \in A[[Z]]$ s'écrit de façon unique $G = QF + r$ avec $Q \in A[[Z]]$ et $r \in A[Z]$ de degré $< N$.
\end{lemme}

\begin{proof}
Si $I = A$, l'anneau $A$, séparé pour la topologie $A$-adique, est nul, et tout est trivial. Supposons $I \neq A$, de sorte que $A/I$ n'est pas nul. Les coefficients de $\bar F$ d'indice $< N$ sont nuls, puisque $a_i \in I$ ; celui d'indice $N$ est l'image de l'inversible $a_N$, donc est inversible dans l'anneau non nul $A/I$, et en particulier non nul. Ainsi $\bar F$ est d'ordre exactement $N$, et, $a_N$ étant inversible, le théorème de division s'applique. Il donne l'existence et l'unicité de l'écriture $G = QF + r$. Si $FH = 0$, on a $HF = 0$ avec le reste $r = 0$ de degré $< N$, donc $H = 0$ : $F$ est régulier.
\end{proof}

\begin{lemme}\label{lem:39-nilp}
Soit $\mathfrak m$ un idéal nilpotent de $A$. Alors $A$ est séparé et complet pour la topologie $\mathfrak m$-adique. Si $a_0, \dots, a_{N-1}$ sont nilpotents, l'idéal qu'ils engendrent est nilpotent.
\end{lemme}

\begin{proof}
La première assertion est l'énoncé général rappelé à la suite de la démonstration, pour le module $A$ : la suite des $\mathfrak m^n$ est nulle à partir d'un rang $k$, et une suite de Cauchy pour la topologie $\mathfrak m$-adique est stationnaire à partir de ce rang. Pour la seconde assertion : l'idéal $\mathfrak m = (a_0, \dots, a_{N-1})$ est contenu dans le nilradical et engendré par un nombre fini d'éléments ; c'est un fait classique qu'un tel idéal est nilpotent (si $a_i^{e} = 0$ pour tout $i$, un produit de $N(e-1)+1$ éléments de $\mathfrak m$ est combinaison de monômes en les $a_i$ dont l'un au moins des exposants atteint $e$). C'est la phrase de la lecture : \q{il est de type fini et engendré par des nilpotents, donc nilpotent}.
\end{proof}
\general{IsAdicCompleteOfIsNilpotent}

\begin{proof}[Démonstration du cas discret]
Soit $A$ un anneau commutatif quelconque. Supposons que les coefficients $a_i$ d'indice $i < N$ soient nilpotents et que $a_N$ soit inversible. Soit $\mathfrak m$ l'idéal engendré par $a_0, \dots, a_{N-1}$. Par le lemme~\ref{lem:39-nilp}, $\mathfrak m$ est nilpotent et $A$ est séparé et complet pour la topologie $\mathfrak m$-adique. Comme $a_i \in \mathfrak m$ pour $i < N$, le lemme~\ref{lem:39-adique}, appliqué à $I = \mathfrak m$, donne la régularité de $F$ et l'écriture unique.
\end{proof}

\begin{remarque}
Dans le cas adique, l'idéal n'a pas à être de type fini. La lecture n'emploie cette hypothèse que pour obtenir $\mathfrak m^j A[[Z]] = \mathfrak m^j[[Z]]$ dans sa démonstration par le gradué associé.
\end{remarque}

\begin{remarque}
La démonstration ci-dessus admet la division de Weierstrass comme théorème classique, là où la page passe par le gradué associé ; le nom renvoie au théorème de préparation de Weierstrass pour les fonctions analytiques, dont l'énoncé est l'analogue formel.
\end{remarque}

\begin{remarque}
Pour la topologie $I$-adique, \q{topologiquement nilpotent} signifie $a_i \in \sqrt I$, condition plus faible que l'hypothèse $a_i \in I$ du lemme~\ref{lem:39-adique}.
\end{remarque}

Ne sont pas démontrés ici : la préparation (unité $\times$ polynôme distingué) ; les séries algébriques ; le cas d'une topologie linéaire quelconque ; le cas $I$-adique sous l'hypothèse $a_i \in \sqrt I$.

\paragraph{L'axiomatique des pages 9 à 14.} Sur un anneau commutatif $k$ quelconque, pour une famille $A_n \subset S_n = k[[t_1, \ldots, t_n]]$, la seconde rédaction pose (I) $t_i \in A_n$ ; (S) si $\varphi \in A_n$ et si $f_1, \ldots, f_n \in A_m$ ont des termes constants nilpotents, $\varphi(f_1, \ldots, f_n) \in A_m$ ; (R) les $A_n$ sont des sous-anneaux unitaires ; (H) l'inverse d'un $A$-morphisme $X_n \to X_n$ qui est un isomorphisme formel est un $A$-morphisme ; (D) les coefficients de $f \in A_{n+m}$ en ses $m$ dernières variables sont dans $A_n$. La page tire de (H) le corollaire~1 (si $f \in A_n$ et si $f(0)$ est inversible dans $k$, $f^{-1} \in A_n$), le corollaire~2 (le couple $(A_n, A_n \cap \mathfrak m_n)$ est zariskien et hensélien) et le corollaire~3 (les fonctions implicites), puis de (D) l'inclusion $A_n \subset k_0[[t]]$, $k_0 = A_0$ (\lot{39}{1}{11}, \lot{39}{1}{12}, \lot{39}{1}{14}). La démonstration du corollaire~1 substitue $t_{n+1} = 1$, substitution que (S) interdit ; la lecture le démontre avec (D) et ne tient le couple pour hensélien que sous (D). On lit ici \q{isomorphisme formel} comme \q{admet un inverse pour la substitution}, et $\mathfrak m_n$ comme l'idéal des séries sans terme constant.

\begin{theoreme}[Grothendieck, page 12, corollaires 2 et 3\piste{39-inverse-function-axioms-henselian}]\label{thm:39-hensel}
Supposons (I), (S), (R), (H). Si $P \in A_{n+1}$, vu comme série en $(Z, t_1, \ldots, t_n)$, vérifie $P(0) = 0$ et si $\partial P/\partial Z\,(0)$ est inversible dans $k$, l'unique $F \in S_n$ tel que $F(0) = 0$ et $P(F(t), t) = 0$ est dans $A_n$. Le couple $(A_n, A_n \cap \mathfrak m_n)$ est hensélien, en particulier zariskien.
\end{theoreme}

\begin{proof}
\emph{Existence et unicité de $F$.} Vu dans $S_n[[Z]]$, $P$ a son terme constant $g_0$ dans l'idéal $I$ des variables, pour lequel $S_n$ est séparé et complet, et son coefficient $g_1$ de $Z$ inversible. La division de Weierstrass de $Z$ par $P$ donne $Z = qP + r$, $r \in S_n$. Le coefficient de $Z$ donne $1 = g_0 q_1 + g_1 q_0$, et $g_0 \in I$ est dans le radical, donc $q_0$ et $q$ sont inversibles ; ainsi $P = q^{-1}(Z - r)$ avec $r = -g_0 q_0 \in I$. La substitution $Z \mapsto G$, $G(0) = 0$, est un morphisme d'anneaux $S_{n+1} \to S_n$ qui envoie $q^{-1}$ sur un inversible : $P(G, t) = 0$ si et seulement si $G = r$.

\emph{Appartenance.} Appliquée à $P(W, t) - Z$, l'existence donne $\varphi(Z, t)$ avec $P(\varphi(Z, t), t) = Z$ ; appliquée à $P(W, t) - P(Z, t)$, dont $W = Z$ et $W = \varphi(P(Z, t), t)$ sont deux solutions, l'unicité donne $\varphi(P(Z, t), t) = Z$. Ainsi $(Z, t) \mapsto (\varphi, t)$ est l'inverse de l'$A$-morphisme $(Z, t) \mapsto (P, t)$ ; par (H), $\varphi \in A_{n+1}$, et par (S), $\varphi(0, t) \in A_n$. Comme $P(\varphi(0, t), t) = 0$, c'est $F$. C'est l'argument de la page.

\emph{Le couple.} Soient $f$ unitaire à coefficients dans $A_n$ et $a_0 \in A_n$ tels que $f(a_0)(0) = 0$ et que $f'(a_0)$ soit inversible modulo $A_n \cap \mathfrak m_n$, donc $f'(a_0)(0)$ inversible dans $k$. La série $P(Z, t) = f(a_0 + Z)$ est dans $A_{n+1}$ par (S), avec $P(0) = 0$ et $\partial P/\partial Z\,(0) = f'(a_0)(0)$ ; la racine $a_0 + F$ est dans $A_n$ et congrue à $a_0$ modulo $\mathfrak m_n$. Si $g \in A_n \cap \mathfrak m_n$ et $y \in A_n$, le polynôme $(1 + gy)Z - 1$ et $a_0 = 1$ donnent un inverse de $1 + gy$ dans $A_n$.
\end{proof}

\noindent Le couple est donc hensélien sous (H) seul, sans la condition (D) que la lecture ajoute : le corollaire~3 ne passe pas par le corollaire~1, et seule la forme forte du corollaire~1 demande davantage. Voir \texttt{implicit\_function}, \texttt{implicit\_mem}, \texttt{hensel\_mem} et \texttt{henselianRing} dans \href{\leanblob/Folder39.lean}{\texttt{Folder39.\allowbreak{}lean}}.

\begin{contrexemple}[énoncé de l'édition]\label{cex:39}
Sur $k = \mathbb Q$, les séries à terme constant entier, $A_n = \{ f \in S_n : f(0) \in \mathbb Z \}$, vérifient (I), (S), (R), (H), et $2 \in A_0$, inversible dans $\mathbb Q$, n'a pas d'inverse dans $A_0$. Le corollaire~1 de la page~11 ne découle pas de (I), (S), (R), (H).
\end{contrexemple}

\begin{proof}
Un nilpotent de $\mathbb Q$ est nul ; une substitution par des séries sans terme constant conserve le terme constant, et un inverse pour la substitution est sans terme constant.
\end{proof}

\begin{theoreme}[D'après les pages 11 et 14, avec (D)]
Supposons (I), (S), (R), (H), (D). Si $f \in A_n$ et si $f(0)$ est inversible dans $k$, alors $f^{-1} \in A_n$. Sous (D) seule, $A_n \subset k_0[[t_1, \ldots, t_n]]$.
\end{theoreme}

\noindent L'énoncé tient, et (D) ne sert au corollaire~1 que pour $n = 0$ : l'inverse de $s \mapsto f(0)s$ est dans $A_1$ par (H), son coefficient $f(0)^{-1}$ dans $A_0$ par (D), et le théorème~\ref{thm:39-hensel} appliqué à $fZ - 1$ en $a_0 = f(0)^{-1}$ donne $f^{-1}$. Voir \texttt{inv\_mem}, \texttt{coeff\_mem}, \texttt{intConst\_isFormalClass} et \texttt{intConst\_not\_inv\_mem}. Ne sont pas démontrés : la forme jacobienne de (H) pour un morphisme quelconque, les produits fibrés transversaux, les sous-schémas formels, les parties principales, la question de fidèle platitude de la page~12, et la première rédaction (pages~2 à~7).
\section[Cote 41 : continuité de la section générique et ouverture (proposition 1)]{Cote 41 : continuité de la section générique et ouverture (proposition 1)\protect\verifie{Folder41}}\label{sec:41}

La cote 41, \emph{Construction de morphismes étales (Chap. V) : notes manuscrites (s.d.)}, datée par l'inventaire \q{[années 1960-1970]}, est une seule section de rédaction en treize pages. Page~3, elle pose la notion de section \emph{monogène}, qui choisit continûment le point générique d'une composante géométriquement irréductible de chaque fibre, et la question de la représentabilité du foncteur qu'elles forment. Elle construit ensuite, sous des conditions de spécialisation, un revêtement étale séparé qui la représente (pages~4 à~10). Page~11, elle revient au cas où les fibres elles-mêmes sont irréductibles, et écrit une \q{Prop.~1°} en trois conditions, à laquelle s'ajoute, encadrée, une condition \q{(iii bis)}. L'hypothèse de finitude porte sur la condition~(ii), \q{$f$ soit ouvert [\dots] si $Y$ est loc.\ noeth., $f$ de type fini}, et la seule formule lisible de la démonstration est $\varphi^{-1}(U) = f(U)$ (\lot{41}{1}{11}).

\begin{enonce}[Proposition 1]
Soit $f : X \to Y$ un morphisme de type fini dont les fibres sont irréductibles et non vides, et soit $\varphi(y)$ le point générique de $X_y$. On considère les conditions :
\begin{enumerate}
\item[(i)] $\varphi : Y \to X$ est continue ;
\item[(ii)] $f$ est ouvert ;
\item[(iii)] $y \in \overline{\{y'\}} \Rightarrow \varphi(y) \in \overline{\{\varphi(y')\}}$ ;
\item[(iii bis)] pour tous $y \in \overline{\{y'\}}$ et $x$ au-dessus de $y$, il existe $x'$ au-dessus de $y'$ tel que $x \in \overline{\{x'\}}$.
\end{enumerate}
Alors (i)~$\Leftrightarrow$~(ii) sans autre hypothèse, et (ii)~$\Rightarrow$~(iii)~$\Leftrightarrow$~(iii bis) ; si $f$ est localement de présentation finie (par exemple $Y$ localement noethérien), les quatre conditions sont équivalentes.
\end{enonce}

Sur les espaces sous-jacents, dire que $\varphi(y)$ est le point générique de la fibre se formule ainsi.

\begin{definition}
Soient $X$, $Y$ des espaces topologiques et $f : X \to Y$ une application quelconque. On dit que $\varphi : Y \to X$ est une \emph{section générique} de $f$ si, pour tout $y \in Y$, on a $f(\varphi(y)) = y$ et $x \in \overline{\{\varphi(y)\}}$ pour tout $x \in f^{-1}(y)$.
\end{definition}

\noindent Cela revient à dire que $\varphi(y)$ est un point générique de la fibre $f^{-1}(y)$ munie de la topologie induite, puisque l'adhérence de $\{\varphi(y)\}$ dans $f^{-1}(y)$ est la trace sur $f^{-1}(y)$ de son adhérence dans $X$ ; une fibre qui a un point générique est irréductible et non vide. Pour un morphisme de schémas, la fibre schématique $X_y$ est homéomorphe au sous-espace $f^{-1}(y)$ ; ce fait classique n'est pas démontré ici. Dans les lemmes qui suivent, $f$ est une application quelconque entre espaces topologiques, qu'on ne suppose même pas continue, et $\varphi$ une section générique de $f$.

\begin{lemme}\label{lem:41-formule}
Pour tout ouvert $U$ de $X$, $\varphi^{-1}(U) = f(U)$.
\end{lemme}

\begin{proof}
Si $\varphi(y) \in U$, alors $y = f(\varphi(y)) \in f(U)$. Inversement, soient $x \in U$ et $y = f(x)$ ; alors $x \in \overline{\{\varphi(y)\}}$, et l'ouvert $U$, qui contient un point de l'adhérence de $\{\varphi(y)\}$, contient $\varphi(y)$ : $y \in \varphi^{-1}(U)$.
\end{proof}

\begin{lemme}\label{lem:41-top}
On a (i)~$\Leftrightarrow$~(ii), (i)~$\Rightarrow$~(iii), et (iii)~$\Leftrightarrow$~(iii bis).
\end{lemme}

\begin{proof}
(i)~$\Leftrightarrow$~(ii). Par le lemme~\ref{lem:41-formule}, pour tout ouvert $U$ de $X$, l'ensemble $\varphi^{-1}(U)$ est ouvert si et seulement si $f(U)$ l'est ; or $\varphi$ est continue si et seulement si le premier l'est pour tout $U$, et $f$ est ouverte si et seulement si le second l'est pour tout $U$.

(i)~$\Rightarrow$~(iii). Une application continue $\varphi$ envoie l'adhérence de $\{y'\}$ dans l'adhérence de $\{\varphi(y')\}$.

(iii)~$\Rightarrow$~(iii bis). Soient $y \in \overline{\{y'\}}$ et $x$ au-dessus de $y$. Alors $x \in \overline{\{\varphi(y)\}}$ par définition de $\varphi$, et $\varphi(y) \in \overline{\{\varphi(y')\}}$ par (iii), donc $x \in \overline{\{\varphi(y')\}}$ ; et $x' = \varphi(y')$ est au-dessus de $y'$.

(iii bis)~$\Rightarrow$~(iii). Soit $y \in \overline{\{y'\}}$. Appliquons (iii bis) à $x = \varphi(y)$, qui est au-dessus de $y$ : il existe $x'$ au-dessus de $y'$ avec $\varphi(y) \in \overline{\{x'\}}$. Comme $x'$ est dans la fibre de $y'$, $x' \in \overline{\{\varphi(y')\}}$, et donc $\varphi(y) \in \overline{\{\varphi(y')\}}$.
\end{proof}

\begin{proof}[Démonstration de la proposition 1]
Les implications (i)~$\Leftrightarrow$~(ii), (ii)~$\Rightarrow$~(iii)~$\Leftrightarrow$~(iii bis) sont celles du lemme~\ref{lem:41-top}, (ii)~$\Rightarrow$~(iii) passant par (i). Il reste, pour $f$ un morphisme de schémas localement de présentation finie, à déduire (ii) de (iii bis). Or (iii bis) dit exactement que les générisations se relèvent le long de $f$, et un morphisme localement de présentation finie qui relève les générisations est ouvert : c'est un théorème de Grothendieck et Dieudonné (EGA~IV, 1.10.4 \cite{ega4-1}), qui repose sur le théorème de Chevalley sur les parties constructibles. Les quatre conditions sont donc équivalentes.
\end{proof}

\begin{remarque}
L'implication (iii bis)~$\Rightarrow$~(ii) ne s'obtient pas par la seule topologie. Soient $X = \mathbb N$ muni de la topologie discrète, $Y = \mathbb N$ muni de la topologie cofinie, et $f : X \to Y$ l'identité, qui est continue. Les fibres sont des points, et $\varphi = f^{-1}$ est une section générique. Les deux espaces étant séparés au sens T$_1$, $y \in \overline{\{y'\}}$ entraîne $y = y'$, et (iii bis) est triviale. Mais $f$ n'est pas ouverte : $f(\{0\}) = \{0\}$ n'est pas ouvert dans $Y$, puisque son complémentaire est infini. L'application $f$ n'est pas un morphisme de schémas, et l'exemple montre seulement qu'une hypothèse, de finitude ou autre, est indispensable à cette implication, et à elle seule.
\end{remarque}

\begin{remarque}
Les implications (i)~$\Leftrightarrow$~(ii) et (i)~$\Rightarrow$~(iii)~$\Leftrightarrow$~(iii bis) valent pour toute application entre espaces topologiques munie d'une section générique, sans que $f$ soit de type fini, ni même continue.
\end{remarque}

\begin{remarque}
Seule l'implication (iii bis)~$\Rightarrow$~(ii) emploie l'hypothèse de finitude, sous la forme de la présentation finie locale, par le critère d'ouverture par relèvement des générisations (EGA~IV, 1.10.4), admis ici comme théorème classique.
\end{remarque}

Ne sont pas démontrés ici : la constructibilité ; l'ouverture universelle ; l'irréductibilité géométrique des fibres ; le cas \q{$Y$ localement noethérien} ; la fibre schématique comme $f^{-1}(y)$ ; les définitions~2 et~3 ; la représentabilité des sections monogènes ; le théorème des pages~8 et~9.

\begin{encadre}
\begin{theoreme*}[D'après les pages 3 et 8 à 10, composantes irréductibles des fibres, forme reconstituée par l'édition\piste{41-irreducible-components-etale-criterion}]\nonverifie
Soit $f : X \to Y$ de type fini qui, en chaque point générique d'une composante d'une fibre, est localement universellement ouvert et quasi-fini sur un espace affine $Y[t_1, \ldots, t_{n-1}]$, sans platitude ni réduction géométrique des fibres. Un $Y$-schéma étale séparé $M$ dont les points géométriques au-dessus de $y$ indexent les composantes géométriquement irréductibles de $X_{\bar y}$ existe si et seulement si, au-dessus de tout trait, aucune composante de la fibre générique ne se spécialise en deux composantes distinctes de la fibre spéciale et deux composantes distinctes ne se rencontrent pas dans une spécialisation ; $M$ est fini si et seulement si toute composante générique se spécialise en une composante spéciale.
\end{theoreme*}
\end{encadre}
{\small La page énonce le théorème sans démonstration ; le sens de la seconde condition et le complément de finitude sont de la lecture.\par}
\section[Cote 42 : familles cohérentes de germes, le lemme 1 et le lemme 2]{Cote 42 : familles cohérentes de germes, le lemme 1 et le lemme 2\protect\verifie{Folder42}}\label{sec:42}

La cote 42, \emph{Réseaux d'anneaux locaux : notes manuscrites (s.d.)}, six pages que l'inventaire date \q{[années 1960-1970]}, demande si une application entre préschémas localement noethériens est déterminée, et peut être construite, point par point, à partir des anneaux locaux reliés par les générisations. La page~3 ramène la question à une proposition sur les faisceaux : sous une condition~(H) d'injectivité des flèches de générisation entre fibres, les sections globales sont les familles cohérentes de germes. Le lemme~1 en porte le contenu, et la page le démontre en une ligne. Le lieu considéré est stable par générisation, et \q{il suffit de montrer qu'il est \emph{constructible}, donc que s'il contient $x$, il contient les pts d'un ouvert non vide de $\bar x$} (\lot{42}{1}{3}). Pour le faisceau structural, la page~4 enchaîne : \q{Il reste à vérifier que les conditions de la prop.\ sont vérifiées}. Elle isole un fait d'algèbre commutative, le lemme~2, dont la démonstration occupe le bas de la page~4 et le haut de la page~5 (\lot{42}{1}{4}). La page glose le noyau de $A \to A_{\mathfrak p}$ comme \q{l'annulateur de $A - p$}, le premier mot étant lu avec doute. Elle traite la seconde assertion en se ramenant au cas $f = 1$, \q{car $A_p = (A_f)_{p A_f}$} (\lot{42}{1}{5}).

\begin{enonce}[Proposition et lemme 1, page 3]
Soient $X$ un espace topologique noethérien et sobre, et $F$ un faisceau d'ensembles sur $X$ vérifiant
\begin{itemize}
\item[(H)] pour tout $x \in X$, il existe un ouvert $W \ni x$ tel que $\rho_{yx} : F_y \to F_x$ soit injective pour tout $y \in W \cap \overline{\{x\}}$.
\end{itemize}
\begin{enumerate}
\item (Lemme~1) Pour toute famille cohérente $(\xi_x)$ et toute section $s \in F(U)$ sur un ouvert $U$, l'ensemble $E = \{x \in U : s_x = \xi_x\}$ est ouvert.
\item (Proposition) L'application $\Gamma(X, F) \to \varprojlim_x F_x$, qui envoie une section sur la famille de ses germes, est bijective.
\end{enumerate}
\end{enonce}

\begin{enonce}[Lemme 2, pages 4 et 5]
Soient $A$ un anneau noethérien et $\mathfrak p$ un idéal premier de $A$.
\begin{enumerate}
\item Il existe $f \in A \setminus \mathfrak p$ tel que $A_f \to A_{\mathfrak p}$ soit injectif.
\item Si de plus $A \to A_{\mathfrak p}$ est injectif, alors $A_{\mathfrak q} \to A_{\mathfrak p}$ est injectif pour tout idéal premier $\mathfrak q \supseteq \mathfrak p$.
\item (Forme de la page) Il existe $f \in A \setminus \mathfrak p$ tel que, pour tout idéal premier $\mathfrak Q$ de $A_f$ dont la trace sur $A$ contient $\mathfrak p$, $(A_f)_{\mathfrak Q} \to A_{\mathfrak p}$ soit injectif.
\end{enumerate}
\end{enonce}

\begin{enonce}[Lemme 1 et corollaire 1, pages 3 et 4, cas affine]
Soit $A$ un anneau noethérien. Appelons famille cohérente une famille $(\xi_{\mathfrak p})$, $\xi_{\mathfrak p} \in A_{\mathfrak p}$, indexée par les idéaux premiers, telle que $\xi_{\mathfrak q} \mapsto \xi_{\mathfrak p}$ par $A_{\mathfrak q} \to A_{\mathfrak p}$ chaque fois que $\mathfrak p \subseteq \mathfrak q$.
\begin{enumerate}
\item (Lemme~1) Pour toute famille cohérente $(\xi_{\mathfrak p})$ et tous $a, s \in A$, l'ensemble des $\mathfrak p$ tels que $s \notin \mathfrak p$ et $\xi_{\mathfrak p} = a/s$ est ouvert dans $\operatorname{Spec} A$.
\item (Corollaire~1) L'application $a \mapsto (a/1)_{\mathfrak p}$ est une bijection de $A = \Gamma(\operatorname{Spec} A, \mathcal O)$ sur l'ensemble des familles cohérentes.
\end{enumerate}
\end{enonce}

\noindent\emph{Conventions.} Pour $x, y \in X$, on écrit $x \rightsquigarrow y$ lorsque $y \in \overline{\{x\}}$ : $y$ est une spécialisation de $x$, $x$ une générisation de $y$. Tout ouvert contenant $y$ contient alors $x$, d'où une application $\rho_{yx} : F_y \to F_x$, compatible aux germes : $\rho_{yx}(s_y) = s_x$ pour toute section $s$ définie au voisinage de $y$. Une famille $(\xi_x)$, $\xi_x \in F_x$, est cohérente si $\rho_{yx}(\xi_y) = \xi_x$ chaque fois que $x \rightsquigarrow y$. Dans $\operatorname{Spec} A$, $\mathfrak p \rightsquigarrow \mathfrak q$ équivaut à $\mathfrak p \subseteq \mathfrak q$. Un ouvert non vide de l'irréductible $\overline{\{x\}}$ contient son point générique $x$ ; la condition~(H) dit donc la même chose que la page, \q{un ouvert non vide} de $\overline{\{x\}}$ sur lequel les $F_y \to F_x$ sont injectives. Pour une partie multiplicative $S$ de $A$, on note $a \mapsto a/1$ le morphisme $A \to S^{-1}A$ ; on rappelle que $a/1 = 0$ si et seulement s'il existe $s \in S$ avec $sa = 0$, que tout $z \in S^{-1}A$ vérifie $z \cdot (s/1) = a/1$ pour un $a \in A$ et un $s \in S$, et que si $g : A \to B$ envoie $S$ dans les inversibles de $B$, il existe un unique $\bar g : S^{-1}A \to B$ avec $\bar g(a/1) = g(a)$. Les flèches $A_f \to A_{\mathfrak p}$ et $A_{\mathfrak q} \to A_{\mathfrak p}$ sont de cette forme, $g$ étant le morphisme canonique $A \to A_{\mathfrak p}$.

\begin{lemme}\label{lem:42-ouvert}
Soient $X$ un espace noethérien et sobre et $E \subseteq X$ une partie stable par générisation telle que, pour tout $x \in E$, il existe un ouvert $W \ni x$ avec $W \cap \overline{\{x\}} \subseteq E$. Alors $E$ est ouvert.
\end{lemme}

\general{NoetherianIsOpenOfStableUnderGeneralization}

\begin{proof}[Démonstration du lemme 1 de la page 3]
\emph{$E$ est stable par générisation.} Soient $x \in E$ et $y \rightsquigarrow x$. Comme $U$ est ouvert et contient $x$, il contient $y$, et $s_y = \rho_{xy}(s_x) = \rho_{xy}(\xi_x) = \xi_y$ par cohérence ; donc $y \in E$.

\emph{Condition locale.} Soit $x \in E$, et soit $W$ l'ouvert que fournit~(H) en $x$. L'ouvert $W \cap U$ contient $x$. Pour $y \in W \cap U \cap \overline{\{x\}}$, on a $x \rightsquigarrow y$, et $\rho_{yx}(s_y) = s_x = \xi_x = \rho_{yx}(\xi_y)$ ; l'injectivité de $\rho_{yx}$ donne $s_y = \xi_y$, donc $y \in E$. Le lemme~\ref{lem:42-ouvert} conclut.
\end{proof}

\begin{proof}[Démonstration de la proposition]
L'injectivité est l'axiome de séparation des faisceaux : deux sections globales qui ont les mêmes germes en tout point sont égales. Soit $(\xi_x)$ une famille cohérente. Pour chaque $x$, le germe $\xi_x$ provient d'une section $s^x$ sur un ouvert $U_x \ni x$ ; par le lemme~1, $V_x = \{y \in U_x : s^x_y = \xi_y\}$ est un ouvert, qui contient $x$. Les restrictions $s^x|_{V_x}$ ont, sur $V_x \cap V_{x'}$, les mêmes germes $\xi_y$ en tout point ; elles y coïncident donc, et se recollent, les $V_x$ recouvrant $X$, en une section globale $s$. Pour tout $x$, $s_x = (s^x|_{V_x})_x = \xi_x$.
\end{proof}

\begin{lemme}\label{lem:42-lift}
Soient $S \subseteq A$ une partie multiplicative et $g : A \to B$ un morphisme d'anneaux envoyant $S$ dans les inversibles de $B$. Si, pour tout $a \in A$, $g(a) = 0$ entraîne $a/1 = 0$ dans $S^{-1}A$, alors $\bar g : S^{-1}A \to B$ est injectif.
\end{lemme}

\begin{proof}
Comme $\bar g$ est additif, il suffit de montrer que son noyau est nul. Soit $z \in S^{-1}A$ avec $\bar g(z) = 0$, et écrivons $z \cdot (s/1) = a/1$ avec $a \in A$ et $s \in S$. En appliquant $\bar g$, on obtient $g(a) = \bar g(z)\, g(s) = 0$, donc $a/1 = 0$ par hypothèse, c'est-à-dire $z \cdot (s/1) = 0$. Comme $s/1$ est inversible dans $S^{-1}A$, $z = 0$.
\end{proof}

\begin{lemme}\label{lem:42-tue}
Soient $A$ un anneau noethérien et $\mathfrak p$ un idéal premier. Il existe $f \notin \mathfrak p$ tel que $fy = 0$ pour tout $y$ du noyau $J$ de $A \to A_{\mathfrak p}$.
\end{lemme}

\begin{proof}
Le noyau $J$ est l'ensemble des $a \in A$ tels que $sa = 0$ pour \emph{au moins un} $s \notin \mathfrak p$. L'anneau $A$ étant noethérien, l'idéal $J$ est engendré par un nombre fini d'éléments $x_1, \dots, x_n$. Pour chaque $i$, l'appartenance $x_i \in J$ donne un $s_i \notin \mathfrak p$ tel que $s_i x_i = 0$. Posons $f = s_1 \cdots s_n$ ; comme $\mathfrak p$ est premier, son complémentaire est stable par produit, et $f \notin \mathfrak p$. L'ensemble des $y \in A$ tels que $fy = 0$ est un idéal de $A$ ; il contient chaque $x_i$, car $f = s_i c_i$ avec $c_i = \prod_{j \neq i} s_j$, donc $f x_i = c_i (s_i x_i) = 0$ ; il contient donc l'idéal engendré par les $x_i$, qui est $J$.
\end{proof}

\begin{proof}[Démonstration du lemme 2]
(1) Soit $f$ donné par le lemme~\ref{lem:42-tue}. Appliquons le lemme~\ref{lem:42-lift} à $S = \{f^n\}$ et au morphisme canonique $g : A \to A_{\mathfrak p}$. Si $g(a) = 0$, alors $a \in J$, donc $fa = 0$ ; comme $f \in S$, cela signifie $a/1 = 0$ dans $A_f$. Le morphisme $A_f \to A_{\mathfrak p}$ est donc injectif.

(2) Appliquons le lemme~\ref{lem:42-lift} à $S = A \setminus \mathfrak q$ et au morphisme canonique $g : A \to A_{\mathfrak p}$, qui inverse $S$ puisque $\mathfrak p \subseteq \mathfrak q$. Si $g(a) = 0$, alors $a = 0$ par l'injectivité supposée de $g$, et a fortiori $a/1 = 0$ dans $A_{\mathfrak q}$.

(3) Prenons $f$ comme en~(1), et soit $\mathfrak Q$ un idéal premier de $A_f$ dont la trace $\mathfrak q$ sur $A$ contient $\mathfrak p$. Le morphisme $h : A_f \to A_{\mathfrak p}$ envoie $A_f \setminus \mathfrak Q$ dans les inversibles : écrivons $y \in A_f \setminus \mathfrak Q$ sous la forme $y \cdot (f^n/1) = a/1$ ; si $a$ était dans $\mathfrak p$, donc dans $\mathfrak q$, $a/1 = y \cdot (f^n/1)$ serait dans $\mathfrak Q$, ce qui est exclu puisque $y \notin \mathfrak Q$ et que $f^n/1$, inversible, n'est pas dans $\mathfrak Q$. Donc $a \notin \mathfrak p$, $h(y)\,h(f^n/1) = a/1$ est inversible dans $A_{\mathfrak p}$, et $h(y)$ l'est aussi. Le morphisme $(A_f)_{\mathfrak Q} \to A_{\mathfrak p}$ est donc défini, et il est injectif par le lemme~\ref{lem:42-lift} appliqué à $h$, qui est injectif par~(1) : c'est l'argument de~(2) pour l'anneau $A_f$.
\end{proof}

\begin{proof}[Démonstration du lemme 1 et du corollaire 1, cas affine]
Pour le lemme~1, soit $E$ l'ensemble des $\mathfrak p$ tels que $s \notin \mathfrak p$ et $\xi_{\mathfrak p} \cdot (s/1) = a/1$. Il est stable par générisation : si $\mathfrak q \in E$ et $\mathfrak p \subseteq \mathfrak q$, alors $s \notin \mathfrak p$, et l'image par $A_{\mathfrak q} \to A_{\mathfrak p}$ de l'égalité $\xi_{\mathfrak q} \cdot (s/1) = a/1$ est $\xi_{\mathfrak p} \cdot (s/1) = a/1$. Soit $\mathfrak p \in E$, et $f$ donné par le lemme~\ref{lem:42-tue}. L'ouvert $D(f) \cap D(s)$ contient $\mathfrak p$. Soit $\mathfrak q$ un premier de cet ouvert qui contient $\mathfrak p$ ; le lemme~\ref{lem:42-lift}, appliqué à $S = A \setminus \mathfrak q$, montre que $A_{\mathfrak q} \to A_{\mathfrak p}$ est injectif : si $a'/1 = 0$ dans $A_{\mathfrak p}$, alors $fa' = 0$ avec $f \notin \mathfrak q$, donc $a'/1 = 0$ dans $A_{\mathfrak q}$. Or $\xi_{\mathfrak q} \cdot (s/1) - a/1$ a pour image $\xi_{\mathfrak p} \cdot (s/1) - a/1 = 0$ ; il est donc nul, et $\mathfrak q \in E$. Le lemme~\ref{lem:42-ouvert} s'applique, $\operatorname{Spec} A$ étant noethérien et sobre.

Pour le corollaire~1, on utilise la description du faisceau structural comme faisceau des familles $(\sigma_{\mathfrak p}) \in \prod_{\mathfrak p \in U} A_{\mathfrak p}$ qui sont localement des fractions (pour tout $\mathfrak p \in U$, il existe un voisinage $V$ de $\mathfrak p$ et $a, s \in A$ avec $s \notin \mathfrak q$ et $\sigma_{\mathfrak q} = a/s$ pour tout $\mathfrak q \in V$), et le fait que $a \mapsto (a/1)_{\mathfrak p}$ est une bijection de $A$ sur les sections globales de ce faisceau. L'injectivité de l'application du corollaire en découle. Soit $(\xi_{\mathfrak p})$ une famille cohérente. Pour chaque $\mathfrak p$, écrivons $\xi_{\mathfrak p} \cdot (s/1) = a/1$ avec $s \notin \mathfrak p$ ; l'ensemble $E$ du lemme~1 pour ces $a$ et $s$ est un voisinage ouvert de $\mathfrak p$, sur lequel $\xi_{\mathfrak q} = a/s$. La famille $(\xi_{\mathfrak p})$ est donc localement une fraction, c'est une section globale du faisceau structural, et elle provient d'un $a \in A$.
\end{proof}

\begin{remarque}
Le corollaire~1, dans le cas affine, est un cas d'un énoncé de D.~Ferrand sur les modules qui sont limite projective de leurs localisés, annoncé sans démonstration en 1966 \cite{ferrand1966} et démontré dans une note de février 2004 (proposition~3).
\end{remarque}

\begin{remarque}
Le lemme~\ref{lem:42-ouvert} est le \q{donc} de la page~3. De la constructibilité, la page passe aussitôt à la propriété \q{s'il contient $x$, il contient les points d'un ouvert non vide de $\bar x$}. Le lemme prend pour hypothèse cette propriété, jointe à la stabilité par générisation, et la constructibilité n'intervient pas dans la démonstration.
\end{remarque}

\begin{remarque}
Les énoncés sont démontrés pour un espace noethérien, et le corollaire~1 pour $X = \operatorname{Spec} A$ affine. C'est le cas auquel la page se ramène (\q{La question est locale. On peut donc supposer $X$ noethérien}). La page~3 écrit \q{un voisinage $U$ de $\bar x$ tel que pour tt $y \in \bar x \cap U$}. Un ouvert contenant tout $\overline{\{x\}}$ donnerait une condition plus forte que~(H), qui l'entraîne. La démonstration de la page, comme celle-ci, n'emploie que la forme faible, \q{un ouvert non vide $U$ de $\bar x$}. L'injectivité de $\Gamma(X,F) \to \varprojlim F_x$ ne demande ni~(H) ni l'hypothèse noethérienne, et celle de $A \to \varprojlim A_{\mathfrak p}$ vaut pour tout anneau commutatif.
\end{remarque}

\begin{remarque}
L'hypothèse noethérienne n'intervient pas dans~(2) du lemme~2, qui vaut pour tout anneau commutatif. Dans~(1), elle sert seulement à rendre de type fini le noyau $J$ de $A \to A_{\mathfrak p}$. Ce noyau est formé des éléments annulés par \emph{un} élément de $A \setminus \mathfrak p$. L'annulateur de $A \setminus \mathfrak p$, que glose la page, est en général plus petit et ne convient pas. La démonstration de la page prend un annulateur par générateur, et suit donc la bonne description.
\end{remarque}

\begin{remarque}
Mathlib contient l'énoncé \q{constructible et stable par générisation, donc ouvert} pour les spectres d'anneaux, mais pas le critère de constructibilité des espaces noethériens par lequel la page y arrive ; le lemme~\ref{lem:42-ouvert} fait les deux pas à la fois.
\end{remarque}

\begin{remarque}
Dans la forme~(3) du lemme~2, l'hypothèse que la trace de $\mathfrak Q$ contienne $\mathfrak p$ est celle de la page, \q{provenant d'un idéal $q' \supset p$ ne rencontrant pas $f$} ; elle rend la flèche $(A_f)_{\mathfrak Q} \to A_{\mathfrak p}$ définie. La démonstration n'a pas besoin de l'identification $A_{\mathfrak p} = (A_f)_{\mathfrak p A_f}$ par laquelle la page se ramène au cas $f = 1$. Le corollaire~1 n'utilise du lemme~2 que le lemme~\ref{lem:42-tue}. Un même $f$ tue le noyau de $A \to A_{\mathfrak p}$ et rend injectives toutes les flèches $A_{\mathfrak q} \to A_{\mathfrak p}$ pour $\mathfrak q \in D(f) \cap V(\mathfrak p)$ : c'est~(H) pour le faisceau structural. Dans la démonstration du lemme~1, l'argument donne l'égalité $s_y = \xi_y$, là où la page écrit \q{d'où $s_x = \xi_y$}.
\end{remarque}

Ne sont pas démontrés ici : le corollaire~1 pour un préschéma localement noethérien non affine ; les deux contre-exemples. Les corollaires~2 et~3 (pleine fidélité) sont démontrés dans l'encadré suivant, et le lemme~3 sous la forme de la page, \q{$F$ vérifie~(H)}, dans le dernier encadré de la section.

\begin{encadre}
\begin{theoreme*}[D'après les pages 1 à 6, réseaux d'anneaux locaux, forme corrigée par l'édition\piste{42-reseau-functor-fully-faithful}]
Soient $S$ un préschéma localement noethérien, $X$ et $Y$ des $S$-préschémas localement de type fini, $Y$ séparé sur $S$. Les $S$-morphismes $X \to Y$ correspondent bijectivement aux homomorphismes de réseaux d'anneaux locaux $p(X) \to p(Y)$ au-dessus de $p(S)$ : applications croissantes des ensembles ordonnés de spécialisation, munies d'homomorphismes locaux compatibles $\mathcal O_{Y,\varphi(x)} \to \mathcal O_{X,x}$. L'hypothèse \q{$Y$ séparé} est celle de l'édition.
\end{theoreme*}
\end{encadre}

\noindent\emph{Conventions.} Un homomorphisme de réseaux $\Phi : p(X) \to p(Y)$ au-dessus de $p(S)$ est la donnée d'une application $\varphi : X \to Y$ telle que $x \rightsquigarrow x'$ entraîne $\varphi(x) \rightsquigarrow \varphi(x')$ et que $s_Y(\varphi(x)) = s_X(x)$, et, pour chaque $x$, d'un homomorphisme local $\alpha_x : \mathcal O_{Y,\varphi(x)} \to \mathcal O_{X,x}$. On demande deux compatibilités : pour $x \rightsquigarrow x'$, le carré formé de $\alpha_{x'}$, $\alpha_x$ et des flèches de générisation $\mathcal O_{Y,\varphi(x')} \to \mathcal O_{Y,\varphi(x)}$, $\mathcal O_{X,x'} \to \mathcal O_{X,x}$ commute ; et le composé $\mathcal O_{S,s_X(x)} \to \mathcal O_{Y,\varphi(x)} \to \mathcal O_{X,x}$ est la flèche de $s_X$. La condition de localisation de la page~1 porte sur $p(X)$ et $p(Y)$, qui viennent de préschémas ; elle n'a pas à figurer dans les homomorphismes. Un $S$-morphisme $f$ donne $p(f) = (f, (f^\sharp_x)_x)$. On appelle \emph{germe} de $\Phi$ en $x$ le morphisme $g_x = \operatorname{Spec}(\alpha_x)$ suivi de $\operatorname{Spec} \mathcal O_{Y,\varphi(x)} \to Y$ ; c'est un $S$-morphisme $\operatorname{Spec} \mathcal O_{X,x} \to Y$, et pour $x \rightsquigarrow x'$ le germe $g_x$ est $g_{x'}$ précédé de $\operatorname{Spec} \mathcal O_{X,x} \to \operatorname{Spec} \mathcal O_{X,x'}$. Le germe de $p(f)$ en $x$ est $\operatorname{Spec} \mathcal O_{X,x} \to X \xrightarrow{f} Y$.

\begin{proof}
\emph{$\Phi$ est déterminé par ses germes.} Le point fermé de $\operatorname{Spec} \mathcal O_{X,x}$ va sur $\varphi(x)$ ; et $\operatorname{Spec} \mathcal O_{Y,y} \to Y$ est un monomorphisme, de sorte que $g_x$ détermine $\operatorname{Spec}(\alpha_x)$, donc $\alpha_x$.

\emph{Injectivité (corollaire~2).} Si $p(f) = p(f')$, les composés de $f$ et $f'$ avec $\operatorname{Spec} \mathcal O_{X,x} \to X$ coïncident pour tout $x$. Comme $X$ est localement noethérien, il existe un ouvert affine $U \ni x$ tel que $\Gamma(U, \mathcal O_X) \to \mathcal O_{X,x}$ soit injectif (lemme~2, (1)) ; $f$ et $f'$ coïncident alors sur un voisinage de $x$, et, ces voisinages recouvrant $X$, $f = f'$. Ni la séparation ni la finitude de $Y$ ne servent ici.

\emph{Le pas local du lemme~3.} Soient $x \rightsquigarrow x''$ tels que $\mathcal O_{X,x''} \to \mathcal O_{X,x}$ soit injectif, et $a, b : \operatorname{Spec} \mathcal O_{X,x''} \to Y$ deux $S$-morphismes qui coïncident après $\operatorname{Spec} \mathcal O_{X,x} \to \operatorname{Spec} \mathcal O_{X,x''}$. L'égalisateur de $a$ et $b$ est un sous-schéma fermé parce que $Y$ est séparé sur $S$, et $\operatorname{Spec} \mathcal O_{X,x} \to \operatorname{Spec} \mathcal O_{X,x''}$ se factorise par lui. Le noyau de cette flèche est nul, l'anneau étant injecté ; celui de l'égalisateur, plus petit, l'est aussi, et une immersion fermée de noyau nul est un isomorphisme : $a = b$. L'injectivité demandée a lieu pour $x''$ dans un ouvert affine $U \ni x$ où $\Gamma(U, \mathcal O_X) \to \mathcal O_{X,x}$ est injectif, puisque $\mathcal O_{X,x''}$ est alors un localisé de $\Gamma(U, \mathcal O_X)$.

\emph{Le lieu d'accord est ouvert (lemme~1).} Soient $W$ un préschéma localement noethérien, $\iota : W \to X$ et $h : W \to Y$ avec $s_Y h = s_X \iota$. Disons que $h$ s'accorde à $\Phi$ en $w$ si le composé $\operatorname{Spec} \mathcal O_{W,w} \to W \xrightarrow{h} Y$ est le germe $g_{\iota(w)}$ précédé de $\operatorname{Spec}(\iota^\sharp_w)$. Ce lieu $E$ est stable par générisation, par la compatibilité des germes. Si $w \in E$, prenons l'ouvert affine $U \ni w$ du pas précédent : pour $w'' \in U \cap \overline{\{w\}}$, les deux morphismes $\operatorname{Spec} \mathcal O_{W,w''} \to Y$ à comparer coïncident après $\operatorname{Spec} \mathcal O_{W,w} \to \operatorname{Spec} \mathcal O_{W,w''}$, puisque $w \in E$, et le pas local donne $w'' \in E$. Le lemme~\ref{lem:42-ouvert}, appliqué dans chaque ouvert affine de $W$, qui est un espace noethérien, montre que $E$ est ouvert.

\emph{Surjectivité (corollaire~3).} Soit $\Phi$. Comme $Y$ est localement de type fini sur $S$ et que $\Gamma(U, \mathcal O_X) \to \mathcal O_{X,x}$ est injectif pour un ouvert affine $U \ni x$, le germe $g_x$ se prolonge en un $S$-morphisme $f_x : U_x \to Y$ sur un ouvert $U_x \ni x$ : c'est le théorème de passage à la limite d'EGA~IV qu'invoque la lecture. Par le pas précédent, le lieu $V_x \subseteq U_x$ où $f_x$ s'accorde à $\Phi$ est un ouvert, qui contient $x$. Sur $V_x \cap V_{x'}$, les restrictions de $f_x$ et $f_{x'}$ s'accordent toutes deux à $\Phi$ en tout point, donc ont les mêmes germes, et coïncident par l'argument de l'injectivité. Elles se recollent en un $S$-morphisme $f : X \to Y$ dont les germes sont ceux de $\Phi$, donc $p(f) = \Phi$.
\end{proof}

\begin{remarque}
Lean démontre l'énoncé dans \href{\leanblob/Folder42.lean}{\texttt{Folder42.\allowbreak{}lean}}, espace \texttt{Reseau}, sous des hypothèses un peu plus larges : $X$ localement noethérien, $Y$ localement de type fini et séparé sur un $S$ quelconque (\texttt{toReseau\_bijective}) ; la forme de la page, $S$ localement noethérien et $X$ localement de type fini, s'en déduit (\texttt{corollaire3}). Les homomorphismes de réseaux sont la structure \texttt{ReseauHom}, et $p(f)$ est \texttt{toReseau}. L'injectivité, \texttt{toReseau\_injective}, ne demande que $X$ localement noethérien. La séparation de $Y$ n'intervient qu'au pas local du lemme~3, \texttt{ext\_of\_injective\_of\_isSeparated} ; le lieu d'accord ouvert est \texttt{isOpen\_matches}, qui s'appuie sur \texttt{isOpen\_of\_stableUnderGeneralization\_of\_locally}, version localement noethérienne du lemme~\ref{lem:42-ouvert} ; la surjectivité est \texttt{toReseau\_surjective}. Le prolongement d'un germe en un morphisme sur un voisinage est pris dans mathlib (\texttt{spread\_out\_of\_isGermInjective'}), avec l'unicité correspondante (\texttt{spread\_out\_unique\_of\_isGermInjective'}). La démonstration ne passe pas par le faisceau $U \mapsto \mathrm{Hom}_S(U, Y)$ ni par la proposition de la page~3 ; elle en reprend les deux pas, le lemme~1 et le lemme~3, sur les germes eux-mêmes. Le lemme~3 sous la forme de la page fait l'objet de l'encadré suivant. La question marginale de la page~6 sur la nécessité de l'hypothèse noethérienne et le cas non séparé ne sont pas formalisés.
\end{remarque}

\begin{encadre}
\begin{theoreme*}[Lemme 3, page 5, forme de la page\piste{42-reseau-functor-fully-faithful}]
Soient $X$ un $S$-préschéma localement noethérien et $Y$ un $S$-préschéma séparé sur $S$. Le préfaisceau $F : U \mapsto \mathrm{Hom}_S(U, Y)$ est un faisceau sur $X$, et il vérifie~(H). Plus précisément, si $x \rightsquigarrow y$ et si $\mathcal O_{X,y} \to \mathcal O_{X,x}$ est injectif, alors $\rho_{yx} : F_y \to F_x$ est injective. Si de plus $X$ est noethérien, $\mathrm{Hom}_S(X, Y) \to \varprojlim_x F_x$ est bijective (corollaire~2, par la proposition de la page~3). L'hypothèse \q{$Y$ séparé} est celle de l'édition.
\end{theoreme*}
\end{encadre}

\begin{proof}
\emph{$F$ est un faisceau.} Si $V = \bigcup_i U_i$ et si des $S$-morphismes $f_i : U_i \to Y$ coïncident deux à deux sur $U_i \cap U_j$, qui est le produit fibré de $U_i \to V \leftarrow U_j$, ils se recollent en un unique $f : V \to Y$, qui est un $S$-morphisme parce qu'il l'est sur chaque $U_i$.

\emph{Les germes.} Pour $x \in U$, notons $\operatorname{Spec} \mathcal O_{X,x} \to U$ la flèche canonique. Deux sections $a \in F(U)$, $b \in F(V)$ ont le même germe en $x$ si et seulement si leurs composés avec $\operatorname{Spec} \mathcal O_{X,x} \to U$ et $\operatorname{Spec} \mathcal O_{X,x} \to V$ coïncident. Dans un sens, ces flèches se factorisent par un voisinage de $x$ où $a$ et $b$ coïncident. Dans l'autre, $U \cap V$ est localement noethérien, et deux morphismes qui coïncident sur $\operatorname{Spec} \mathcal O_{X,x}$ coïncident au voisinage de $x$ (le prolongement unique de mathlib, déjà employé pour l'injectivité du corollaire~2).

\emph{L'injectivité.} Soient $x \rightsquigarrow y$ avec $\mathcal O_{X,y} \to \mathcal O_{X,x}$ injectif, et $a, b$ deux sections au voisinage de $y$ dont les germes ont même image dans $F_x$, c'est-à-dire, l'ouvert contenant aussi $x$, mêmes germes en $x$. Leurs composés avec $\operatorname{Spec} \mathcal O_{X,y} \to Y$ sont deux $S$-morphismes qui coïncident après $\operatorname{Spec} \mathcal O_{X,x} \to \operatorname{Spec} \mathcal O_{X,y}$. Le pas local du lemme~3 de l'encadré précédent les rend égaux, et les germes en $y$ sont égaux.

\emph{La condition~(H).} Soit $W \ni x$ un ouvert affine où $\Gamma(W, \mathcal O_X) \to \mathcal O_{X,x}$ est injectif. Pour $y \in W \cap \overline{\{x\}}$, $\mathcal O_{X,y}$ est un localisé de $\Gamma(W, \mathcal O_X)$, donc $\mathcal O_{X,y} \to \mathcal O_{X,x}$ est injectif, et l'étape précédente s'applique. Pour $X = \operatorname{Spec} A$ avec $A \to A_{\mathfrak p}$ injectif, c'est le lemme~2,~(2), qui donne l'injectivité de $A_{\mathfrak q} \to A_{\mathfrak p}$ pour $\mathfrak q \supseteq \mathfrak p$, comme le veut la page. Le corollaire~2 est la proposition de la page~3 appliquée à $F$, l'espace sous-jacent d'un préschéma noethérien étant noethérien et sobre.
\end{proof}

\begin{remarque}
Lean démontre l'énoncé dans \href{\leanblob/Folder42.lean}{\texttt{Folder42.\allowbreak{}lean}}, espace \texttt{Reseau}, pour un $S$ quelconque : le faisceau est \texttt{homSheaf} (\texttt{isSheaf\_homPresheaf}), la description des germes \texttt{germ\_homSheaf\_eq\_iff}, l'injectivité \texttt{stalkSpecializes\_homSheaf\_injective}, la condition~(H) \texttt{lemme3}, et le corollaire~2 sous forme faisceautique \texttt{corollaire2}, qui applique \texttt{proposition} à \texttt{homSheaf}. La séparation ne sert, là encore, qu'à \texttt{ext\_of\_injective\_of\_isSeparated}. La forme affine de la page, avec $A_{\mathfrak q} \to A_{\mathfrak p}$, n'est pas énoncée en Lean : l'énoncé formalisé porte sur l'injectivité de $\mathcal O_{X,y} \to \mathcal O_{X,x}$, et l'identification de ces anneaux locaux aux localisés de $A$ n'y est pas écrite.
\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{theoreme*}[Grothendieck, page 12, critère d'immersion ouverte\piste{102-open-immersion-criterion}]\nonverifie
Sur une base localement noethérienne $S$, un monomorphisme formellement étale $u : G \to F$ de foncteurs sur les $S$-schémas est une immersion ouverte dès que $F$ et $G$ sont des faisceaux fpqc qui commutent aux limites inductives filtrantes d'anneaux et aux limites adiques d'anneaux artiniens.
\end{theoreme*}
\end{encadre}
{\small Démonstration donnée par l'édition, non vérifiée en Lean.\par}
{\small La page dit \q{infinitésimalement étale}, et le mot \q{adiques} y est incertain. Mathlib n'a pas la descente fpqc des foncteurs sur les schémas. On se reportera aux notes de Grothendieck (\lot{102}{1}{12}).\par}

\begin{encadre}
\begin{theoreme*}[Grothendieck, pages 2 à 4, 15 et 19, critère valuatif de platitude d'une adhérence\piste{127-closure-flatness-artinian-or-trait}]\nonverifie
Soient $X \to Y$ localement noethérien, $F$ cohérent sur $X$, $U$ un ouvert rétrocompact et $G_U$ un quotient cohérent de $F|_U$, plat sur $Y$. Si les anneaux locaux de $X$ aux points de $X - U$ ont des fibres formelles géométriquement normales, alors $G = \mathrm{Im}(F \to i_*G_U)$ est plat sur $Y$, avec $U$ universellement $G$-dense relativement à $Y$, si et seulement s'il en est ainsi après tout changement de base $Y' \to Y$ où $Y'$ est artinien ou un trait.
\end{theoreme*}
\end{encadre}
{\small Les feuillets en esquissent une démonstration incomplète (pages 3 et 4). La page~4 est en grande partie illisible, et le \q{vrai théorème} de la page~15, qui porte \q{artinien ou trait}, est sans démonstration ; le mot \q{artinien} n'est incertain que dans la remarque~1.4.2 qui le précède. Mathlib n'a pas la densité schématique universelle ni les fibres formelles. On se reportera aux notes de Grothendieck (\lot{127}{1}{2}).\par}

\begin{encadre}
\begin{theoreme*}[Grothendieck, pages 7, 9, 10 et 12, ouverture de Hironaka sur une base réduite ; voir aussi Kollár 2011\piste{127-hironaka-reduced-base-openness}]\nonverifie
Soient $f : X \to Y$ de type fini, $Y$ noethérien, et $\mathcal O_{Y,y}$ réduit à fibres formelles géométriquement normales. Supposons $f$ universellement ouvert en $x$, à fibres équidimensionnelles de même dimension près de $x$, $X_y$ réduit aux générisations maximales de $x$ et $(X_y)_{\mathrm{red}}$ géométriquement normal. Alors $x$ a un voisinage ouvert $U$ tel que $U_{\mathrm{red}} \to Y$ soit plat à fibres géométriquement normales.
\end{theoreme*}
\end{encadre}
{\small Les feuillets en esquissent une démonstration incomplète (pages 9 à 12), avec un \q{lemme à dégager} jamais écrit. D'après le résumé de l'article de Kollár, Hironaka traite le cas d'une base régulière. Mathlib n'a pas les fibres formelles ni les morphismes universellement ouverts. On se reportera aux notes de Grothendieck (\lot{127}{1}{7}).\par}

\begin{encadre}
\begin{theoreme*}[Grothendieck, pages 2 et 3, descente non plate sur une base artinienne\piste{127-non-flat-descent-artinian-epimorphism}]\nonverifie
Sur une base artinienne $Y$, le problème d'un quotient plat $G$ de $F$ qui prolonge $G_U$, avec $G \to i_*G_U$ universellement injectif relativement à $Y$, descend le long de tout épimorphisme de schémas $Y' \to Y$, plat ou non, pourvu que $Y' \to Y$ soit fini, ou que $f$ et la solution soient de présentation finie. La solution, si elle existe, est unique.
\end{theoreme*}
\end{encadre}
{\small Le lemme~1.3 n'est pas démontré, et l'alternative \q{fini ou de présentation finie} vient d'une note au crayon. Mathlib n'a pas la descente le long des épimorphismes de schémas. On se reportera aux notes de Grothendieck (\lot{127}{1}{2}).\par}

\begin{encadre}
\begin{theoreme*}[Grothendieck, pages 1 à 5, 13 et 15, représentabilité par un schéma localement quasi-fini ; voir aussi Murre 1965\piste{131-locally-quasi-finite-representability}]\nonverifie
Un foncteur $F$ sur les schémas au-dessus d'un $S$ localement noethérien est représentable par un $S$-schéma séparé localement quasi-fini si et seulement s'il vérifie la descente fpqc, testée sur $B \to \hat B$, la présentation finie locale, l'effectivité sur $\hat B = \varprojlim B_n$, la pro-représentabilité sur les anneaux artiniens par des anneaux finis sur eux, le critère valuatif de séparation, et deux conditions de \q{modularité}, l'une locale sur les bases locales complètes, l'autre générique.
\end{theoreme*}
\end{encadre}
{\small Les feuillets en esquissent une démonstration incomplète (pages 1 à 5) : la dernière étape s'arrête à la condition de constructibilité, et deux propositions formelles ne sont pas démontrées. Murre traite le cas non ramifié et dit seulement que le cas localement quasi-fini est possible. Mathlib n'a pas les critères de représentabilité de type Artin. On se reportera aux notes de Grothendieck (\lot{131}{1}{1}).\par}

\begin{encadre}
\begin{theoreme*}[Grothendieck, pages 8, 9 et 19, Tor génériques et suites régulières : l'énoncé en un point\piste{94-generic-tor-regular-sequences}]
Soient $A$ un anneau commutatif, $J$ un idéal nilpotent de $A$ ($J^n = 0$), $A_0 = A/J$, et $R$ un $A$-module quelconque. On suppose que les gradués $\mathrm{gr}^k_J(A) = J^kA/J^{k+1}A$ sont des $A_0$-modules libres et que les gradués $\mathrm{gr}^k_J(R) = J^kR/J^{k+1}R$ sont des $A_0$-modules plats. Alors toute suite $A$-régulière $t = (t_1, \ldots, t_r)$ est $R$-régulière, et son image dans $A_0$ est $A_0$-régulière. Si $A$ est local noethérien, il suffit que les $\mathrm{gr}^k_J(A)$ soient plats sur $A_0$ ; si de plus $R$ est de type fini non nul et les $t_i$ dans l'idéal maximal, $t$ est une suite $R$-régulière au sens strict. C'est la situation de $A_{\mathfrak p}$, $\mathfrak p \in U$, dans les lemmes~6 et~16 ; le complexe de Koszul de $t$ résolvant $A/(t)$, on en tire $\mathrm{Tor}_i^A(R, A/(t)) = 0$ pour $i > 0$.
\end{theoreme*}
\end{encadre}
{\small \emph{Démonstration.} Trois outils. (1) Deux sur trois : pour une suite exacte $0 \to M' \to M \to M'' \to 0$ et $t$ faiblement régulière sur $M''$, $t$ est faiblement régulière sur $M'$ si et seulement si elle l'est sur $M$, et $M'/(t)M' \to M/(t)M$ reste injective (c'est l'annulation de $\mathrm{Tor}_1(M'', A/(t))$ que demande la page) ; on le voit élément par élément, par le lemme du serpent. (2) Dévissage : si $t$ est faiblement régulière sur les gradués $\mathrm{gr}^k_J(M)$ pour $k < j$, elle l'est sur $M/J^jM$, par la suite exacte $0 \to \mathrm{gr}^j_J(M) \to M/J^{j+1}M \to M/J^jM \to 0$ et (1) ; avec $J^nM = 0$, elle l'est sur $M$. (3) Platitude : si $\bar t$ est $A_0$-régulière, elle l'est sur tout $A_0$-module plat $N = N \otimes_{A_0} A_0$. Le pas de récurrence du lemme~6 se fait alors ainsi. Supposons $\bar t_1, \ldots, \bar t_k$ déjà $A_0$-régulière, et soit $J^m$ le dernier gradué non nul de $A$ ($J^{m+1} = 0$), libre et non nul sur $A_0$. Par (3) et (2), $(t_1, \ldots, t_k)$ est faiblement régulière sur $A/J^m$, donc, par (1), $J^m/(t)J^m$ s'injecte dans $A/(t)A$, où $t_{k+1}$ est régulier ; il l'est donc sur $J^m/(t)J^m \simeq (A_0/(\bar t))^{(I)}$, $I \neq \emptyset$, et, en restreignant à un facteur, sur $A_0/(\bar t_1, \ldots, \bar t_k)$. Une fois $\bar t$ régulière dans $A_0$, (3) la rend régulière sur chaque $\mathrm{gr}^k_J(R)$ et (2) sur $R$. Comme le dit la note de la page~19, la liberté ne sert, côté module, qu'à travers la platitude, et aucune finitude n'est demandée à $R$. Dans le cas local noethérien, les $\mathrm{gr}^k_J(A)$ sont de type fini sur l'anneau local $A_0$, et plats, donc libres. Lean (\href{\leanblob/Folder94.lean}{\texttt{Folder94.\allowbreak{}lean}}) démontre (1) (\texttt{isWeaklyRegular\_iff\_of\_exact}, \texttt{injective\_mapQ\_of\_exact}), (2) (\texttt{isWeaklyRegular\_quotient\_filt}, \texttt{isWeaklyRegular\_of\_layers}), (3) (\texttt{isWeaklyRegular\_of\_flat}), le pas de récurrence (\texttt{isWeaklyRegular\_quotient\_of\_layers\_free}), l'énoncé (\texttt{isWeaklyRegular\_of\_gr}) et sa forme locale (\texttt{isWeaklyRegular\_of\_gr\_flat\_of\_isLocalRing}, \texttt{isRegular\_of\_gr\_flat\_of\_isLocalRing}).\par}
{\small Ne sont pas démontrés en Lean : le passage de la régularité de $t$ sur $R$ à l'annulation des $\mathrm{Tor}_i$ par le complexe de Koszul (Mathlib n'a ni les complexes de Koszul ni la suite exacte longue des $\mathrm{Tor}$ ; seul l'analogue de $\mathrm{Tor}_1$ ci-dessus l'est), et l'ouvert dense de l'énoncé global ci-dessous. On se reportera aux notes de Grothendieck (\lot{94}{1}{8}).\par}

\begin{encadre}
\begin{theoreme*}[Grothendieck, pages 8 et 9, l'ouvert dense pour $X = S$\piste{94-generic-tor-regular-sequences}]
Soient $A$ un anneau noethérien, $J$ un idéal nilpotent de $A$ tel que $A_0 = A/J$ soit réduit (par exemple le nilradical), et $R$ un $A$-module de type fini. Il existe un ouvert dense $U \subset \operatorname{Spec} A$ tel que, pour tout $\mathfrak p \in U$, toute suite $A_{\mathfrak p}$-faiblement régulière d'éléments de $A_{\mathfrak p}$ soit $R_{\mathfrak p}$-faiblement régulière. On peut prendre pour $U$ le lieu, dans $\operatorname{Spec} A = \operatorname{Spec} A_0$, où les gradués non nuls, en nombre fini, $\mathrm{gr}^k_J(A)$ et $\mathrm{gr}^k_J(R)$ sont libres sur $A_0$.
\end{theoreme*}
\end{encadre}
{\small \emph{Démonstration.} Les gradués sont des $A_0$-modules de type fini, donc de présentation finie, et leur lieu de liberté est ouvert ; l'intersection $U$ de ces lieux contient les idéaux premiers minimaux, où l'anneau réduit $A_0$ se localise en un corps, et un ensemble qui contient les premiers minimaux est dense. Les gradués commutent à la localisation : $\mathrm{gr}^k_J(S^{-1}M) = S^{-1}\mathrm{gr}^k_J(M)$, car $J^k(S^{-1}M)$ est le localisé de $J^kM$ ; si $\mathfrak p$ est au-dessus de $\mathfrak q \in \operatorname{Spec} A_0$, on a donc $\mathrm{gr}^k_J(M_{\mathfrak p}) = (A_0)_{\mathfrak q} \otimes_{A_0} \mathrm{gr}^k_J(M)$, libre sur $(A_0)_{\mathfrak q}$ pour $\mathfrak p \in U$. Le pas de récurrence de l'énoncé en un point vaut avec n'importe quelle $A$-algèbre $B$ au lieu de $A_0$ et n'importe quel module non nul $T$ au lieu de $A$, par la même démonstration ; avec $B = (A_0)_{\mathfrak q}$ et $T = A_{\mathfrak p}$, toute suite d'éléments de $A$ faiblement régulière sur $A_{\mathfrak p}$ l'est sur $R_{\mathfrak p}$. Enfin tout élément de $A_{\mathfrak p}$ est le produit d'une unité par l'image d'un élément de $A$, et la régularité faible ne dépend de la suite qu'à des unités près. Lean (\href{\leanblob/Folder94.lean}{\texttt{Folder94.\allowbreak{}lean}}) démontre la commutation à la localisation (\texttt{isLocalizedModule\_layerMap}, \texttt{layerEquiv}), le pas de récurrence généralisé (\texttt{isWeaklyRegular\_of\_gr'}) et l'énoncé (\texttt{exists\_isOpen\_dense\_isWeaklyRegular'}).\par}

\begin{encadre}
\begin{theoreme*}[Grothendieck, pages 8, 9 et 19, Tor génériques et suites régulières : l'ouvert dense\piste{94-generic-tor-regular-sequences}]\nonverifie
Soient $S = \operatorname{Spec} A$ noethérien, non nécessairement réduit, et $R$ un faisceau cohérent sur un $S$-schéma $X$ de type fini. Il existe un ouvert dense $U \subset S$ tel que $\mathrm{Tor}_i^A(R, A_{\mathfrak p}/(t)) = 0$ pour tout $i > 0$, tout $\mathfrak p \in U$ et toute suite $A_{\mathfrak p}$-régulière~$t$. C'est un substitut de la platitude générique, qui tombe en défaut sur une base non réduite.
\end{theoreme*}
\end{encadre}
{\small Le pas de récurrence du lemme~6, que la page dit \q{bien standard}, est de l'édition, et la page écrit $\mathrm{gr}_J(\mathcal O_X)$ là où l'argument demande $\mathrm{gr}_J(R)$. L'énoncé en un point et le cas $X = S$ ci-dessus, pour la régularité des suites, sont vérifiés en Lean ; restent le passage aux $\mathrm{Tor}$ par le complexe de Koszul, et, pour $X$ de type fini, la platitude générique, que Mathlib n'a pas. On se reportera aux notes de Grothendieck (\lot{94}{1}{8}).\par}

\begin{encadre}
\begin{theoreme*}[Grothendieck, pages 15 et 16, critère de représentabilité sur $\mathrm{Mod}(A)$ ; voir aussi Hall 2013\piste{94-representability-criterion}]\nonverifie
Soit $A$ un anneau noethérien quotient d'un anneau régulier. Un foncteur $F : \mathrm{Mod}(A) \to \mathrm{Ens}$ est de la forme $\mathrm{Hom}_A(P, -)$ avec $P$ fini si et seulement s'il est exact à gauche, commute aux limites inductives filtrantes, vérifie une condition de complétion $\mathfrak m_{\mathfrak p}$-adique et une $g$-adique sur les modules finis, envoie les modules finis sur des modules finis, a une fonction $\mathfrak p \mapsto \dim F(k(\mathfrak p))$ constructible et, pour tout quotient $B$ et tout $B$-module fini $\Omega$, commute génériquement à la réduction de $\Omega$ modulo les systèmes de paramètres. La conservation des produits n'en fait pas partie.
\end{theoreme*}
\end{encadre}
{\small Les feuillets en esquissent une démonstration incomplète (pages 15 et 16) : plusieurs liens sont de l'édition, et la démonstration telle qu'elle est écrite n'est sûre que pour $A$ excellent. Hall énonce un autre critère, par la conservation des produits. Mathlib n'a pas ces conditions de complétion sur les foncteurs de modules. On se reportera aux notes de Grothendieck (\lot{94}{1}{15}).\par}

\noindent Piste dont l'énoncé dépend d'une lecture à vérifier :
\begin{itemize}\small\setlength{\itemsep}{0pt}
\item Cote~94 : pour $A$ noethérien dont tout quotient intègre est génériquement normal, et $F$ exact à gauche, commutant aux limites inductives filtrantes et vérifiant la condition de complétion locale et la finitude locale, la représentabilité de $F$ par un module fini sur un ouvert non vide de chaque $V(\mathfrak p)$ équivaut à la constructibilité de $\mathfrak p \mapsto \dim_{k(\mathfrak p)} F(k(\mathfrak p))$. La réciproque repose sur le milieu de la page~7, en grande partie illisible, et l'hypothèse de normalité sur une lecture incertaine, à vérifier sur le fac-similé. Mathlib n'a pas la constructibilité de ces fonctions de rang. On se reportera aux notes de Grothendieck (\lot{94}{1}{7}).\piste{94-rank-constructibility}
\end{itemize}

\begin{encadre}
\begin{contrexemple}[Page 7, la réciproque de la remarque 5 bis sous la finitude locale]\verifie[\leanblobmain]{Folder94}
Sur $A = k[x, y]$, $k$ un corps infini, soient $a_2, a_3, \dots$ des éléments distincts de $k$ et $h_j = x - a_j$. Le foncteur $F(M) = \varinjlim\,(M \xrightarrow{h_2} M \xrightarrow{h_3} M \to \cdots)$ est l'identité sur chaque $A_{\mathfrak p}$, vérifie la condition de complétion et la finitude locale, et $\dim_{k(\mathfrak p)} F(k(\mathfrak p)) = 1$ pour tout $\mathfrak p$ ; pourtant $F(A_g)$ n'est de type fini sur $A_g$ pour aucun $g \neq 0$, et $F$ n'est représentable sur aucun ouvert non vide de $\operatorname{Spec} A$.
\end{contrexemple}
\end{encadre}
{\small \emph{Démonstration.} Un idéal premier contient au plus un $h_j$, donc presque tous les $h_j$ sont inversibles dans $A_{\mathfrak p}$ et $F$ y est l'identité à partir d'un rang (\texttt{tele\_atPrime\_bijective}) ; d'où les conditions locales et la dimension~$1$ des fibres (\texttt{finrank\_tele\_field}). Un $g \neq 0$ n'est divisible que par un nombre fini de $h_j$, et $F(A_g)$ est la réunion strictement croissante des $(h_2 \cdots h_i)^{-1} A_g$ (\texttt{not\_finite\_tele\_away}, \texttt{not\_representable\_away}). L'exactitude à gauche et la commutation aux limites inductives filtrantes sont classiques et ne sont pas formalisées. Sous la finitude globale, $F(M)$ de type fini pour tout $M$ de type fini, que l'esquisse de la page utilise, la réciproque tient, et sans l'hypothèse sur le lieu normal : sur un ouvert de $V(\mathfrak p)$ où le rang vaut $n$, les modules locaux de la proposition~4 sont libres de rang $n$, $F(B)$ est projectif de type fini et $F(B) \otimes M \to F(M)$ est un isomorphisme en chaque point. Les deux étapes d'algèbre commutative de cet argument sont démontrées en Lean ci-dessous ; la proposition~4 et le passage du foncteur $F$ à ces énoncés ne le sont pas. Quelle finitude la page écrit au juste reste à lire sur le fac-similé.\par}

\begin{encadre}
\begin{theoreme*}[Page 7, rang constant sur un anneau réduit\piste{94-rank-constructibility}]
Soient $B$ un anneau local réduit, de corps résiduel $k$, et $P$ un $B$-module de type fini tel que $\dim_{B_{\mathfrak q}} (B_{\mathfrak q} \otimes_B P) = \dim_k (k \otimes_B P)$ pour tout idéal premier minimal $\mathfrak q$ ($B_{\mathfrak q}$ est alors un corps). Alors $P$ est libre. Par suite, si $P$ est de présentation finie sur un anneau $B$, à localisés libres aux idéaux maximaux, et si $\varphi \colon P \otimes_B M \to N$ est bijectif après localisation en chaque idéal maximal, $P$ est projectif et $N \simeq \operatorname{Hom}_B(P^\vee, M)$.
\end{theoreme*}
\end{encadre}
{\small \emph{Démonstration.} Une base de $k \otimes P$ se relève, par Nakayama, en une surjection $B^n \to P$. En un premier minimal $\mathfrak q$, elle devient une surjection entre deux $B_{\mathfrak q}$-espaces de même dimension $n$, donc une bijection ; les coordonnées d'un élément du noyau ont donc une image nulle dans chaque $B_{\mathfrak q}$, sont dans chaque premier minimal, donc nilpotentes, donc nulles. Aucune hypothèse noethérienne n'est utile. Pour le second point, la projectivité se lit sur les localisés en les idéaux maximaux, de même que la bijectivité de $\varphi$, et $P \otimes M \simeq P^{\vee\vee} \otimes M \simeq \operatorname{Hom}(P^\vee, M)$ pour $P$ projectif de type fini. C'est ce qu'on applique à $P = F(B)$ et $\varphi \colon F(B) \otimes M \to F(M)$ dans la réciproque sous la finitude globale. Lean (\href{\leanblob/Folder94.lean}{\texttt{Folder94.\allowbreak{}lean}}) : \texttt{free\_of\_finrank\_eq\_of\_isReduced}, \texttt{nonempty\_equiv\_hom\_dual}.\par}