\section[Cote 161-3 : le topos d'un produit d'espaces]{Cote 161-3 : le topos d'un produit d'espaces\protect\verifie[\leanblobmain]{Folder161_3}}\label{sec:161-3}

La cote 161-3, \emph{Topos : notes manuscrites (s.d.)}, cinquante-quatre pages que l'inventaire date \q{[vers 1963-1973]}, appartient au même groupe de dossiers que les cotes 161-1 et 161-2 (sections~\ref{sec:161-1} et~\ref{sec:161-2}). C'est un dossier rassemblé : plusieurs chantiers sans lien entre eux y voisinent sous le seul mot \q{Topos}. Le premier, pages~3 à~14, porte sur les produits. Les pages~3 à~8 construisent le produit de deux topos (\lot{161-3}{1}{3}). Les pages~9 à~14 le comparent au produit de deux espaces (\lot{161-3}{1}{9}).

Pour deux espaces topologiques $X$ et $Y$, le produit est le produit cartésien $X \times Y$, dont les rectangles $U \times V$ forment une base d'ouverts. Un topos se donne par ses faisceaux, et le produit des topos $\mathrm{Top}(X)$ et $\mathrm{Top}(Y)$ est l'endroit où vivent les données à deux variables qui sont locales séparément en chacune. Un faisceau sur $X \times Y$ est une telle donnée, d'où un foncteur $\mathrm{Top}(X \times Y) \to \mathrm{Top}(X) \times \mathrm{Top}(Y)$. La question des pages~9 à~14 est de savoir quand c'est une équivalence. Elle n'a rien d'évident : savoir une chose séparément en $x$ et en $y$ n'est pas la savoir en $(x, y)$, de même qu'en algèbre linéaire les fonctions de deux variables ne sont pas toutes des combinaisons de produits $f(x)g(y)$.

\begin{encadre}
\begin{methode*}[Grothendieck, pages 9 à 14, spatialité du locale produit\piste{161-3-locale-spatiality-suprema-proof}]
Pour identifier $\mathrm{Top}(X \times Y)$ et $\mathrm{Top}(X) \times_{\mathrm{top}} \mathrm{Top}(Y)$, on les voit comme faisceaux sur le même site $O_X \times O_Y$ pour deux topologies : la topologie produit $\pi$, dont les faisceaux sont les bifaisceaux, et la topologie $\pi'$ induite par $X \times Y$. On comble l'écart entre elles par trois passages à la borne supérieure dans le treillis des sous-objets, $X \times Y$ étant borne supérieure de rectangles ; la spatialité du locale produit en résulte.
\end{methode*}
\end{encadre}

Tout faisceau pour $\pi'$ l'est pour $\pi$, et le foncteur est un plongement. C'est une équivalence exactement quand les deux topologies coïncident, c'est-à-dire quand tout recouvrement ensembliste $U \times V = \bigcup_i U_i \times V_i$ fait aussi de $U \times V$ la borne supérieure des $U_i \times V_i$ dans le produit des topos. Aux pages~9 et~10, la réponse habituelle : si tout point de $X$ a un système fondamental de voisinages quasi-compacts, le lemme du tube referme l'écart. Aux pages~10 et~11 vient un énoncé plus fort, sous une hypothèse plus faible que la compacité locale.

\begin{encadre}
\begin{theoreme}[Grothendieck, pages 10 et 11, topos d'un produit\pisteresolue{161-3-product-converse}]\label{thm:161-3-produit}
Si toute partie localement fermée non vide de $X$ a un point qui y possède un voisinage relativement quasi-compact, $\mathrm{Top}(X \times Y) \to \mathrm{Top}(X) \times \mathrm{Top}(Y)$ est une équivalence.
\end{theoreme}
\end{encadre}

Les feuillets en esquissent une démonstration : le lemme du tube, puis un plus grand ouvert $U'$ et sa maximalité. L'inclusion $U'' \subset U' \cup \bigcup_i U_i$ qu'elle demande n'y est pas écrite, et l'édition la rétablit.

\noindent\emph{Le langage des cadres.} Les ouverts d'un espace forment un \emph{cadre} (\emph{frame} en anglais) : un treillis complet où l'intersection se distribue sur les réunions quelconques. Un cadre qu'on regarde comme un espace sans points s'appelle un \emph{locale}. En ces termes, le $2$-produit $\mathrm{Top}(X) \times \mathrm{Top}(Y)$ est le topos des faisceaux sur le locale produit des ouverts de $X$ et de $Y$, et la flèche de l'énoncé est une équivalence exactement quand ce locale est spatial, c'est-à-dire égal au locale des ouverts de $X \times Y$. La condition habituelle est la compacité locale d'un facteur.

\noindent\emph{La démonstration, sous la forme où la page la mène.} Lean vérifie le cœur de l'argument, puis sa traduction en termes de locales. Appelons \emph{famille de rectangles} un ensemble $S$ de couples $(U, V)$, formés d'un ouvert $U$ de $X$ et d'un ouvert $V$ de $Y$, stable quand on rétrécit $U$ ou $V$ et stable par réunion quelconque en chaque variable séparément : c'est le \q{$S$} de la page, vu comme l'ensemble des rectangles situés sous la borne supérieure des $U_i \times V_i$ dans le produit des topos. Sous l'hypothèse de l'énoncé, et pour des espaces $X$ et $Y$ quelconques, Lean démontre qu'une telle famille contient tout rectangle $U \times V$ recouvert par ses propres rectangles (\texttt{covering}).

La preuve suit la page. Soit $U \times V$ recouvert par des rectangles $U_i \times V_i$ avec $(U_i, V_i) \in S$. On prend le plus grand ouvert $U'$ de $U$ avec $(U', V) \in S$ ; il existe, puisque $S$ est stable par réunion en la première variable. Si $U' \neq U$, la partie $Z = U \setminus U'$ est localement fermée et non vide : elle a donc un point $x$ muni d'un voisinage $T$ dans $Z$ qui est quasi-compact, et un ouvert $U''$ de $U$ contenant $x$ avec $U'' \cap Z \subset T$. Pour chaque $y \in V$, le lemme du tube au-dessus de $T$ donne un nombre fini d'indices $i$ avec $T \subset \bigcup_i U_i$, et l'intersection $V_y$ des $V_i$ correspondants est un voisinage ouvert de $y$. Comme $U'' \setminus U'$ est contenu dans $T$, on a $U'' \subset U' \cup \bigcup_i U_i$, et $(U' \cup U'', V_y)$ est dans $S$ ; c'est l'inclusion que la page omet, et elle n'y coûte qu'une distinction de cas. La réunion en $y$ donne $(U' \cup U'', V) \in S$, ce qui contredit la maximalité de $U'$, puisque $x \in U'' \setminus U'$.

Lean en tire que ces familles correspondent exactement aux ouverts de $X \times Y$ : à un ouvert $W$ on associe les rectangles qu'il contient, et $W$ en est la réunion (\texttt{iUnion\_rect}, \texttt{eq\_rect}).

\noindent\emph{Le coproduit des cadres.} Sans aucune hypothèse sur $X$ ni sur $Y$, ces familles sont les éléments du coproduit des treillis d'ouverts, et Lean le vérifie aussi. Elles forment un cadre : l'intersection de deux familles est leur intersection ensembliste, la réunion d'une collection est la plus petite famille qui les contient toutes, et la distributivité tient à un lemme sur la famille engendrée par un ensemble $D$ de couples stable quand on rétrécit : elle rencontre un ensemble $A$ de même nature à l'intérieur de la famille engendrée par $D \cap A$ (\texttt{CIdeal.\allowbreak{}instFrame}, \texttt{CIdeal.\allowbreak{}span\_inter}). Un ouvert $U$ de $X$ donne la famille engendrée par $(U, Y)$, un ouvert $V$ de $Y$ celle engendrée par $(X, V)$ (\texttt{CIdeal.\allowbreak{}inl}, \texttt{CIdeal.\allowbreak{}inr}).

Pour deux morphismes de cadres $f$ et $g$ à valeurs dans un même cadre $L$, l'application $S \mapsto \bigvee_{(U, V) \in S} f(U) \wedge g(V)$ est l'unique morphisme de cadres qui prolonge $f$ et $g$ (\texttt{CIdeal.\allowbreak{}lift}, \texttt{CIdeal.\allowbreak{}existsUnique\_lift}) : c'est la propriété universelle du coproduit. Pour l'existence, on vérifie que la borne supérieure ne change pas quand on remplace un ensemble de couples par la famille qu'il engendre ; c'est là que servent la compatibilité de $f$ et $g$ aux réunions et la distributivité de $L$. L'unicité vient du fait que chaque famille est la réunion de ses rectangles (\texttt{CIdeal.\allowbreak{}eq\_iSup\_rect}).

Quand $f$ et $g$ sont les images réciproques par les deux projections, ce morphisme envoie $S$ sur l'ouvert $\bigcup_{(U, V) \in S} U \times V$ de $X \times Y$ (\texttt{toOpens}, \texttt{toOpens\_comp\_inl}, \texttt{toOpens\_comp\_inr}). Il est toujours surjectif (\texttt{toOpens\_surjective}).

\noindent\emph{Les trois passages à la borne supérieure.} La méthode des pages~9 à~14 se vérifie dans le même modèle, au niveau des cadres. Disons que $X$ et $Y$ ont la \emph{propriété de recouvrement} (\texttt{Covers}) si toute famille de rectangles contient les rectangles recouverts par ses propres rectangles : c'est l'égalité des topologies $\pi$ et $\pi'$, lue sur les cadres. Si tout point de $X$ a un système fondamental de voisinages quasi-compacts, la propriété tient (\texttt{covers\_of\_locallyCompact}), et la démonstration est celle de la page. Soit $U \times V$ recouvert par des rectangles $U_i \times V_i$ d'une famille $S$. Pour $x \in U$, soit $K \subset U$ un voisinage compact de $x$ ; pour $y \in V$, le lemme du tube donne un nombre fini de rectangles de $S$ qui recouvrent $K \times \{y\}$, d'où $(\mathring K, V_{x,y}) \in S$ pour un voisinage ouvert $V_{x,y}$ de $y$ (premier passage). La borne supérieure en $y$ donne $(\mathring K, V)$ (deuxième), celle en $x$ donne $(U, V)$ (troisième). La seule égalité de la chaîne, $(\operatorname{Sup}_i U_i) \times V' = \operatorname{Sup}_i (U_i \times V')$, est la stabilité de $S$ par réunions en une variable, qui fait partie de la définition du coproduit des cadres. Sous l'hypothèse plus faible du théorème~\ref{thm:161-3-produit}, la propriété est le résultat \texttt{covering} (\texttt{covers\_of\_hypG}).

Elle rend injective la comparaison \texttt{toOpens} (\texttt{toOpens\_injective\_\allowbreak of\_covers}), qui est donc un isomorphisme de cadres (\texttt{coversEquiv}) ; sous l'hypothèse de la page, c'est l'isomorphisme \texttt{frameEquiv} (\texttt{frameEquiv\_apply}). Le cadre $\mathcal O(X \times Y)$, muni des images réciproques par les deux projections, est alors le coproduit de $\mathcal O(X)$ et $\mathcal O(Y)$ : pour deux morphismes de cadres $f$ et $g$ à valeurs dans un cadre $L$, il existe un unique morphisme de cadres $h$ de $\mathcal O(X \times Y)$ dans $L$ avec $h(U \times Y) = f(U)$ et $h(X \times V) = g(V)$ (\texttt{existsUnique\_opens\_prod}). Le locale produit est spatial.

\begin{remarque}
Isbell démontre le même énoncé sous une hypothèse voisine : toute partie fermée non vide de $X$ a un point qui y possède un voisinage quasi localement compact, c'est-à-dire dont les ouverts forment un treillis continu \cite{gierz2003}. Il procède par récurrence transfinie, et la réciproque vaut pour $X$ complètement régulier \cite[th.~1 et~4]{isbell1981}. Pour $X$ sobre, son hypothèse entraîne celle de la page, et les deux coïncident pour $X$ séparé (remarque de l'édition, qui s'appuie sur \cite[cor.~4.6]{hofmannlawson1978}). La page remplace la récurrence par un seul argument de maximalité. Plewe caractérise la spatialité des produits de locales par un jeu topologique \cite{plewe1996}.
\end{remarque}

\noindent\emph{Comparaison avec l'hypothèse d'Isbell.} Pour $X$ sobre, l'hypothèse de la page est strictement plus faible que celle d'Isbell, et Lean le vérifie sur le contre-exemple d'une réponse publiée sur MathOverflow~\cite{mo516361}.

On part de l'espace $K$ formé d'un point $\bot$, d'un point $p$ et de points isolés $d_{n,m}$ indexés par $\mathbf N \times \mathbf N$ : le seul ouvert qui contient $\bot$ est $K$ tout entier, et un ouvert contient $p$ seulement s'il contient toutes les lignes $R_n = \{d_{n,m} : m \in \mathbf N\}$ à partir d'un certain rang. Toute partie non vide de $K$ a un point isolé dans elle (\texttt{K.\allowbreak{}scattered}), et cela suffit à rendre $K$ sobre, car un point isolé d'un fermé irréductible en est le point générique (\texttt{Scattered.\allowbreak{}quasiSober}, \texttt{Scattered.\allowbreak{}t0Space}). Pourtant $K$ n'est pas quasi localement compact en $p$ (\texttt{K.\allowbreak{}not\_coreCompact}). Un ouvert $W$ de $K \setminus \{\bot\}$ qui contient $p$ contient en effet une ligne entière $R_n$. Si l'on retire de $K \setminus \{\bot\}$ les points $d_{n,m}$ avec $m \geq m_0$, on obtient des ouverts qui croissent avec $m_0$ et recouvrent $K \setminus \{\bot\}$, mais aucun ne contient $W$.

L'espace du contre-exemple est la puissance dénombrable $K^{\mathbf N}$.
\begin{itemize}
\item Il est sobre, parce qu'un produit quelconque d'espaces sobres l'est \cite{gierz2003} : le point générique d'un fermé irréductible a pour coordonnées les points génériques des adhérences de ses projections (\texttt{quasiSober\_pi}).
\item Il vérifie l'hypothèse de la page, comme tout produit d'espaces compacts où chaque partie non vide a un point isolé (\texttt{hypG\_pi}). Dans une partie localement fermée $Z = U \cap H$, avec $U$ ouvert et $H$ fermé, on fixe une à une les coordonnées, en nombre fini, d'un ouvert élémentaire contenu dans $U$, en prenant chaque fois une valeur isolée (\texttt{exists\_isolated\_pi}). La fibre au-dessus des valeurs choisies est compacte par le théorème de Tychonoff, et sa trace sur $H$ est un voisinage compact dans $Z$.
\item Il ne vérifie pas l'hypothèse d'Isbell (\texttt{not\_hypI\_pi}). Un ouvert de $K^{\mathbf N}$ laisse au moins une coordonnée libre, le long de laquelle $K$ est un rétracte de cet ouvert, et l'argument fait en $p$ vaut pour tout espace dont $K$ est un rétracte (\texttt{K.\allowbreak{}not\_coreCompact\_of\_retract}).
\end{itemize}
Le théorème \texttt{hypG\_not\_hypI} rassemble ces faits : un espace sobre peut vérifier l'hypothèse de la page sans vérifier celle d'Isbell. Avec la remarque de l'édition selon laquelle, pour $X$ sobre, l'hypothèse d'Isbell entraîne celle de la page, le théorème~\ref{thm:161-3-produit} est donc strictement plus général que le théorème~4 d'Isbell.

\noindent\emph{Portée de la vérification.} Les noms cités sont ceux de \href{\leanblobmain/Folder161_3.lean}{\texttt{Folder161\_3.\allowbreak{}lean}}, sauf \texttt{quasiSober\_pi}, \texttt{Scattered.\allowbreak{}quasiSober} et \texttt{Scattered.\allowbreak{}t0Space}, résultats généraux que la bibliothèque du projet démontre une fois pour toutes dans \href{\leanblobmain/Upstream/QuasiSoberPiCoreCompact.lean}{\texttt{Upstream/\allowbreak QuasiSoberPiCoreCompact.lean}}. Lean démontre l'argument de la page dans le modèle des familles de rectangles, les trois passages à la borne supérieure des pages~9 et~10, la bijection avec les ouverts de $X \times Y$, la propriété universelle du coproduit des cadres, la spatialité du locale produit sous l'une ou l'autre hypothèse, puis le contre-exemple \texttt{hypG\_not\_hypI}. Reste le côté des topos : l'égalité $\pi = \pi'$ des topologies elles-mêmes, et l'identification des faisceaux sur le locale produit au $2$-produit $\mathrm{Top}(X) \times \mathrm{Top}(Y)$. Mathlib n'a pas de $2$-catégorie des topos, et l'équivalence de l'énoncé n'est démontrée qu'au niveau des cadres. Lean ne vérifie pas non plus la remarque de l'édition selon laquelle, pour $X$ sobre, l'hypothèse d'Isbell entraîne celle de la page. Elle repose sur le théorème de Hofmann et Lawson : un espace sobre quasi localement compact est localement quasi-compact \cite[cor.~4.6]{hofmannlawson1978}.

Ne sont pas démontrés ici : la construction du $2$-produit de topos (pages~3 à~8) ; le cas d'un produit infini (pages~11 et~12) au-delà des cadres d'ouverts, démontré ci-dessous ; la question de la page~14, sur des facteurs discrets, que la page laisse sur un point d'interrogation.

\begin{encadre}
\begin{theoreme*}[Grothendieck, pages 3 à 8, 2-produit de topos\piste{161-3-two-product-by-intersection}]\nonverifie
Le 2-produit des topos $\tilde C$ et $\tilde D$ existe : c'est l'intersection, dans le topos des préfaisceaux sur $C \times D$, des images réciproques des sous-topos $\tilde C \subset \hat C$ et $\tilde D \subset \hat D$. Les familles quelconques de topos ont de même un 2-produit.
\end{theoreme*}
\end{encadre}
\begin{demopage}[pages 3 à 8]
SGA~4 ne construit pas ce produit : la remarque~IV~5.13 renvoie à un §~15 qui n'a pas paru, et VI~§~8 ne traite que des limites projectives cofiltrantes \cite{sga4-1}. SGA~4 énonce en revanche (IV~9.1.2~d) et 9.1.3) que l'intersection de sous-topos est le topos des faisceaux pour la borne supérieure des topologies, ce qu'utilise la page. La construction par intersection elle-même figure chez Pitts (\emph{Cahiers} 26, 1985, preuve du théorème~2.3), qui la donne comme connue, et chez Caramello et Lafforgue (2025, lemme~III.1.9~(ii), théorème~III.1.10~(ii)) pour les produits finis. Dans $\widehat{C \times D}$, les préfaisceaux qui sont des faisceaux en la première variable, resp. la seconde, forment deux sous-topos, dont les bifaisceaux sont l'intersection (pp.~3--4). Ce sont les images réciproques de $\tilde C \subset \hat C$ et $\tilde D \subset \hat D$ par les projections, et $\widehat{C \times D}$ est le 2-produit de $\hat C$ et $\hat D$, les foncteurs exacts à gauche sur $C \times D$ correspondant aux couples de tels foncteurs sur $C$ et sur $D$ (pp.~5--6). Pour une famille, la page prend le produit restreint des $C_i$ et l'intersection des images réciproques (pp.~7--8). L'existence de l'intersection de sous-topos n'est pas énoncée.
\end{demopage}
{\small Les sous-topos sont ici les sous-catégories réflexives à réflecteur exact à gauche de la section~\ref{sec:161-1}.\par}

\begin{encadre}
\begin{theoreme*}[Grothendieck, pages 11 et 12, topos d'un produit infini\piste{161-3-infinite-product-criterion}]\nonverifie
Pour une famille quelconque d'espaces $(X_i)$, $\mathrm{Top}(\prod X_i) \to \prod \mathrm{Top}(X_i)$ est une équivalence quand tous les facteurs sauf un au plus ont des systèmes fondamentaux de voisinages quasi-compacts et que tous sauf un au plus sont quasi-compacts.
\end{theoreme*}
\end{encadre}
\begin{demopage}[pages 11 et 12]
Le cas fini se tire du cas de deux facteurs (p.~11). En général, $I$ étant réunion filtrante de parties finies $J_\alpha$, le 2-produit est le topos des faisceaux sur la catégorie $\mathcal O'_Z$ des ouverts de $Z = \prod X_i$ venus d'un $Z_\alpha = \prod_{i \in J_\alpha} X_i$, pour la topologie limite ; il reste à voir qu'elle est la topologie induite par $Z$. Pour $W = U \times Z'_\alpha$ recouvert par des $V_\lambda$, la quasi-compacité de $Z'_\alpha = \prod_{i \notin J_\alpha} X_i$ donne pour chaque $z \in U$ un voisinage $U_z$ tel que $U_z \times Z'_\alpha$ soit majoré par la borne supérieure $S$ des $V_\lambda$, d'où $S \geq W$ (p.~12). Cet argument suppose quasi-compacts tous les facteurs hors d'un nombre fini.
\end{demopage}

\noindent\emph{Le cas des cadres d'ouverts.} Comme pour deux facteurs, la page raisonne sur le produit restreint $\prod' \mathcal O_{X_i}$, au niveau des cadres d'ouverts. C'est cette forme de l'énoncé que Lean démontre, sous une hypothèse un peu plus faible que celle de la page, celle que dégage la note de la lecture.

\begin{encadre}
\begin{enonce}[Grothendieck, pages 11 et 12, forme des cadres d'ouverts]\verifie[\leanblobmain]{Folder161_3}
Soit $(X_i)_{i \in I}$ une famille quelconque d'espaces topologiques. On appelle \emph{pavé} une famille $(U_i)$ d'ouverts avec $U_i = X_i$ sauf pour un nombre fini d'indices, et on note $\bigotimes_i \mathcal O(X_i)$ le cadre des ensembles de pavés stables par rétrécissement et par réunion quelconque en chaque coordonnée séparément.
\begin{enumerate}
\item[(a)] Muni des injections $U \mapsto \mathrm{pr}_i^{-1}(U)$, $\bigotimes_i \mathcal O(X_i)$ est le coproduit des cadres $\mathcal O(X_i)$.
\item[(b)] Si tous les $X_i$ sauf un au plus sont localement quasi-compacts, et si tous sauf un nombre fini sont quasi-compacts, l'application $S \mapsto \bigcup_{(U_i) \in S} \prod_i U_i$ est un isomorphisme de cadres de $\bigotimes_i \mathcal O(X_i)$ sur $\mathcal O(\prod_i X_i)$. Le cadre $\mathcal O(\prod_i X_i)$, muni des images réciproques par les projections, est alors le coproduit des $\mathcal O(X_i)$ : le locale produit est spatial.
\end{enumerate}
En particulier, l'hypothèse de la page (« tous sauf au plus un », deux fois) suffit.
\end{enonce}
\end{encadre}

\begin{proof}
(a) Un élément $S$ est la borne supérieure de ses pavés, et un pavé est la borne inférieure \emph{finie} des $\mathrm{pr}_i^{-1}(U_i)$, $U_i \neq X_i$ ; un morphisme de cadres est donc déterminé par ses composées avec les injections, et $S \mapsto \bigvee_{(U_i) \in S} \bigwedge_i f_i(U_i)$ le fournit. La loi distributive se démontre comme pour deux facteurs.

(b) L'application est surjective sans hypothèse, car tout ouvert du produit est réunion des pavés qu'il contient. Pour l'injectivité, il faut voir qu'un $S$ contient tout pavé $u$ que ses pavés recouvrent ensemblistement. D'abord un lemme du tube, sans hypothèse : un produit de parties compactes $\prod_i K_i$ recouvert par les pavés de $S$ est contenu dans un seul pavé de $S$. Par Tychonoff, un nombre fini de pavés suffisent, à supports dans une partie finie $H$, et l'on raisonne coordonnée par coordonnée sur $H$, par la récurrence des parties compactes, les autres coordonnées étant figées en un point. Soient ensuite $e$ l'indice exceptionnel et $G$ la partie finie des indices où $u_i \neq X_i$ ou bien $X_i$ n'est pas quasi-compact. On passe à la borne supérieure sur chaque coordonnée de $G$ autre que $e$, au moyen de voisinages compacts $K_i \subset u_i$. On passe enfin à la borne supérieure sur les points $y$ de la coordonnée $e$ : le compact $\prod_{i \in G \setminus \{e\}} K_i \times \{y\} \times \prod_{i \notin G \cup \{e\}} X_i$ est dans $\prod u_i$, donc dans un pavé de $S$, ce qui donne un voisinage de $y$.
\end{proof}

\noindent Lean : \href{\leanblobmain/Folder161_3.lean}{\texttt{PIdeal.\allowbreak{}existsUnique\_lift}} pour (a) ; \href{\leanblobmain/Folder161_3.lean}{\texttt{PIdeal.\allowbreak{}exists\_box\_of\_isCompact}} pour le lemme du tube, \href{\leanblobmain/Folder161_3.lean}{\texttt{piCovers}} pour la spatialité, \href{\leanblobmain/Folder161_3.lean}{\texttt{piCoversEquiv}} et \href{\leanblobmain/Folder161_3.lean}{\texttt{existsUnique\_opens\_pi}} pour (b), \href{\leanblobmain/Folder161_3.lean}{\texttt{piFrameEquiv}} pour l'hypothèse de la page.

\begin{remarque}
La démonstration de Lean ne suit pas le chemin de la page, qui passe par les produits finis $\prod_{i \in J_\alpha} X_i$ et la limite filtrante sur $\alpha$ : elle va directement au produit restreint, et les passages à la borne supérieure sont ceux des pages~9 et~10. Reste le côté des topos : l'identification des faisceaux sur le locale produit au $2$-produit $\prod^{\mathrm{top}} \mathrm{Top}(X_i)$. Mathlib n'a pas de $2$-catégorie des topos.
\end{remarque}
\section[Cote 37 : le contre-exemple à EGA I 10.10.5]{Cote 37 : le contre-exemple à EGA~I 10.10.5\protect\verifie{Folder37}}\label{sec:37}

La cote 37, \emph{Rééditions SGA, EGA [SGA 4 à SGA 7, EGA I et EGA II]}, quatre-vingt-dix-neuf pages de tapuscrits, de lettres et de notes, dont l'inventaire date les lettres \q{(1967-1971, s.d.)}, est un dossier de travail éditorial : les rééditions de SGA~1, 4, 5, 6 et~7 et d'EGA~I et~II, avec les lettres échangées et quelques morceaux de mathématiques inédits. La page~92 est une lettre dactylographiée à Dieudonné, datée à la main du 27.8.1967. Dieudonné avait tiqué sur la généralisation proposée d'EGA~I 10.10.5 hors du cas noethérien ; la lettre admet que les conditions a) et c) \q{ne son[t] pas impliquées par b)} et le montre sur $A = B[[T]]$, $A_n = B[T]/(T^{n+1})$, $M_n = A_n/J_n$ avec $J_n = (X_0, X_1T, \ldots, X_nT^n)$ et $B = k[(X_i)_{i \geq 0}]$, pour lequel les générateurs écrits de $J_n$ sont \q{en nombre minimal} (\lot{37}{5}{92}). La lettre affirme pour cela que ces générateurs sont linéairement indépendants sur $B$ dans $J_n/TJ_n$ ; c'est faux : $X_0 \cdot X_1T = T \cdot X_1X_0 \in TJ_n$. Sa réduction modulo les $X_j$, $j \neq i$, montre seulement que chaque coefficient est dans l'idéal $(X_j)_{j \geq 0}$, et cela suffit. La lecture rédige ainsi la minimalité et ajoute l'étape de Schanuel, que la lettre laisse implicite.

\noindent\emph{Conventions.} $k$ est un corps, $B = k[X_0, X_1, \ldots]$, $P = B[T]$, $A_n = P/(T^{n+1})$ et $J_n \subset A_n$ l'idéal engendré par les classes de $X_lT^l$, $0 \leq l \leq n$. Pour $f \in P$, on note $\lambda_i(f) \in k$ le coefficient du monôme $X_iT^i$ et $\varepsilon(f) \in k$ le terme constant ; $\varepsilon$ est un homomorphisme d'anneaux, $\lambda_i$ est $k$-linéaire.

\begin{lemme}\label{lem:37-lambda}
Pour $a \in P$ et $i, l \geq 0$, $\lambda_i(a \cdot X_lT^l)$ vaut $\varepsilon(a)$ si $l = i$ et $0$ sinon. Pour $i \leq n$, $\lambda_i(a\,T^{n+1}) = 0$.
\end{lemme}

\begin{proof}
Tout monôme de $a\,X_lT^l$ est divisible par $X_lT^l$. Le monôme $X_iT^i$ ne l'est que si $l = i$, et le coefficient de $X_iT^i$ dans $a\,X_iT^i$ est alors celui du monôme $1$ dans $a$. Tout monôme de $a\,T^{n+1}$ a un degré en $T$ au moins $n + 1 > i$.
\end{proof}

\begin{theoreme}[Grothendieck, page 92, minimalité des générateurs\piste{37-ega-i-10-10-5-counterexample}]\label{thm:37-minimal}
L'idéal $J_n$ de $A_n$ est engendré par $n + 1$ éléments et ne l'est par aucune famille de moins de $n + 1$ éléments.
\end{theoreme}

\begin{proof}
Soient $g_1, \ldots, g_m$ des générateurs de $J_n$. On écrit chaque $X_jT^j$, $0 \leq j \leq n$, comme combinaison $\sum_r a_{jr}g_r$, et chaque $g_r$ comme combinaison $\sum_l b_{rl}X_lT^l$, puis on relève tout dans $P$ : les égalités y valent à un multiple de $T^{n+1}$ près. Appliquons $\lambda_i$, $i \leq n$, à la première. Par le lemme~\ref{lem:37-lambda}, le membre de gauche donne $\delta_{ij}$, le multiple de $T^{n+1}$ ne contribue pas, et chaque $a_{jr}g_r$ donne $\sum_l \lambda_i(a_{jr}b_{rl}X_lT^l) = \varepsilon(a_{jr})\,\varepsilon(b_{ri})$. Les matrices $E = (\varepsilon(a_{jr}))$, de taille $(n+1) \times m$, et $L = (\varepsilon(b_{ri}))$, de taille $m \times (n+1)$, à coefficients dans $k$, vérifient donc $EL = 1$. Le rang de l'identité, $n + 1$, est au plus celui de $E$, lui-même au plus $m$.
\end{proof}

\begin{enonce}[Page 92, compatibilité]\label{prop:37-compat}
Le $A_n$-module $M_n = A_n/J_n$ est de présentation finie, et la réduction $A_{n+1} \to A_n$ envoie $J_{n+1}$ sur $J_n$ : les $M_n$ forment un système compatible.
\end{enonce}

\begin{proof}
$M_n$ est le quotient de $A_n$ par un idéal de type fini. L'image de $J_{n+1}$ est engendrée par les classes de $X_lT^l$, $l \leq n + 1$, et $X_{n+1}T^{n+1}$ est nul dans $A_n$.
\end{proof}

\begin{lemme}[l'étape de Schanuel]\label{lem:37-schanuel}
Soient $S$ un anneau commutatif, $J$ un idéal de $S$, $F$ un $S$-module projectif, $\varphi : F \to N$ surjective et $\gamma : K \to F$ d'image le noyau de $\varphi$, où $K$ est engendré par $p$ éléments. Si $N \simeq S/J$, alors $J$ est engendré par $p + 1$ éléments.
\end{lemme}

\begin{proof}
Soit $\varphi' : F \to S/J$ le composé de $\varphi$ et de l'isomorphisme. Comme $F$ est projectif, $\varphi'$ se relève en $\psi : F \to S$ ; comme $\varphi'$ est surjective, il existe $x_0 \in F$ d'image la classe de $1$, et l'on pose $\chi(s) = s x_0$. Alors $c = 1 - \psi(x_0)$ est dans $J$, et les $\psi(\gamma(v_r))$, pour des générateurs $v_1, \ldots, v_p$ de $K$, aussi, puisque $\varphi \circ \gamma = 0$. Réciproquement, pour $x \in J$, $\varphi'(\chi(x))$ est la classe de $x$, nulle, donc $\chi(x) = \gamma(y)$ pour un $y \in K$, et $x = xc + x\,\psi(x_0) = xc + \psi(\gamma(y))$ est dans l'idéal engendré par $c$ et les $\psi(\gamma(v_r))$.
\end{proof}

\begin{theoreme}[D'après la page 92, contre-exemple à EGA~I 10.10.5, sous une forme plus générale\piste{37-ega-i-10-10-5-counterexample}]\label{thm:37-contre}
Soient $A$ un anneau commutatif quelconque et, pour tout $n$, un homomorphisme d'anneaux quelconque $A \to A_n$. Il n'existe pas de $A$-module de présentation finie $M$ tel que $A_n \otimes_A M \simeq M_n$ comme $A_n$-modules pour tout $n$. En particulier, pour $A = B[[T]]$ et ses réductions, le système compatible $(M_n)$ de modules de présentation finie ne vient d'aucun $A$-module de présentation finie : la condition b) d'EGA~I 10.10.5 n'entraîne pas a) et c) sans hypothèse noethérienne.
\end{theoreme}

\begin{proof}
Soit $A^p \xrightarrow{\gamma_0} A^q \xrightarrow{\varphi_0} M \to 0$ une présentation. Le produit tensoriel par $A_n$ est exact à droite : $A_n \otimes_A A^p \to A_n \otimes_A A^q \to A_n \otimes_A M \to 0$ est exact, le module du milieu est libre, et celui de gauche est engendré par $p$ éléments. Si $A_n \otimes_A M \simeq A_n/J_n$, le lemme~\ref{lem:37-schanuel} engendre $J_n$ par $p + 1$ éléments, et le théorème~\ref{thm:37-minimal} donne $n + 1 \leq p + 1$ pour tout $n$, ce qui est absurde pour $n = p + 1$.
\end{proof}

\begin{remarque}
Le contre-exemple tient tel que la lettre l'énonce, et plus généralement. Ni la complétude de $A$, ni la surjectivité des $A \to A_n$, ni la compatibilité des isomorphismes ne servent : une présentation de $M$ par $q$ générateurs et $p$ relations borne uniformément, par $p + 1$, le nombre de générateurs de chaque $J_n$. La borne de la lecture, $p + q$, est remplacée par $p + 1$. La minimalité est démontrée comme la lecture la rédige, par l'indépendance des $n+1$ générateurs dans $J_n/(TJ_n + \mathfrak m J_n)$, $\mathfrak m = (X_j)_{j \geq 0}$, mise en équations : les formes $\lambda_i$ sont nulles sur $TJ_n + \mathfrak m J_n$ et valent $\delta_{il}$ sur $X_lT^l$.
\end{remarque}

Ne sont pas démontrés ici : les schémas formels et les conditions a), b), c) d'EGA~I 10.10.5 elles-mêmes, que la page ne rappelle pas ; l'implication a) $\Rightarrow$ c) sans hypothèse noethérienne, que les deux correspondants laissent ouverte ; le \q{canular} d'EGA~IV 17.1.6 (i) que signale la page~93.
\bigskip
\noindent Autres pistes de l'onglet Findings pour ce thème, dans des cotes qui n'ont pas de section ici :\par

\begin{encadre}
\begin{theoreme*}[Grothendieck, pages 86 à 88, finitude de la normalisation\piste{23-finite-normalisation-quotient-of-regular}]\nonverifie
Soit $A$ un anneau noethérien intègre quotient d'un anneau régulier. La clôture intégrale de $A$ est finie sur $A$ si et seulement si les premiers $\mathfrak p$ de hauteur un tels que $A_{\mathfrak p}$ n'est pas régulier sont en nombre fini et que, pour chacun, la normalisée de $A_{\mathfrak p}$ est finie sur $A_{\mathfrak p}$.
\end{theoreme*}
\end{encadre}
{\small Les feuillets en esquissent une démonstration incomplète : ils construisent $C = i_*i^*\tilde B$ à travers un fermé de codimension $\geq 2$ et la montrent $(S_2)$ et $(R_1)$ par le critère de Serre ; l'universelle caténarité de $A$ vient de l'édition, et la cohérence de $C$ repose sur une phrase dont le milieu est illisible.\par}

\begin{encadre}
\begin{theoreme*}[Grothendieck, page 22, quand $\mathrm{Ind}(C)$ est un topos\piste{37-ind-topos-exercise}]\nonverifie
Pour une petite catégorie $C$ d'enveloppe de Karoubi $C'$, $\mathrm{Ind}(C)$ est un topos si et seulement si $C'$ a les limites inductives finies et que son foncteur canonique vers les faisceaux pour la topologie finitaire les respecte ; ce topos est alors parfait exactement quand $C'$ a les limites projectives finies.
\end{theoreme*}
\end{encadre}
{\small Mathlib n'a pas les conditions de SGA~4 pour que $\mathrm{Ind}(C)$ soit un topos. On se reportera aux notes de Grothendieck (\lot{37}{2}{22}).\par}

\begin{encadre}
\begin{conjecture*}[Grothendieck, pages 1 à 4, Dold--Kan hors de $\Delta$\piste{112-linearization-beyond-the-simplex}]
Pour une petite catégorie $A$, la restriction aux préfaisceaux abéliens \q{lisses}, ceux le long desquels la linéarisation ne varie pas, donne une correspondance de type Dold--Kan avec une catégorie dérivée de complexes localement constants. La page pose la question sous plusieurs formes et relève que $L_b$ porte des coefficients tordus et non constants.
\end{conjecture*}
\end{encadre}
{\small Mathlib n'a pas les catégories dérivées de complexes localement constants. On se reportera aux notes de Grothendieck (\lot{112}{1}{1}).\par}

\begin{encadre}
\begin{theoreme*}[Grothendieck, pages 6 et 7, recollement de topos de préfaisceaux\piste{116-presheaf-gluing-continuous-gluing-functor}]\nonverifie
Un topos recollé d'un sous-topos ouvert $X_0$ et de son fermé complémentaire $X_1$ le long d'un foncteur exact à gauche $\varphi$ est un topos de préfaisceaux exactement quand $X_0$ et $X_1$ sont de la forme $\mathrm{Top}(\mathcal X_0)$ et $\mathrm{Top}(\mathcal X_1)$ et que $\varphi$ commute aux limites projectives quelconques ; la donnée de recollement est alors un bifoncteur $\mathcal X_0^{\mathrm{op}} \times \mathcal X_1 \to (\mathrm{Ens})$.
\end{theoreme*}
\end{encadre}
{\small Mathlib n'a pas le recollement des topos. On se reportera aux notes de Grothendieck (\lot{116}{1}{6}).\par}