\section[Cote 121 : la décomposition cellulaire admissible la plus grossière]{Cote 121 : la décomposition cellulaire admissible la plus grossière\protect\verifie{Folder121}}\label{sec:121} La cote 121, \emph{Topologie modérée}, cherche dans sa première mouture une notion de partie \q{modérée} d'un espace topologique $X$. Les pages~3 à~5 posent une algèbre de Boole $\mathcal F$ de parties de $X$ et les conditions c~bis) ($A \in \mathcal F \Rightarrow \overline A \in \mathcal F$), d) (tout $A \in \mathcal F$ contient un ouvert dense de son adhérence) et e) (toute suite décroissante de fermés de $\mathcal F$, chacun rare dans le précédent, est stationnaire à $\varnothing$) (\lot{121}{1}{4}, \lot{121}{1}{5}). La page~8 montre que la frontière d'un membre est rare (\lot{121}{1}{8}). La page~10 appelle décomposition cellulaire une partition finie de $X$ telle que (1) l'adhérence de chaque cellule soit une réunion de cellules et (2) deux cellules distinctes aient des adhérences distinctes ; elle est $\mathcal F$-admissible si ses cellules sont dans $\mathcal F$ (\lot{121}{1}{10}). La page~14 énonce la proposition suivante et en démontre l'existence par récurrence, en retirant la réunion des frontières et en s'arrêtant par e) (\lot{121}{1}{14}). Comme dans la lecture, on prend dans d) l'intérieur relatif à l'adhérence. \begin{encadre} \begin{theoreme}[Grothendieck, page 14\piste{121-coarsest-cell-decomposition}] Soit $\mathcal F$ une algèbre de Boole de parties d'un espace topologique, stable par adhérence, dont chaque membre contient un ouvert dense de son adhérence, et dans laquelle toute suite décroissante de membres fermés, chacun rare dans le précédent, aboutit à $\varnothing$. Toute sous-famille finie $\mathcal L \subset \mathcal F$ admet une décomposition cellulaire $\mathcal F$-admissible dont chaque élément de $\mathcal L$ est réunion de cellules, et parmi ces décompositions une plus grossière que toutes les autres. \end{theoreme} \end{encadre} \noindent L'énoncé tient : voir \texttt{page14}, avec le lemme de la page~8 (\texttt{Tame.\allowbreak{}rare\_bd}), dans \href{\leanblob/Folder121.lean}{\texttt{Folder121.\allowbreak{}lean}}. La récurrence porte sur un fermé $Z \in \mathcal F$ quelconque à la place de $X$ (\texttt{exists\_coarsest}), la frontière d'un membre étant prise relativement à $Z$. La page affirme sans argument que la décomposition obtenue est la plus grossière ; l'argument de l'édition (\texttt{subset\_bd}) est qu'une cellule d'une décomposition dont $Y$ est réunion de cellules, si elle rencontre la frontière de $Y$, y est contenue, de sorte que toute décomposition admissible convenable se restreint à la partie retirée et raffine les cellules ouvertes. La page~9 ajoute la condition f) : pour $B, C$ fermés de $\mathcal F$, les composantes connexes du localement fermé $B \setminus C$ sont en nombre fini et appartiennent à $\mathcal F$ (\lot{121}{1}{9}). La remarque de la page~16 en tire la version à cellules connexes (\lot{121}{1}{16}). \begin{encadre} \begin{theoreme}[Grothendieck, page 16\piste{121-coarsest-cell-decomposition}] Si $\mathcal F$ satisfait de plus f), toute sous-famille finie $\mathcal L \subset \mathcal F$ admet une décomposition cellulaire $\mathcal F$-admissible à cellules connexes dont chaque élément de $\mathcal L$ est réunion de cellules, et parmi ces décompositions à cellules connexes une plus grossière que toutes les autres. \end{theoreme} \end{encadre} \noindent L'énoncé tient : voir \texttt{page16} et \texttt{exists\_\allowbreak{}coarsest\_conn}. La récurrence est celle de la page~14, les cellules ouvertes $U_i$ étant remplacées par leurs composantes connexes, comme le dit la page. Une cellule $U_i$ s'écrit $\overline{U_i} \setminus X'$, de sorte que f) s'applique à elle. Une composante $V$ de $U_i$ vérifie $\overline V \cap U_i \subset V$, car $\overline V \cap U_i$ est connexe ; avec le fait que l'adhérence d'une $U_i$ ne rencontre aucune autre $U_j$, cela donne la condition de frontière et la distinction des adhérences. Pour \q{la plus grossière}, une cellule connexe d'une décomposition concurrente contenue dans $U_i$ est contenue dans une composante de $U_i$ ; chaque composante est donc réunion de cellules de la décomposition concurrente, qui se restreint alors à $X'$ en une décomposition convenable pour la famille $\{Y \cap X'\} \cup \{\overline V \cap X'\}$. Ne sont pas démontrés ici : les corollaires de la page~15 et les décompositions régulières de la page~17. \section[Cote 120 : sommes amalgamées, écraser une partie modérée sur un corps]{Cote 120 : sommes amalgamées, écraser une partie modérée sur un corps\protect\verifie{Folder120}}\label{sec:120} La cote 120, \emph{Topologie modérée}, vingt-quatre pages que l'inventaire date \q{à partir de 1973 --- à partir de 1978}, cherche des axiomes pour les parties \q{modérées} des puissances d'un ensemble $R$. La page~2 pose les axiomes (M1) à (M4) sur des familles $\mathcal M_n$ de parties de $R^n$, que la page~4 transcrit pour des ensembles d'indices finis quelconques ; la page~5 appelle modérée une application dont le graphe est une partie modérée. L'axiome (M6) de la page~12 demande que toute partie modérée $Y$ d'un espace modéré $X$ soit une fibre $\bigcap_\alpha f_\alpha^{-1}(e_\alpha)$ d'un nombre fini de fonctions modérées, les $e_\alpha$ étant des points modérés, \q{de plus, on peut supposer} que les $f_\alpha$ séparent les points de $X \smallsetminus Y$ : c'est dire que le quotient $X/Y$, où $Y$ est écrasé en un point, existe au sens strict. La section~(VI) suppose $R$ un corps et ajoute l'axiome (M11) : $0$ et $1$ sont des points modérés, $x - y$ et $xy$ sont des fonctions modérées sur toute partie modérée de $R^2$, et les inverses d'une partie modérée de $R^*$ sont contenus dans une partie modérée (\lot{120}{1}{20}). Les pages~22 et~23 en tirent que la seconde moitié de (M6) découle de la première : la page~22 se ramène à $e_\alpha = 0$ par translation et introduit les produits $f_\alpha g_\beta$, la page~23 vérifie la séparation et énonce la proposition \q{Si on a M1 : M7 et M11 \ldots}, dont la \q{Dém :} reste vide (\lot{120}{2}{22}). Le manuscrit écrit \q{$e_\alpha \in R$} et \q{sépare les pts de $X$} ; la lecture corrige en $e_\alpha \in R_0$ et en $X \smallsetminus Y$. \noindent\emph{Conventions.} Pour un ensemble fini $I$, $\mathcal M_I$ est un ensemble de parties de $R^I$ ; pour $u : I \to J$, $u^* : R^J \to R^I$ est $x \mapsto x \circ u$. Les axiomes, sous la forme (M$'$1) à (M$'$4) de la page~4, sont : (M$'$1) $u^*(A) \in \mathcal M_I$ pour $A \in \mathcal M_J$ ; (M$'$2) $(u^*)^{-1}(B) \in \mathcal M_J$ pour $u$ surjective et $B \in \mathcal M_I$ ; (M$'$3) $(u^*)^{-1}(B) \cap A \in \mathcal M_J$ ; (M$'$4) $A \times B \in \mathcal M_{I \sqcup J}$ pour $A \in \mathcal M_I$, $B \in \mathcal M_J$. Le graphe d'une famille $F : R^I \to R^K$ au-dessus de $X \subset R^I$ est $\Gamma_F = \{(x, F(x)) \mid x \in X\} \subset R^{I \sqcup K}$. Une fonction $f : X \to R$ est modérée si son graphe est dans $\mathcal M_{I \sqcup \{\ast\}}$, et $R_0$ est l'ensemble des $c \in R$ tels que $\{c\} \in \mathcal M_{\{\ast\}}$. Un espace modéré est ici une partie modérée $X \in \mathcal M_I$, et des fonctions modérées $g_\beta$ le plongent si $x \mapsto (g_\beta(x))_\beta$ est injective sur $X$. \begin{lemme}[pages 5 et 20]\label{lem:120-anneau} Soient $X \in \mathcal M_I$ et $f$, $g$ des fonctions modérées sur $X$. \begin{enumerate} \item Le graphe de $(f, g) : X \to R^2$ est modéré, ainsi que son image. \item Si $F : R^I \to R^K$ a un graphe modéré au-dessus de $X$ et si $h$ est une fonction modérée sur $F(X)$, alors $h \circ F$ est modérée sur $X$. \item Si $R$ est un anneau commutatif vérifiant (M11)~b), $f - g$ et $fg$ sont modérées. Les constantes $c \in R_0$ et les coordonnées $x \mapsto x_i$ sont modérées sur $X$. \end{enumerate} Seuls servent (M$'$1), (M$'$2), (M$'$4) et (M11)~b). \end{lemme} \begin{proof} 1. Soit $w : (I \sqcup \{\ast\}) \sqcup (I \sqcup \{\ast\}) \to I \sqcup \{0, 1\}$ l'application qui envoie les deux copies de $I$ sur $I$, la première étoile sur $0$ et la seconde sur $1$ ; elle est surjective. Un $y \in R^{I \sqcup \{0,1\}}$ a son image $w^*(y)$ dans $\Gamma_f \times \Gamma_g$ si et seulement si $y|_I \in X$, $y_0 = f(y|_I)$ et $y_1 = g(y|_I)$ : la préimage de $\Gamma_f \times \Gamma_g$, modérée par (M$'$4) puis (M$'$2), est le graphe de $(f, g)$. Plus généralement, l'image $F(X)$ d'une famille de graphe modéré est la projection de ce graphe sur $R^K$, modérée par (M$'$1). 2. On forme $\Gamma_F \times \Gamma_h \subset R^{(I \sqcup K) \sqcup (K \sqcup \{\ast\})}$, modéré par (M$'$4), et on le tire en arrière par la surjection $(I \sqcup K) \sqcup (K \sqcup \{\ast\}) \to (I \sqcup K) \sqcup \{\ast\}$ qui identifie les deux copies de $K$ : on obtient, par (M$'$2), l'ensemble des $(x, F(x), h(F(x)))$, $x \in X$. Sa projection sur $R^{I \sqcup \{\ast\}}$, modérée par (M$'$1), est le graphe de $h \circ F$. 3. On applique le point~2 à $F = (f, g)$, dont l'image est modérée par le point~1, et à $h$ égale à $(z_0, z_1) \mapsto z_0 - z_1$ ou $z_0 z_1$, modérée sur cette image par (M11)~b). Le graphe de la constante $c$ est $X \times \{c\}$, modéré par (M$'$4) ; celui de la coordonnée $x_i$ est l'image de $X$ par $u^*$, où $u : I \sqcup \{\ast\} \to I$ est l'identité sur $I$ et envoie $\ast$ sur $i$, modérée par (M$'$1). \end{proof} \begin{lemme}[pages 22 et 23, l'argument]\label{lem:120-separation} Soient $R$ un anneau sans diviseur de zéro, $X$ un ensemble, $(f_\alpha)_{\alpha \in A}$ et $(g_\beta)_{\beta \in B}$ des familles quelconques de fonctions $X \to R$. La famille formée des $f_\alpha$ et des $f_\alpha g_\beta$ a pour lieu des zéros communs celui des $f_\alpha$. Si $x$ n'est pas un zéro commun des $f_\alpha$ et si un $g_\beta$ sépare $x$ et $y$, cette famille sépare $x$ et $y$. \end{lemme} \begin{proof} Un zéro commun des $f_\alpha$ annule les $f_\alpha g_\beta$. Pour la séparation, si un $f_\alpha$ sépare $x$ et $y$, c'est fini. Sinon $f_\alpha(x) = f_\alpha(y)$ pour tout $\alpha$ ; on choisit $\alpha$ avec $\lambda = f_\alpha(x) \neq 0$ et $\beta$ avec $g_\beta(x) \neq g_\beta(y)$. Alors $f_\alpha g_\beta(x) - f_\alpha g_\beta(y) = \lambda\,(g_\beta(x) - g_\beta(y))$ n'est pas nul, puisque $R$ n'a pas de diviseur de zéro. \end{proof} \begin{theoreme}[Pages 22 et 23, écrasement sur un corps, forme corrigée par l'édition\piste{120-collapse-separation-over-a-field}]\label{thm:120-ecrasement} Supposons (M$'$1) à (M$'$4) et (M11), $R$ étant un corps. Soient $X \in \mathcal M_I$, des fonctions modérées $f_\alpha$ sur $X$ en nombre fini, des $e_\alpha \in R_0$, $Y = \bigcap_\alpha f_\alpha^{-1}(e_\alpha)$, et des fonctions modérées $g_\beta$ qui plongent $X$. Les fonctions $f_\alpha - e_\alpha$ et $(f_\alpha - e_\alpha)\,g_\beta$ sont modérées, ont $Y$ pour lieu des zéros communs, et séparent les points de $X \smallsetminus Y$. En particulier $Y$ est le lieu des zéros communs d'une famille finie de fonctions modérées qui sépare les points de $X \smallsetminus Y$ : la seconde moitié de (M6) découle de la première, et $X/Y$ est un espace modéré au sens strict. \end{theoreme} \begin{proof} Par le lemme~\ref{lem:120-anneau}, la constante $e_\alpha$ est modérée parce que $e_\alpha \in R_0$, donc $f_\alpha - e_\alpha$ aussi, et les produits $(f_\alpha - e_\alpha)\,g_\beta$ le sont. Les zéros communs des $f_\alpha - e_\alpha$ forment $Y$. Pour $x \neq y$ dans $X \smallsetminus Y$, un $f_\alpha - e_\alpha$ ne s'annule pas en $x$, et comme les $g_\beta$ plongent $X$, l'un d'eux sépare $x$ et $y$ : le lemme~\ref{lem:120-separation} conclut. Pour l'énoncé d'existence, les coordonnées, modérées par le lemme~\ref{lem:120-anneau}, plongent $X$, et la famille est indexée par $A \sqcup (A \times I)$, qui est fini. \end{proof} \begin{remarque} L'énoncé tient tel que la lecture le donne, et plus généralement. Ni (M$'$3), ni (M5) à (M7), ni les parties a) et c) de (M11), ni la finitude des familles ne servent ; de (M11), seule sert la partie b), sur un anneau commutatif sans diviseur de zéro. L'hypothèse d'intégrité ne peut être omise : sur $\mathbf Z/4\mathbf Z$, avec $f = 2$ et $g = \mathrm{id}$, la famille $2,\ 2x$ ne sépare pas $0$ et $2$, bien que $f(0) \neq 0$ et $g(0) \neq g(2)$. Les deux corrections de la lecture sont nécessaires. Sans $e_\alpha \in R_0$, la constante $e_\alpha$ n'est pas modérée et la translation n'est pas permise. Et une famille qui s'annule sur $Y$ ne sépare aucun couple de points de $Y$ : \q{sépare les points de $X$} ne peut s'entendre que de $X \smallsetminus Y$. \end{remarque} \noindent\emph{Sommes amalgamées (pages 8 à 13).} On ajoute (M5$'$), $\emptyset \in \mathcal M_I$ et la stabilité par réunion de deux parties (page~9) ; (M6), toute partie modérée $Z$ d'un $X \in \mathcal M_I$ est la fibre $F^{-1}(e)$, $e \in R_0^A$, d'une famille modérée finie $F$ injective hors de $Z$ ; (M7), une fonction modérée sur $Z$ se prolonge en une fonction modérée sur $X$ (page~12). Un espace est un $X \in \mathcal M_I$, une application modérée une famille à graphe modéré. \begin{theoreme}[D'après les pages 10 à 13, conclusion restituée par la lecture\piste{120-axiomatic-pushouts-along-embeddings}] Supposons $R$ non vide et (M5$'$). Soient $i_1 : Z \hookrightarrow X_1$ et $i_2 : Z \hookrightarrow X_2$ deux plongements modérés. \begin{enumerate} \item (Critère de la page~10, suffisance.) Si des familles modérées $J_1 : X_1 \to R^N$, $J_2 : X_2 \to R^N$ sont injectives, vérifient $J_1 i_1 = J_2 i_2$ sur $Z$ et $J_1(x_1) \neq J_2(x_2)$ hors de $i_1(Z)$ et de $i_2(Z)$, alors $J_1(X_1) \cup J_2(X_2)$ est modérée, c'est la somme amalgamée ensembliste ($J_1 x_1 = J_2 x_2$ si et seulement si $x_1 = i_1 z$ et $x_2 = i_2 z$), et toute paire d'applications modérées $f_1$, $f_2$ compatibles sur $Z$ se factorise par une application modérée. \item (Proposition de la page~12.) Sous (M6) et (M7), de telles familles existent : la somme amalgamée existe et l'oubli la respecte. \item (Critère de la page~10, nécessité.) Inversement, si une partie modérée $P \subset R^N$ et des familles modérées $q_1 : X_1 \to P$, $q_2 : X_2 \to P$ forment une somme amalgamée dans les ensembles ($q_1 i_1 = q_2 i_2$ sur $Z$, $P = q_1(X_1) \cup q_2(X_2)$, et toute paire d'applications vers un ensemble non vide compatibles sur $Z$ se factorise par $P$), les coordonnées de $q_1$ et $q_2$ sont des fonctions modérées vérifiant a), b), c). Les conditions a), b), c) équivalent donc à l'existence d'une somme amalgamée modérée que l'oubli respecte. \end{enumerate} \end{theoreme} \noindent L'énoncé tient (\href{\leanblob/Folder120.lean}{\texttt{pushout\_of\_criterion}}, \href{\leanblob/Folder120.lean}{\texttt{pushout\_exists}}), y compris la conclusion restituée à la page~13 : les deux images se rencontrent exactement le long de $Z$. La nécessité tient aussi (\href{\leanblob/Folder120.lean}{\texttt{criterion\_of\_pushout}}, \href{\leanblob/Folder120.lean}{\texttt{criterion\_iff}}) : le plongement $F$ de la lecture est l'inclusion $P \subset R^N$, et $f = q_1$, $g = q_2$. Pour b), on factorise par $P$ le couple à valeurs dans les propositions $u_1(y) = (y = x)$, $u_2(y) = (\exists z \in Z,\ y = i_2 z \text{ et } i_1 z = x)$, compatible sur $Z$ parce que $i_2$ est injectif : $q_1 x = q_1 x'$ force $x' = x$. Pour c), le couple $u_1 = \mathrm{vrai}$, $u_2(y) = (y \in i_2(Z))$ montre que $q_1 x_1 = q_2 x_2$ force $x_2 \in i_2(Z)$, ce qui est plus fort que c). Ni (M5$'$), ni (M6), ni (M7), ni le caractère modéré de $P$ ne servent à cette direction ; l'injectivité de $i_1$ et $i_2$ y sert. \[ \begin{tikzcd}[column sep=large] Z \arrow[r, hook, "i_2"] \arrow[d, hook, "i_1"'] & X_2 \arrow[d, "J_2"] \arrow[ddr, bend left=25, "f_2"] & \\ X_1 \arrow[r, "J_1"'] \arrow[drr, bend right=20, "f_1"'] & J_1(X_1) \cup J_2(X_2) \subset R^N \arrow[dr, dashed] & \\ & & R^L \end{tikzcd} \] C'est le point~1 : si $f_1 i_1 = f_2 i_2$, il existe une application modérée, en tirets, dont les composés avec $J_1$ et $J_2$ sont $f_1$ et $f_2$ ; elle est unique, les deux images recouvrant la réunion. \begin{remarque} La propriété universelle demande $R$ non vide, puisqu'il faut une application vers $R^L$ ; ce sont les cas triviaux que la page~4 exclut. (M5$'$) ne sert qu'à la réunion $J_1(X_1) \cup J_2(X_2)$ et au graphe de l'application induite. (M6) sert avec sa seconde moitié, l'injectivité hors de $Z$, que la lecture ne déduit de la première que sur un corps. \end{remarque} Ne sont pas démontrés ici : la catégorie $\Sigma$ des espaces modérés et ses limites finies (pages~5 à~7), le NB de la page~10 pour les diagrammes finis, les ind-espaces et la topologie des pages~14 à~19, et le programme de trivialité de la page~24. \section[Cote 150 : voisinages coniques, un contre-exemple sur {[0, 1]}]{Cote 150 : voisinages coniques, un contre-exemple sur $[0, 1]$\protect\verifie{Folder150}}\label{sec:150} La cote 150, \emph{Espaces stratifiés et voisinages côniques (ou : déploiement des espaces stratifiés)}, quatre-vingt-dix-huit pages de décembre 1981 et janvier 1982, cherche à déplier un espace stratifié : remplacer chaque strate par une version rognée, sans jointure, et garder la trace de la façon dont les morceaux se recollaient. Les pages~11 à~19 en posent le vocabulaire. Un \emph{voisinage conique} d'un fermé $Y$ dans un espace $X$ est un voisinage $T$ de $Y$ muni d'une action $(\lambda, t) \mapsto \lambda t$ du monoïde multiplicatif $\mathbf I = [0, 1]$, qui fixe $Y$ et écrase $T$ sur $Y$ pour $\lambda = 0$. Son bord $\dot T$ est la base du cône, et $f : \dot T \to Y$, $t \mapsto 0 \cdot t$, envoie chaque point du bord sur la pointe de son segment. Ôter l'intérieur de $T$ laisse un espace à bord $X^\sharp = X \smallsetminus \mathring T$, que la page note $X^{*}$, dont le bord est $\dot T$. La page~19 énonce une proposition de reconstruction (\lot{150}{1}{19}). Les systèmes $(X, Y, (X_i)_{i \in I}, T)$, où les $X_i$ sont des fermés et $T$ un voisinage conique de $Y$ compatible avec eux, seraient équivalents, en ne gardant pour morphismes que les isomorphismes, aux systèmes $(X^\sharp, \dot X, (X_i^\sharp), Y, f : \dot X \to Y)$, où $\dot X = \dot T$ et $X_i^\sharp = X_i \cap X^\sharp$. Dans l'autre sens, on recolle à $X^\sharp$, le long de $\dot X$, le cylindre de l'application $f$. Intuitivement, couper le voisinage conique ne perd rien, puisque le cône se reconstruit à partir de sa base et de la projection sur la pointe. \noindent\emph{Les définitions.} Une partie $T' \subset T$ est \emph{conique} quand elle est formée des segments issus de sa trace sur le bord et de sa trace sur $Y$ : $T' = \mathbf I \cdot (T' \cap \dot T) \cup (T' \cap Y)$. C'est la remarque de la page~15 (\lot{150}{1}{15}) ; elle contient la stabilité par l'action. Le voisinage $T$ est \emph{compatible} avec un fermé $X'$ si $X' \cap T$ est conique. Un \emph{collier} de $\dot T$ dans $X^\sharp$ est un voisinage $E$ de $\dot T$ identifié à $\dot T \times [0, 1]$, et $X'$ lui est compatible si $X' \cap E$ s'écrit $X'_0 \times [0, 1]$. La partie conique $T'$ est \emph{stricte} si sa trace sur $Y$ se réduit aux pointes de ses segments, $T' \cap Y = 0 \cdot (T' \cap \dot T)$ : c'est la condition que la page~16 ajoute au bas du feuillet et entoure (\lot{150}{1}{16}). \noindent\emph{Pourquoi la proposition demande une condition.} Les données de droite ne voient de $X_i$ que sa partie hors de l'intérieur de $T$. Dans $T$, la compatibilité reconstruit les segments à partir de leur base $X_i \cap \dot T$, mais elle laisse libre un morceau de $Y$ que $X_i$ peut contenir sans qu'aucun segment n'y aboutisse. Ce morceau est invisible à droite. L'exemple le plus petit est sur un segment. \noindent\emph{L'exemple.} On prend $X = [0, 1]$, $Y = \{0\}$ et $T = [0, \frac12]$, avec l'action $(\lambda, t) \mapsto \lambda t$. Le bord est $\dot T = \{\frac12\}$, l'application $f$ envoie $\frac12$ sur $0$, et $X^\sharp = [\frac12, 1]$. Le collier est $E = [\frac12, \frac34]$, identifié à $\dot T \times [0, 1]$ par $(\frac12, s) \mapsto \frac12 + \frac s4$. Le voisinage $T$ est strict, au sens de la page~14 : c'est $\frac12 \cdot X$, et $X$ est lui-même un voisinage conique de $Y$ pour la même action (figure~\ref{fig:150-segment}). \begin{figure}[htbp] \centering \begin{tikzpicture}[x=9.5cm, y=1cm, >=stealth, every node/.style={font=\small}] % X = [0, 1] et ses morceaux \fill[black!10] (0.5,-0.09) rectangle (0.75,0.09); \draw[thick] (0,0) -- (1,0); \foreach \x/\l in {0/0, 0.5/\tfrac12, 0.75/\tfrac34, 1/1} { \draw (\x,-0.1) -- (\x,0.1); \node[below=2pt] at (\x,-0.1) {$\l$}; } \fill[piste] (0,0) circle (2pt); \node[piste, left=4pt] at (0,0) {$Y = \{0\}$}; \fill (0.5,0) circle (2pt); \node[above] at (0.5,0.1) {$\dot T = \{\frac12\}$}; \node[black!65] at (0.625,-0.36) {\footnotesize collier $E$}; \draw[decorate, decoration={brace, amplitude=5pt}] (0.005,0.75) -- node[above=5pt] {$T = [0, \frac12]$} (0.495,0.75); \draw[->, black!65] (0.41,0.35) -- node[above] {\footnotesize $t \mapsto \lambda t$} (0.06,0.35); \draw[decorate, decoration={brace, amplitude=5pt, mirror}] (0.5,-0.72) -- node[below=5pt] {$X^\sharp = [\frac12, 1]$, de bord $\dot T$} (1,-0.72); % les deux fermés \foreach \y/\l/\p in {-2.1/{$X_1 = \{0\}$}/1, -2.9/{$X_1 = \emptyset$}/0} { \draw[black!30] (0,\y) -- (1,\y); \draw[black!30, line width=3pt] (0.5,\y) -- (1,\y); \node[anchor=east] at (-0.03,\y) {\l}; \ifnum\p=1 \fill[piste] (0,\y) circle (2pt); \fi \node[black!65, anchor=west] at (1.02,\y) {\footnotesize trace vide}; } \end{tikzpicture} \caption{L'exemple de la page~19 sur $X = [0, 1]$. Le voisinage conique $T$ de $Y$ est écrasé sur $0$ par l'action $t \mapsto \lambda t$, son bord est le point $\frac12$, et $X^\sharp$ est ce qui reste quand on ôte l'intérieur de $T$. Les deux fermés du bas sont compatibles avec $T$ et avec le collier, et leur trace sur $X^\sharp$, en gris épais, est vide dans les deux cas : les données de droite ne les distinguent pas. Le point $0$ du premier n'est la pointe d'aucun segment issu du bord, puisque $\dot X_1$ est vide ; c'est la condition $X_1 \cap Y = f(\dot X_1)$ qui l'exclut.} \label{fig:150-segment} \end{figure} \begin{encadre} \begin{contrexemple}[contre-exemple de l'édition, page~19] Dans l'exemple ci-dessus, les fermés $X_1 = \{0\}$ et $X_1 = \emptyset$ de $[0, 1]$ sont tous deux compatibles avec $T$ et avec le collier $E$, et ils ont la même trace, vide, sur $X^\sharp$. Les deux systèmes ont donc les mêmes données de droite, mais ils ne sont pas isomorphes, puisque l'un des fermés est vide et l'autre non. Le fermé $\{0\}$ ne vérifie pas la condition $X_1 \cap Y = f(\dot X_1)$, où $\dot X_1 = X_1 \cap \dot T$. \end{contrexemple} \end{encadre} \begin{proof} Pour $X_1 = \{0\}$ : $X_1 \cap T = \{0\}$, sa trace sur le bord est vide et sa trace sur $Y$ est $\{0\}$, de sorte que $\mathbf I \cdot \emptyset \cup \{0\} = \{0\}$ : la partie est conique. Elle ne rencontre pas $E$, et $X_1 \cap E = \emptyset = \emptyset \times [0, 1]$. Pour $X_1 = \emptyset$, tout est vide. Les deux traces sur $X^\sharp = [\frac12, 1]$ sont vides. Enfin $\{0\} \cap Y = \{0\}$, alors que $\dot X_1 = \emptyset$ et $f(\emptyset) = \emptyset$. \end{proof} Le contre-exemple tient encore si l'on demande que $T$ soit strict, comme le faisait la première définition de \q{strictement compatible} de la lecture, et si l'on ajoute le collier : ni l'une ni l'autre condition ne regarde la trace de $X_1$ sur $Y$. La lecture a donc mis dans la définition la condition $X_i \cap Y = f(\dot X_i)$, que la page impose elle-même au bas de la page~16. Sous cette condition, l'exemple ne présente plus d'ambiguïté. \begin{encadre} \begin{enonce}[énoncé de l'édition, page~19, dans l'exemple] Dans l'exemple ci-dessus, soient $X_1$ et $X_2$ deux fermés de $[0, 1]$ compatibles avec $T$ et avec le collier, qui vérifient $X_k \cap Y = f(\dot X_k)$. Si $X_1 \cap X^\sharp = X_2 \cap X^\sharp$, alors $X_1 = X_2$. \end{enonce} \end{encadre} \begin{proof} Une partie conique $C$ de $T$ est $T$ tout entier si elle contient $\frac12$, puisqu'elle contient alors le segment $\mathbf I \cdot \frac12 = [0, \frac12]$ ; sinon sa trace sur le bord est vide et $C = C \cap Y \subset \{0\}$. Sous la condition stricte, le second cas donne $C \cap Y = f(\emptyset) = \emptyset$, donc $C = \emptyset$. Ainsi $X_k \cap T$ vaut $T$ ou $\emptyset$ selon que $\frac12$ est dans $X_k$ ou non. Or $\frac12$ appartient à $X^\sharp$, et l'on lit sur la trace $X_k \cap X^\sharp$ s'il est dans $X_k$. Comme $[0, 1] = T \cup X^\sharp$, on a $X_k = (X_k \cap T) \cup (X_k \cap X^\sharp)$, et les deux morceaux sont déterminés par la trace sur $X^\sharp$. \end{proof} \begin{remarque} Le collier ne sert pas à la démonstration de l'énoncé : dans l'exemple, la condition stricte suffit. La page laisse deux réparations possibles : demander la condition stricte, ou ajouter les traces $X_i \cap Y$ aux données de droite. La lecture a retenu la première, et l'exemple montre qu'elle répare le défaut qu'il met en évidence ; il ne démontre pas la proposition corrigée en général. \end{remarque} \noindent\emph{Portée de la vérification.} Lean traite l'exemple seul, dans $\mathbb R$ : les parties $X$, $Y$, $T$, $\dot T$, $X^\sharp$ et le collier y sont des intervalles explicites, et les notions de partie conique, de compatibilité, de compatibilité au collier et de compatibilité stricte y sont écrites pour cette action. Il démontre que $T$ est conique et strict (\texttt{isConic\_T}, \texttt{T\_eq\_half\_smul}), le contre-exemple (\texttt{compatible\_not\_determined}, \texttt{not\_strictlyCompatible\_singleton\_zero}) et l'énoncé (\texttt{eq\_of\_strictlyCompatible}). Ne sont pas formalisés : les deux catégories de la proposition et le foncteur de recollement $X = X^\sharp \amalg_{\dot X} \mathcal C(f)$ pour des espaces quelconques, la transversalité et l'équisingularité de la même page. Mathlib n'a pas les espaces stratifiés ni les voisinages coniques. Ne sont pas démontrés ici, de la même cote : \begin{encadre} \begin{theoreme*}[Grothendieck, pages 1 et 45 à 47, lissité des fibrations de drapeaux\piste{150-flag-fibration-smoothness}]\nonverifie Dans le déploiement d'une stratification équisingulière non singulière, présenté comme foncteur sur les drapeaux de $I$, soit $d = (i_1, \dots, i_p)$ un segment initial de $d' = (i_1, \dots, i_n)$. Le bord des fibres de $\Sigma_{d'} \to \Sigma_d$ est stratifié cylindriquement par les drapeaux non vides de la somme ordinale $I_{]i_p,i_{p+1}[} \sqcup \dots \sqcup I_{]i_{n-1},i_n[}$. La fibration est donc à fibres sans bord exactement quand $i_{k+1}$ couvre $i_k$ dans $I$ pour $p \leq k < n$, condition où $i_1, \dots, i_{p-1}$ n'interviennent pas. \end{theoreme*} \end{encadre} {\small Le mot qui qualifie \q{successeur} à la page~47 est une addition incertaine ; le critère est fixé par la page~46, lisible. Mathlib n'a pas les stratifications équisingulières ni leurs déploiements. On se reportera aux notes de Grothendieck (\lot{150}{1}{1}).\par} \noindent\emph{Le critère combinatoire, vérifié.} Le théorème reste non démontré, mais sa partie purement ordinale est vérifiée par Lean (\texttt{Folder150.Flags}). Soit $I$ un ensemble ordonné quelconque, $d' = (i_1 < \dots < i_n)$ un drapeau, $m = i_p$ l'un de ses termes et $d = (i_1, \dots, i_p)$ le segment initial qu'il détermine. On note $J$ la réunion des intervalles ouverts $]i_k, i_{k+1}[$, $p \leq k < n$, et l'on appelle \emph{drapeaux au-dessus de $d'$} les drapeaux $e \supset d'$ qui ont les mêmes termes que $d'$ jusqu'à $i_p$ et le même dernier terme $i_n$ : ce sont les indices des strates $\Sigma_e$ du bord des fibres. \begin{encadre} \begin{enonce}[énoncé de l'édition, pages~45 à~47, partie combinatoire] \begin{enumerate} \item[(i)] $J$ est la somme ordinale des $I_{]i_k, i_{k+1}[}$ : un point d'un intervalle est en dessous de tout point d'un intervalle plus haut. C'est l'ensemble des points hors de $d'$, strictement compris entre $i_p$ et $i_n$ et comparables à tous les termes de $d'$. \item[(ii)] $e \mapsto e \smallsetminus d'$ est un isomorphisme d'ensembles ordonnés (par inclusion) des drapeaux au-dessus de $d'$ sur les drapeaux de $J$, qui envoie $d'$ sur le drapeau vide. \item[(iii)] Les conditions suivantes sont équivalentes : $J$ est vide ; $J$ n'a aucun drapeau non vide ; $d'$ est le seul drapeau au-dessus de lui-même ; $i_{k+1}$ couvre $i_k$ dans $I$ pour $p \leq k < n$. Les termes $i_1, \dots, i_{p-1}$ n'interviennent pas. \end{enumerate} \end{enonce} \end{encadre} \begin{proof} (i) Si $x \in \,]i_k, i_{k+1}[$ et $y \in \,]i_l, i_{l+1}[$ avec $k < l$, on a $i_{k+1} \leq i_l$, sans quoi $i_l$ serait un terme de $d'$ strictement entre $i_k$ et $i_{k+1}$ ; donc $x < i_{k+1} \leq i_l < y$. Un point de $]i_k, i_{k+1}[$ n'est pas un terme, puisque les termes sont consécutifs, et il est comparable à tous les termes, qui sont soit $\leq i_k$, soit $\geq i_{k+1}$. Réciproquement, si $x \notin d'$ est comparable à tous les termes et $i_p < x < i_n$, soit $a$ le plus grand terme $< x$ et $b$ le plus petit terme $> x$ ; ils sont consécutifs, et $a \geq i_p$. (ii) Soit $e$ au-dessus de $d'$ et $x \in e \smallsetminus d'$. Comme $e$ est une chaîne qui contient $d'$, $x$ est comparable à tous les termes ; il n'est pas $\leq i_p$, puisque $e$ et $d'$ ont les mêmes termes jusqu'à $i_p$, ni égal à $i_n$, et il est $\leq i_n$ : par (i), $x \in J$. Inversement, si $c$ est un drapeau de $J$, $c \cup d'$ est une chaîne, puisque les points de $J$ sont comparables aux termes, et elle est au-dessus de $d'$ par (i). Les deux applications sont inverses l'une de l'autre parce que $J$ ne rencontre pas $d'$, et elles respectent l'inclusion. (iii) $J$ est vide si et seulement si chaque $]i_k, i_{k+1}[$, $k \geq p$, l'est, c'est-à-dire si $i_{k+1}$ couvre $i_k$ ; un point de $J$ est un drapeau non vide ; et par (ii) les drapeaux au-dessus de $d'$ autres que $d'$ correspondent aux drapeaux non vides de $J$. \end{proof} {\small\noindent\emph{Portée de la vérification.} Lean vérifie (i) à (iii) pour un ensemble ordonné quelconque, les drapeaux étant des chaînes finies (\texttt{lt\_of\_mem\_Ioo}, \texttt{mem\_gaps\_iff}, \texttt{aboveEquiv}, \texttt{aboveEquiv\_eq\_empty}, \texttt{aboveEquiv\_subset}, \texttt{gaps\_eq\_empty\_iff}, \texttt{flags\_gaps\_iff}, \texttt{above\_eq\_iff}). Ne sont pas formalisés : le déploiement, les variétés à bord $\Sigma_d$, les fibrations $\Sigma_{d'} \to \Sigma_d$, la stratification cylindrique de leur bord et l'identification de ses strates aux $\Sigma_e$, c'est-à-dire tout ce qui fait passer du critère ordinal à la lissité. C'est pourquoi l'encadré ci-dessus reste non vérifié.\par} \begin{encadre} \begin{theoreme*}[Grothendieck, pages 47 à 66 et 70, le déploiement comme espace ordonné\piste{150-unfolding-as-ordered-space}]\nonverifie Les données déployées d'une stratification équisingulière indexée par un ensemble ordonné fini $I$ (strates déployées $\Sigma_i$, tubes de raccord $\Sigma_{ij}$ fibrés sur $\Sigma_i$ et plongés de façon fermée, avec collier, dans $\Sigma_j$) équivalent à un seul espace topologique ordonné $\Sigma$, dont le graphe de l'ordre est la réunion des tubes. Cet espace est soumis à des conditions de propreté, de transversalité et de finitude, chaque $\Sigma_{