\section[Cote 29 : le critère du déterminant sur l'inertie modérée]{Cote 29 : le critère du déterminant sur l'inertie modérée\protect\verifie{Folder29}}\label{sec:29}

La cote 29 réunit, entre 1959 et 1969, les notes de Grothendieck sur le groupe fondamental modéré, dont l'échange de 1967 avec Murre. Le tapuscrit \q{Comportement fonctoriel des groupes d'inertie} (pages~116 à 122) calcule, pour un morphisme $f$ de schémas strictement locaux réguliers munis de diviseurs à croisements normaux de branches indexées par $C$ et $C'$, l'application induite sur l'inertie modérée : c'est l'application $N : \prod_{\ell \neq p} \mathbf Z_\ell(1)^C \to \prod_{\ell \neq p} \mathbf Z_\ell(1)^{C'}$ de la matrice $(n_{c,c'})$ des multiplicités, $f^*(\bar E_{c'}) = \sum_c n_{c,c'} \bar D_c$ (\lot{29}{6}{120}). L'identification de cette application à $N$ demande l'inertie modérée des schémas réguliers, que mathlib n'a pas ; elle n'est pas démontrée ici. Le critère que la page en tire porte sur la seule matrice, $\mathbf Z_\ell(1)$ étant libre de rang~$1$ sur $\mathbf Z_\ell$.

\noindent\emph{Ramification modérée.} Le cadre est celui de SGA~1, exposé~XIII, et de son appendice~I : pour $X$ strictement local régulier et $D$ à croisements normaux de branches indexées par $C$, le groupe fondamental modéré de $X \smallsetminus D$ est $\prod_{\ell \neq p} \mathbf Z_\ell(1)^C$ (corollaire~5.3 de l'appendice, dans l'édition de 2003 \cite{sga1}), et l'on cherche ici sa fonctorialité. Le groupe fondamental modéré d'un voisinage formel d'un diviseur à croisements normaux, objet des pages~87 à~97 et de l'échange avec Murre, est aussi le sujet du livre de Grothendieck et Murre (1971) \cite{grothendieckmurre1971}. Les pages~190 à~200 cherchent un cadre axiomatique, les \q{domaines de ramification}, et réalisent les revêtements modérés comme revêtements étales d'un champ (ci-dessous). La monodromie modérée à plusieurs paramètres de la cote~34 et la dimension cohomologique de la cote~31, de la même période, sont encadrées dans les parties \q{Groupes fondamentaux et théorie de Galois} et \q{Cohomologie étale et $\ell$-adique}.

\begin{theoreme}[Grothendieck, page 120, le critère\piste{29-inertia-matrix-determinant}]\label{thm:29-critere}
Soient $C$, $C'$ des ensembles finis, $N$ une matrice entière de lignes indexées par $C'$ et de colonnes par $C$, et $p$ un nombre premier ou $p = 1$ (l'exposant caractéristique). L'application $\mathbf Z_\ell^C \to \mathbf Z_\ell^{C'}$ de matrice $N$ est bijective pour tout nombre premier $\ell \neq p$ si et seulement si $\operatorname{card} C = \operatorname{card} C'$ et, les colonnes étant mises en bijection avec les lignes, l'entier $\det N$ vaut $\pm p^k$ pour un $k \geq 0$.
\end{theoreme}

\noindent L'énoncé tient tel que la page le donne, par l'argument d'une ligne de la lecture (\texttt{criterion}, dans \href{\leanblob/Folder29.lean}{\texttt{Folder29.\allowbreak{}lean}}). L'égalité des cardinaux vient d'une seule valeur de $\ell$ ; le choix de la bijection entre colonnes et lignes ne change le déterminant que d'un signe.

\noindent La preuve vérifiée établit aussi les deux pas : la bijectivité pour un $\ell$ donné force $\operatorname{card} C = \operatorname{card} C'$ (\texttt{card\_eq\_of\_bijective}), et une matrice carrée entière est bijective sur $\mathbf Z_\ell$ si et seulement si $\ell \nmid \det$ (\texttt{bijective\_iff\_not\_dvd\_det}). Elle ne définit ni l'inertie modérée ni $\mathbf Z_\ell(1)$ : le passage de la géométrie à la matrice est l'énoncé encadré ci-dessous, non vérifié.

\begin{encadre}
\begin{theoreme*}[Grothendieck, page 120, inertie modérée et matrice des multiplicités]\nonverifie
Dans la situation ci-dessus, l'application induite sur l'inertie modérée est l'application $N$ de matrice $(n_{c,c'})$ ; lorsque $N$ est un isomorphisme, les sous-groupes d'inertie de $H$ en $y$ sont exactement les conjugués des images de ceux de $G$ en $x$.
\end{theoreme*}
\end{encadre}
{\small Mathlib n'a pas l'inertie modérée des schémas réguliers. On se reportera aux notes de Grothendieck (\lot{29}{6}{120}).\par}

\noindent\emph{Le degré comme donnée primitive (pages~212 et~214).} Deux feuillets insérés, \q{1 bis} et \q{1 ter}, axiomatisent directement la notion de morphisme de degré~$n$, sans foncteur fibre ni points à compter (\lot{29}{11}{212}). Sur une catégorie $C$, on se donne pour chaque $n \in \mathbf N$ une classe $\mathrm{deg}_n$ de morphismes telle que : a) elle est stable par changement de base ; b) elle est additive pour les sommes finies ($\varnothing \to Y$ est de degré~$0$, et si $X = X_1 \sqcup X_2$ avec $X_i \to Y$ de degré $n_i$, alors $X \to Y$ est de degré $n_1 + n_2$) ; c) un isomorphisme est de degré~$1$ ; d$'$) pour tout $f : X \to Y$, $Y = \coprod_{n \in \mathbf N} Y_n$ avec $X \times_Y Y_n \to Y_n$ de degré~$n$ ; d) un morphisme de degré $n \geq 1$ est de descente effective universelle ; e) un morphisme de degré~$0$ a une source vide et est l'inclusion d'un sommande direct. La \q{Conclusion} de la page~214 affirme que, sous ces conditions et les conditions (0) à (2) de la page~212 (limites projectives finies, monomorphismes inclusions de sommandes directs), la notion est uniquement déterminée, et qu'un morphisme est de degré~$n$ si et seulement s'il devient $[1, n]$, la somme de $n$ copies de la base, après un changement de base de descente effective universelle.

Dans la vérification, la classe des morphismes trivialisants est un paramètre $E$, puisque mathlib n'a pas les morphismes de descente effective universelle ; on n'en utilise que les propriétés que la page utilise. On note $\mathrm{Triv}_n(E)$ la classe des $f : X \to Y$ pour lesquels il existe $g : Y' \to Y$ dans $E$ avec $X \times_Y Y' \simeq [1, n]_{Y'}$ au-dessus de $Y'$.

\begin{contrexemple}[Grothendieck, page 214, la Conclusion telle qu'elle est écrite\piste{29-degree-n-as-primitive}]
Les conditions a) à e) ne déterminent pas la notion de degré. Si $\mathrm{deg}$ les vérifie, la classe $\mathrm{deg}^{\leq}$, où $\mathrm{deg}^{\leq}_0 = \mathrm{deg}_0$ et où $f$ est de degré~$n \geq 1$ s'il est de degré~$k$ pour un $1 \leq k \leq n$, les vérifie aussi. Dans la catégorie des ensembles finis, avec pour $E$ les surjections, le degré usuel (toutes les fibres ont $n$ éléments) et son $\mathrm{deg}^{\leq}$ sont deux notions distinctes : l'identité d'un point y est de degré~$1$ et~$2$.
\end{contrexemple}

\begin{proof}
Pour $\mathrm{deg}^{\leq}$, a), c), d$'$) et e) se lisent sur $\mathrm{deg}$, d) vient de ce qu'un degré $k \geq 1$ est encore $\geq 1$, et b) de ce que $1 \leq k_1 \leq n_1$ et $1 \leq k_2 \leq n_2$ donnent $k_1 + k_2 \leq n_1 + n_2$. Dans les ensembles finis, le degré usuel vérifie a) à e) : les fibres se conservent par changement de base et s'additionnent sur une somme, $Y_n$ est l'ensemble des points dont la fibre a $n$ éléments, une fibre non vide donne la surjectivité. L'identité d'un point n'y est pas de degré~$2$.
\end{proof}

Le pas de la page~214 qui cède est \q{donc par additivité, $X'_1 \to Y'$ est de degré $n - 1$} : de $X' = Y' \sqcup X'_1$ de degré~$n$ et $Y' \to Y'$ de degré~$1$, la condition b) ne permet pas de soustraire. C'est une simplification, et elle suppose qu'un morphisme n'a qu'un degré. On ajoute donc la condition

\smallskip
\noindent (u) si $f : X \to Y$ est à la fois de degré~$m$ et de degré~$n$, avec $m \neq n$, alors $Y$ est vide (initial),
\smallskip

\noindent que le degré usuel des ensembles finis vérifie, et que $\mathrm{deg}^{\leq}$ ne vérifie pas.

\begin{theoreme}[d'après les pages 212 et 214, avec la condition (u)\piste{29-degree-n-as-primitive}]
Soit $C$ une catégorie à produits fibrés, finitairement extensive (sommes finies disjointes et universelles), dans laquelle tout monomorphisme est l'inclusion d'un sommande direct. Soit $E$ une classe de morphismes contenant les identités, stable par composition, et dont tout changement de base d'un élément est un épimorphisme. Si $\mathrm{deg}$ vérifie a) à e) pour $E$ et la condition (u), alors pour tout~$n$, $\mathrm{deg}_n = \mathrm{Triv}_n(E)$. En particulier deux telles notions de degré coïncident.
\end{theoreme}

\begin{proof}
\emph{Sens direct}, par récurrence sur $n$, en suivant la page~214. Pour $n = 0$, $X$ est vide par e), et $g = \mathrm{id}_Y$ convient. Pour $n \geq 1$, $f$ est dans $E$ par d) ; on change de base par $f$ lui-même : $q : X' = X \times_Y X \to X$ est de degré~$n$ par a). La diagonale est un monomorphisme, donc $X' = X \sqcup X'_1$, la diagonale étant une section de $q$. \emph{Simplification} : on décompose $X = \coprod_j Z_j$ par d$'$) pour $r : X'_1 \to X$. Au-dessus de $Z_j$, la somme universelle donne $X' \times_X Z_j = Z_j \sqcup (X'_1 \times_X Z_j)$, de degré $1 + j$ par b) et c), et de degré~$n$ par a) ; par (u), $Z_j$ est vide pour $j \neq n - 1$, donc $Z_{n-1} = X$ et $r$ est de degré $n - 1$. La récurrence fournit $h : W \to X$ dans $E$ avec $X'_1 \times_X W \simeq [1, n-1]_W$ ; alors $h f$ est dans $E$, et $X \times_Y W = X' \times_X W = W \sqcup (X'_1 \times_X W) \simeq [1, n]_W$.

\emph{Réciproque}, que la page n'écrit pas. Soient $g : Y' \to Y$ dans $E$ et $X \times_Y Y' \simeq [1, n]_{Y'}$, qui est de degré~$n$ par b) et c). On décompose $Y = \coprod_k Y_k$ par d$'$) pour $f$, et l'on pose $R_k = Y' \times_Y Y_k$. Au-dessus de $R_k$, le changement de base de $f$ est de degré~$n$ (par $Y'$) et de degré~$k$ (par $Y_k$) ; par (u), $R_k$ est vide pour $k \neq n$. Alors $R_k \to Y_k$, changement de base de $g$, est un épimorphisme de source vide, et $Y_k$ est vide dans une catégorie extensive. Donc $Y = Y_n$ et $f$ est de degré~$n$.
\end{proof}

\noindent Lean : \href{\leanblob/Folder29.lean}{\texttt{DegreeAxioms}, \texttt{DegreeAxioms.\allowbreak{}atMost}, \texttt{atMost\_ne}, \texttt{Finite.\allowbreak{}degree\_not\_unique}} pour le contre-exemple ; \texttt{cancel} (la simplification), \texttt{deg\_imp\_triv} (la récurrence de la page~214), \texttt{triv\_imp\_deg} (la réciproque), \texttt{deg\_iff\_triv} et \texttt{unique} pour le théorème. Le contre-exemple reste vrai si l'on ajoute les conditions (0) à (2), que les ensembles finis vérifient (corollaire ci-dessous) ; la réciproque n'utilise de $E$ que l'universalité des épimorphismes, la récurrence que les identités et la composition. Ne sont pas formalisés : que les morphismes de descente effective universelle ont ces propriétés (leur stabilité par composition est un théorème de la théorie de la descente), et l'énoncé A(iii) qu'en tire la page pour les catégories multigaloisiennes.

\begin{corollaire}[les ensembles finis, d'après les pages 212 et 214\piste{29-degree-n-as-primitive}]
La catégorie des ensembles finis vérifie les conditions (0) à (2) de la page~212 : ses classes d'isomorphie forment un ensemble, elle a les limites projectives finies, et tout monomorphisme y est l'inclusion d'un sommande direct. Elle est finitairement extensive, et, $E$ étant la classe des surjections, tout changement de base d'un élément de $E$ est un épimorphisme. Par suite, une notion de degré qui vérifie a) à e) pour les surjections et la condition (u) est le degré usuel, et $f$ est de degré~$n$ si et seulement si un changement de base surjectif le rend isomorphe à $[1, n]$. La notion $\mathrm{deg}^{\leq}$ du contre-exemple vérifie a) à e) et (0) à (2), mais pas (u).
\end{corollaire}

\begin{proof}
(0) : la catégorie est équivalente à son squelette, indexé par $\mathbf N$. (1) : les limites finies se calculent dans les ensembles. (2) : un monomorphisme $m : A \to B$ est injectif, et $B$ est la somme de l'image de $m$ et de son complémentaire. L'extensivité se lit dans les ensembles, le foncteur d'oubli préservant les produits fibrés et les sommes binaires et reflétant les isomorphismes. Si $g : Y' \to Y$ est surjectif, son changement de base $B \times_Y Y' \to B$ est surjectif, donc épimorphe. Le théorème s'applique au degré usuel, qui vérifie (u), et à toute autre notion vérifiant (u), d'où l'unicité ; si $\mathrm{deg}^{\leq}$ vérifiait (u), il serait égal au degré usuel, ce que le contre-exemple exclut.
\end{proof}

\noindent Lean : \href{\leanblob/Folder29.lean}{\texttt{Finite.\allowbreak{}conditions}, \texttt{Finite.\allowbreak{}mono\_complement}, \texttt{Finite.\allowbreak{}surj\_pullback\_epi}, \texttt{Finite.\allowbreak{}deg\_iff\_triv}, \texttt{Finite.\allowbreak{}unique}, \texttt{Finite.\allowbreak{}not\_uniqueDegree\_atMost}}. Les surjections sont ici les morphismes de descente effective universelle des ensembles finis ; cette identification n'est pas formalisée.

Les autres pistes de la cote, hors de portée de Lean pour l'instant :

\begin{encadre}
\begin{theoreme*}[Grothendieck, pages 190 à 193, axiome R2 des domaines de ramification\piste{29-ramification-domain-axioms}]\nonverifie
Soit $(R, r)$ un domaine de ramification sur $S$ : un champ de catégories multigaloisiennes sur le site étale de $S$ muni d'une réalisation géométrique continue $r$ vers les schémas relatifs. Sous les axiomes R1, R3 et R4, l'axiome R2 (les sous-objets directs de $X$ correspondent bijectivement aux parties ouvertes et fermées de $r(X)$) équivaut à la fidélité de~$r$.
\end{theoreme*}
\end{encadre}
{\small La proposition est énoncée page~193, une page rayée. La page n'en argumente que le sens \q{$r$ fidèle $\Rightarrow$ R2}, en se ramenant à $X'' = X' \sqcup X_1$ et jusqu'à $r(X_1) = \emptyset$ ; la réciproque n'est démontrée ni sur la page ni ici. Les catégories multigaloisiennes sont les sommes finies de catégories galoisiennes au sens de SGA~1, exposé~V \cite{sga1} ; un domaine de ramification en fait un champ sur le site étale de $S$, et la réalisation $r$ joue le rôle du foncteur fibre.\par}

\begin{encadre}
\begin{enonce}[Grothendieck, page 197, proposition~6, homomorphismes de domaines de ramification, énoncée sans démonstration\piste{29-domram-morphisms-fully-faithful}]\nonverifie
Pour $(R, r)$ défini par un schéma $Z$ muni d'un groupe fini d'opérateurs $G$, $\mathrm{Hom}((R,r),(R',r'))$ est équivalente à la catégorie des couples $(P', \alpha)$, $P'$ objet galoisien de $R'_S$ de groupe $G$ et $\alpha$ un $G$-isomorphisme $r'(P') \simeq Z$. En particulier, dans tout homomorphisme $(\varphi, \lambda)$ de domaines de ramification, $\varphi$ est pleinement fidèle.
\end{enonce}
\end{encadre}


\begin{encadre}
\begin{theoreme*}[Grothendieck, pages 87 à 97, $\pi_1$ modéré et auto-intersection\piste{29-formal-tame-pi1-self-intersection}]\nonverifie
Soit $\mathfrak X$ un schéma formel régulier dont la fibre spéciale $X_o$ est une composante d'un diviseur à croisements normaux~$D$. Le groupe fondamental modéré $\pi_1^t(\mathfrak X/D)$ est une extension centrale de $\pi_1^t(X_o/D'_o)$ par un quotient de $\mu^\infty$, dont la classe est la classe de Chern de l'auto-intersection de $X_o$ dans $\mathfrak X$ ; pour $X_o = \mathbf P^1_k$ et $D'_o$ vide, l'extension est $\mu_n(k)$, où $n$ est la partie première à $p$ du degré de $X_o \cdot X_o$.
\end{theoreme*}
\end{encadre}
{\small Les feuillets en esquissent une démonstration incomplète : les lemmes~1 et~2 et l'argument de Kummer de la page~95 sont donnés, mais la page~91 porte \q{il faut prouver} et \q{à vérifier}, et la raison de la divisibilité, page~93, est omise. Le cas local, au-dessus d'un schéma strictement local, est le corollaire~5.3 cité plus haut ; l'énoncé global, avec la classe d'extension égale à la classe de Chern du fibré normal $\mathcal O_{X_o}(X_o)$, n'a été trouvé ni dans SGA~1 ni dans la description logarithmique de l'inertie. En termes de champs, on peut la rapprocher de la $\mu_n$-gerbe des racines $n$-ièmes du fibré normal (ci-dessous), dont la classe dans $H^2(X_o, \mu_n)$ est l'image de Kummer de la classe de ce fibré ; ce rapprochement est de l'édition.\par}

\noindent\emph{Gerbes de Kummer et champs des racines (pages~199 et~200).} Les revêtements modérés de $(S, D)$ y sont construits comme les revêtements étales finis du champ associé à la gerbe dont les objets au-dessus de $S'$ sont les familles d'équations $a_i$ des $D_i$ et les morphismes les familles $\xi$ d'unités telles que $b_i = a_i \xi_i^{n_i}$ ; l'obstruction à une section globale est la classe des $D_i$. C'est aujourd'hui le champ des racines $n_i$-ièmes le long des $D_i$ : Cadman (2007) \cite{cadman2007} définit, dans la numérotation de la version arXiv, le champ des racines $r$-ièmes d'un couple $(L, s)$ (définition~2.1), la racine $r$-ième de $X$ le long d'un diviseur de Cartier effectif $D$ (définition~2.3) et la $\mu_r$-gerbe au-dessus de $D$ que contient ce champ (définition~3.5). La correspondance entre revêtements modérés et revêtements étales de ce champ, que la page affirme, n'est pas démontrée ici.


\begin{encadre}
\begin{theoreme*}[Grothendieck, pages 170 et 171, torseurs sous un groupe discret infini\piste{29-h1-five-classes-infinite-group}]\nonverifie
Soit $G$ un groupe discret, éventuellement infini, et soient $C_1$ à $C_5$ les classes de familles couvrantes fppf quasi-compactes, de type fini, quasi-finies, principales finies et principales finies étales. On a $H^1_{C_3} \simeq H^1_{C_2}$ en général ; $H^1_{C_2} \simeq H^1_{C_1}$ sur un anneau de Dedekind ; $H^1_{C_i} \simeq H^1(\hat V/V, -)$ pour $i = 1, 2, 3$ sur un anneau de valuation discrète complet $V$ à corps résiduel algébriquement clos ; $H^1_{C_5} \simeq H^1_{C_4} \simeq H^1_{C_3}$ et $H^1_{C_i}(V, -) \simeq H^1_{C_i}(k, -)$ sur un anneau local complet $V$ de corps résiduel $k$.
\end{theoreme*}
\end{encadre}
{\small Mathlib n'a pas les torseurs fppf ni le $H^1$ pour ces topologies. On se reportera aux notes de Grothendieck (\lot{29}{9}{170}).\par}
\section[Cote 145 : l'exposant unité dans le groupe profini libre]{Cote 145 : l'exposant unité dans le groupe profini libre\protect\verifie{Folder145}}\label{sec:145}

La cote 145 étudie les automorphismes du groupe profini libre $\hat\pi$ sur $l_0$, $l_1$, avec $l_\infty l_1 l_0 = 1$, qui préservent les sous-groupes de lacets $L_0$, $L_1$, $L_\infty$ à des \q{rectificateurs} près. Les pages~34 et~35 caractérisent dans le cas discret, où l'exposant $p$ vaut $\pm 1$, les systèmes $(p, \sigma, 1, 1, 1)$ à rectificateurs triviaux : ce sont les six $(\operatorname{sg}\sigma, \sigma)$ du groupe $\Gamma_P$. La page conjecture (\q{Sans doute}) qu'il en va de même dans le cas profini, ramène la question à l'énoncé (14) ci-dessous et le laisse en \q{Exercice !} (\lot{145}{2}{34}). La lecture modernisée en donne une solution, qui est de l'édition, par un quotient diédral.

\noindent\emph{L'axe galoisien de ce texte.} Les cotes 142, 145, 146 et 149 étudient l'action de $\mathrm{Gal}(\overline{\mathbf Q}/\mathbf Q)$ sur le groupe fondamental profini de $\mathbf P^1 \smallsetminus \{0, 1, \infty\}$ et des espaces de modules $M_{g,\nu}$, que l'on décrit aujourd'hui par le groupe de Grothendieck--Teichmüller $\widehat{GT}$ (Drinfeld 1990, §~4 \cite{drinfeld1990} ; Ihara 1991 \cite{ihara1991}). Le groupe $\hat\pi$ de la page est le groupe profini libre $\hat F_2$, complété de $\pi_1(\mathbf P^1(\mathbf C) \smallsetminus \{0, 1, \infty\})$ ; les sous-groupes $L_0$, $L_1$, $L_\infty$ sont les sous-groupes d'inertie des trois pointes, et les \q{rectificateurs} sont les éléments par lesquels on conjugue l'image de chacun d'eux pour retrouver un $L_{\sigma(i)}$. Les droites tangentes aux points marqués de la section~\ref{sec:146} sont les points base tangentiels de Deligne \cite{deligne1989}. Le groupe $\mathfrak S_3$ des six substitutions anharmoniques, qui permute les trois pointes, revient aux sections~\ref{sec:146}, \ref{sec:62} et~\ref{sec:64}. Les énoncés de la cote~142 (catégorie de Teichmüller--Galois, image de Galois sur une seule courbe) et de la cote~149, non démontrés, sont encadrés à la fin de cette partie ; ceux de la cote~147 dans la partie \q{Topologie combinatoire, surfaces et cartes}.

\noindent Deux ensembles inédits de la même époque prolongent cet axe vers les espaces de modules : les \emph{Teichmülleries} (cote 144, 1981--1983), avec une \q{Rétrospection sur les cartes cellulaires} de 1982 et les présentations du groupe des tresses $B_3$, et la \emph{Structure à l'infini des $M_{g,\nu}$} (cote 147). Ce sont des textes suivis, jamais édités. Aucun énoncé de 144 n'est formalisé ici ; ceux de 147 sont dans la partie « Topologie combinatoire, surfaces et cartes ».

\noindent\emph{Conventions.} Mathlib n'a ni le groupe profini libre ni les puissances d'exposant dans $\hat{\mathbf Z}$. Une relation vaut dans $\hat\pi$ si et seulement si elle vaut pour toute image de $(l_0, l_1)$ dans tout groupe fini, et $p \in \hat{\mathbf Z}$ agit sur un groupe fini $G$ par son résidu modulo $\operatorname{card} G$. On représente donc $p$ par une famille compatible de résidus $p_n \in \mathbf Z/n$, $n \geq 1$, et l'on pose $x^p = x^{p_{\operatorname{card} G}}$ dans un groupe fini~$G$. La relation (14) pour $p$ signifie : pour tout groupe fini $G$ et tous $x, y, z \in G$ tels que $zyx = 1$, on a $z^p y^p x^p = 1$.

\begin{theoreme}[Grothendieck, pages 34 et 35, l'exercice\piste{145-unit-exponent-exercise}]\label{thm:145-exercice}
Soit $p \in \hat{\mathbf Z}^*$. Si $l_\infty^p\, l_1^p\, l_0^p = 1$ dans le groupe profini libre sur $l_0$, $l_1$, avec $l_\infty l_1 l_0 = 1$, alors $p = 1$. Autrement dit, la relation (14) vaut pour $p$ si et seulement si $p_n = 1$ pour tout $n \geq 1$.
\end{theoreme}

\begin{proof}
La réciproque est claire. Soit $N \geq 1$. Comme $p_2$ est inversible dans $\mathbf Z/2$, $p_2 = 1$, et par compatibilité le représentant $m \in [0, 2N[$ de $p_{2N}$ est impair. Dans le groupe diédral $D_N$, d'ordre $2N$, soient $x$ et $y$ deux réflexions dont le produit $r = yx$ est une rotation d'ordre $N$, et $z = r^{-1}$, de sorte que $zyx = 1$. Comme $m$ est impair, $x^m = x$ et $y^m = y$, donc $z^m y^m x^m = r^{-m} r = r^{1 - m}$, qui vaut $1$ si et seulement si $m \equiv 1 \pmod N$. La relation (14) dans $D_N$ donne donc $p_N = 1$, image de $p_{2N}$.
\end{proof}

\begin{remarque}
L'énoncé tient sous une hypothèse plus faible : seule sert l'imparité de $p$, c'est-à-dire $p_2 = 1$, et non l'inversibilité de $p$ aux nombres premiers impairs. L'imparité ne peut être omise, car $p = 0$ vérifie (14). La compatibilité de la famille ne sert qu'à passer de $p_{2N}$ à $p_N$ et à $p_2$.
\end{remarque}

\noindent La preuve vérifiée établit l'équivalence pour toute famille compatible impaire (\texttt{rel14\_iff}), en déduit la forme de la page pour $p \in \hat{\mathbf Z}^*$ (\texttt{rel14\_unit\_iff}) et montre que $p = 0$ vérifie (14) (\texttt{rel14\_zero}). Elle ne construit pas $\hat F_2$ : la relation y est lue dans tous les groupes finis, ce qui revient au même par définition de la complétion profinie.

\begin{remarque}
La relation (14) a la forme de la relation hexagonale de $\widehat{GT}$ pour $f = 1$. Un élément de $\widehat{GT}$ est un couple $(\lambda, f)$, $\lambda \in \hat{\mathbf Z}^*$, $f$ dans l'adhérence du groupe dérivé de $\hat F_2$, soumis entre autres à $f(z, x)\,z^m f(y, z)\,y^m f(x, y)\,x^m = 1$ pour $xyz = 1$ et $m = (\lambda - 1)/2$ (relation~(5) chez Furusho 2010 \cite{furusho2010}, d'après Drinfeld \cite{drinfeld1990}). Pour $f = 1$, elle devient $z^m y^m x^m = 1$ sous $xyz = 1$ : l'ordre des facteurs est renversé par rapport à~(14). Le même quotient diédral montre que ses seules solutions sont $m = 0$ et $m = -1$, c'est-à-dire $\lambda = \pm 1$ : pour $m$ impair, deux réflexions $x$, $y$ et $z = (xy)^{-1}$ donnent $(yx)^{m+1} = 1$, d'où $m \equiv -1$ modulo tout~$N$ ; pour $m$ pair, $z^m = 1$ donne $m \equiv 0$ ; et $m = -1$ convient, $z^{-1}y^{-1}x^{-1} = (xyz)^{-1}$. Cet argument est de l'édition et n'est pas vérifié en Lean. Il rejoint le cas discret de la page~35, où $p = \pm 1$.
\end{remarque}

Ne sont pas démontrés ici : la conséquence pour $S\hat{\hat{\mathcal E}}$ (les systèmes à rectificateurs triviaux sont les six $(\operatorname{sg}\sigma, \sigma)$ de $\Gamma_P$), qui demande le groupe $\Gamma_P$ et la réduction de la page aux $\sigma$ paires, ni le cas discret de la page~35.
\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{definition*}[Grothendieck, pages 2 à 16, catégorie de Teichmüller--Galois\piste{142-teichmuller-galois-category-etale}]
La catégorie de Teichmüller--Galois a pour objets les courbes anabéliennes de tous types $(g, \nu)$ et pour flèches les complétés profinis des classes d'isotopie d'applications étales finies ; elle est obtenue par une complétion profinie des catégories dont les groupes d'automorphismes vérifient la condition de finitude $(\ast)$, l'image du stabilisateur de chaque flèche $u : X \to Y$ étant d'indice fini dans $\mathrm{Aut}(Y)$. Chaque groupe d'automorphismes y est le groupe de Teichmüller profini ; la construction est algébrique, invariante par extension de corps algébriquement clos de caractéristique~$0$, et $\mathrm{Aut}(k)$ y opère.
\end{definition*}
\end{encadre}
{\small Les flèches de cette catégorie relient des types $(g, \nu)$ différents par des applications étales finies, et non par les inclusions de sous-surfaces et les recollements de la tour de Teichmüller. Sur cette tour, Hatcher, Lochak et Schneps font agir le sous-groupe $\Lambda$ de $\widehat{GT}$ défini par une relation de plus, et montrent que $\Lambda$ s'injecte dans les automorphismes extérieurs spéciaux de la tour (2000, théorèmes~A à~C \cite{hatcherlochakschneps2000}). Dans la catégorie de la page, l'action de $\mathrm{Aut}(k)$ est l'analogue, pour tous les types, de l'action de Galois sur $\hat\pi_1(M_{0,4}) = \hat F_2$ de la section~\ref{sec:145}. Mathlib n'a pas la complétion profinie des catégories ni les groupes de Teichmüller. On se reportera aux notes de Grothendieck (\lot{142}{1}{2}).\par}

\begin{encadre}
\begin{theoreme*}[Grothendieck, pages 167 et 175 à 180, monodromie modérée à plusieurs paramètres\piste{34-multiparameter-tame-monodromy}]\nonverifie
Soient $S$ un schéma strictement local de dimension quelconque et $\bar X$ un $S$-schéma projectif et plat, de fibre fermée à croisements normaux hors de la codimension~$2$, lisse à bord à croisements normaux relatifs au-dessus d'un ouvert $U \subset S$. L'image de $\pi_1(U)$ dans $\mathrm{Out}(\pi_1^{(p')})$ d'une fibre géométrique est un groupe abélien d'ordre premier à $p$, de rang au plus le nombre $\nu$ de points doubles en dimension relative~$1$.
\end{theoreme*}
\end{encadre}
{\small Les feuillets en esquissent une démonstration incomplète (pages 175 à 180), où le lemme~3.1, sur la courbe nodale verselle, n'est pas démontré. Les hypothèses (a) à (d) reposent sur des lectures incertaines de la page~167. Sur une base de dimension~$1$, la finitude de l'image de l'inertie sauvage dans $\mathrm{Out}(\pi_1^{(p')})$ d'une fibre géométrique, pour toute variété sur un corps complet de valuation discrète, est le théorème~2.1 de Kisin (2000) \cite{kisin2000}, démontré par les altérations et non par réduction aux courbes. En dimension relative~$1$, la lecture y voit la description de la monodromie le long d'une courbe stable dégénérée par les twists de Dehn des points doubles, élevés aux multiplicités~$n_i$ des équations locales $xy = t^{n_i}$ ; en dimension relative $\geq 2$, l'énoncé encadré reste ouvert ici. Quand $S \smallsetminus U$ est un diviseur à $r$ branches à croisements normaux, le groupe fondamental modéré de $U$ au voisinage du point fermé est $\prod_{\ell \neq p} \mathbf Z_\ell(1)^r$ (SGA~1, exposé~XIII, appendice~I, corollaire~5.3 \cite{sga1}), abélien d'ordre premier à~$p$ ; la section~\ref{sec:29} en calcule la fonctorialité. Mathlib n'a pas la monodromie modérée. On se reportera aux notes de Grothendieck (\lot{34}{9}{167}).\par}

\begin{encadre}
\begin{contrexemple*}[pages 36 à 39, le lemme du Complément\piste{149-dominant-faithfulness-curves}]\nonverifie
Le lemme de la page~36, qui omet l'hypothèse de~$(\ast)$ sur les groupes fondamentaux, est faux pour les courbes hyperboliques de types $(1,1)$ et $(1,2)$, et réduire l'ouvert $V$ n'écarte pas le cas exceptionnel $\operatorname{card} I = 1$. L'extension que la page annonce aux polycourbes hyperboliques de toute dimension repose sur un plongement dans une variété semi-abélienne, qui manque en dimension~$2$ : la courbe elliptique universelle privée de sa section nulle, au-dessus de $Y(N)$, n'en a pas.
\end{contrexemple*}
\end{encadre}
{\small Pour les courbes, l'énoncé de la piste, en caractéristique~$0$ sur un corps algébriquement clos (deux morphismes $f, g : X \to Y$ vers une courbe hyperbolique, $f$ dominant, qui induisent le même homomorphisme extérieur des groupes fondamentaux étales profinis, sont égaux), n'est pas démontré ici ; l'édition ferme les types $(1,1)$ et $(1,2)$ par l'hypothèse de~$(\ast)$. Mathlib n'a pas le groupe fondamental étale des courbes hyperboliques. On se reportera aux notes de Grothendieck (\lot{149}{2}{21}).\par}

\begin{encadre}
\begin{theoreme*}[Grothendieck, pages 153 à 155, 1-asphéricité locale\piste{34-lci-local-1-asphericity}]\nonverifie
Soit $f : X \to S$ plat sur un trait strictement local, de fibre fermée $X_0$ localement d'intersection complète, dont le lieu non lisse est de codimension $\geq 2$ dans $X_0$. Alors $f$ est localement 1-asphérique pour les premiers $\neq p$ ; si $f$ est propre, la spécialisation $H^1(X_0, G) \to H^1(X_{\bar\eta}, G)$ est bijective pour tout groupe fini $G$ d'ordre premier à~$p$.
\end{theoreme*}
\end{encadre}
\begin{demopage}[pages 153 à 155]
Au n\textsuperscript{o}~5.5, $f$ étant localement 1-acyclique aux générisations strictes de $x$, la 1-asphéricité locale en $x$ pour un groupe fini $G$ d'ordre premier à $p$ se ramène à (5.5.1), $H^i(\bar V, G) \simeq H^i(V_{\bar\eta}, G)$ pour $i \leq 1$ (p.~153), puis à (5.5.2), $H^i(V(h), G) = 0$ pour $i \leq 1$ (p.~154). La page affirme sans démonstration (\q{On sait}) que (5.5.2) vaut aux points d'intersection complète de dimension $\geq 3$, et la lecture le rapporte à la pureté de SGA~2. Pour $f$ plat, cela revient à $X_0$ d'intersection complète de dimension $\geq 2$ en $x$, et le cas lisse traite les autres points, d'où le théorème~5.6 et, sans autre argument, l'assertion sur $H^1$.
\end{demopage}

\begin{encadre}
\begin{conjecture*}[D'après les pages 94, 95 et 98 à 101, forme regroupée par l'édition, image de Galois sur une seule courbe\piste{142-galois-image-conditions-single-curve}]
Soient $X$ une courbe algébrique anabélienne sur un corps $K$ de type fini sur $\mathbf Q$ et $\Theta$ un automorphisme du groupoïde fondamental profini $\hat\Pi_1(X, I)$ qui fixe les points base. Si $\Theta$ se relève à $\hat\Pi_1(X', I')$ pour tout revêtement étale fini $X'$ de $X$ défini sur $K$, respecte les noyaux de $\hat\pi_1(X', x') \to \hat\pi_1(Y, f(x'))$ pour tout $K$-morphisme $f : X' \to Y$, est compatible aux morphismes entre revêtements et vérifie la condition des lacets avec un seul multiplicateur, alors $\Theta$ provient de $\mathrm{Gal}(\bar K/K)$. Ces conditions sont nécessaires.
\end{conjecture*}
\end{encadre}
{\small La page~95 conjecture suffisantes les conditions de relèvement et de noyaux ; leur regroupement avec les conditions des pages 98 à 101 est de l'édition. En termes actuels, c'est une forme de la question d'Ihara et de la conjecture d'Oda--Matsumoto (I/OM) attachée à une seule courbe et à ses revêtements : I/OM demande si $\mathrm{Gal}(\overline K/K)$ est le groupe des automorphismes du foncteur groupe fondamental géométrique sur une catégorie de $K$-variétés. Topaz (2018) \cite{topaz2018} en démontre une forme renforcée, pour le quotient modulo~$\ell$ abélien-par-central de ce groupe, sur un corps parfait infini de caractéristique $\neq \ell$ et pour toute catégorie de variétés assez grosse au sens de son §~1.7 ; cette forme porte sur une catégorie de variétés, non sur une courbe et ses revêtements, et ne fait pas intervenir de condition d'inertie. Les variantes tripodes finies de Pop (2019) \cite{pop2019} supposent une base de dimension au moins deux, munie d'un nombre fini d'applications rationnelles dominantes vers $\mathbf P^1 \smallsetminus \{0,1,\infty\}$ ; elles ne couvrent donc pas les revêtements d'une seule courbe, et c'est la condition des lacets de la page qui devrait en tenir lieu. Pour $X = \mathbf P^1 \smallsetminus \{0, 1, \infty\}$, la condition des lacets est celle des sous-groupes $L_0$, $L_1$, $L_\infty$ de la section~\ref{sec:145}. Mathlib n'a pas les groupoïdes fondamentaux profinis des courbes. On se reportera aux notes de Grothendieck (\lot{142}{5}{94}).\par}

\begin{encadre}
\begin{conjecture*}[Grothendieck, pages 72 à 77 et 84 à 93, spécialisation vers une pointe\piste{149-cusp-specialisation-index}]
Soient $U = X \setminus T$ une courbe hyperbolique relative sur un trait et $f$ une section rationnelle qui rencontre la section de pointe $g_{i_0}$ dans la fibre spéciale avec la multiplicité $n$. L'inertie s'envoie sur $n$ fois le sous-groupe de lacet $L_{i_0}$ de cette pointe, et elle agit trivialement exactement quand $f$ se prolonge.
\end{conjecture*}
\end{encadre}
{\small Mathlib n'a pas la spécialisation des sections des courbes hyperboliques relatives. On se reportera aux notes de Grothendieck (\lot{149}{4}{72}).\par}