\section[Cote 146 : les exposants trivialisants de $L_i$ et de $L$ sur $M_{0,n}$]{Cote 146 : les exposants trivialisants de $L_i$ et de $L$ sur $M_{0,n}$\protect\verifie{Folder146}}\label{sec:146}

La cote 146, \emph{Groupoïdes de Teichmüller}, cent trente-trois pages que l'inventaire date \q{[à partir de 1978]}, porte page~70 un tableau : pour $n = \operatorname{card} I = 4, 5, 6$, le plus petit exposant qui rend trivial, de façon compatible au groupe symétrique, le fibré $L = \bigotimes L_i$ sur $M_{0,I}$, et les fibrés $L_i$ attachés aux points marqués (\lot{146}{4}{70}). Pour $n = 4$ il donne $3$ pour $L$ et $6$ pour $L_i$ ; les colonnes $n = 5$ et~$6$ portent des points d'interrogation. La lecture ne vérifie pas le tableau, et la piste tombe si les valeurs pour $n = 4$ ne se vérifient pas.

\noindent\emph{Conventions.} $M_{0,4} = U = \mathbf P^1 \setminus \{0, 1, \infty\}$, de coordonnée $\lambda$, le quatrième point étant mobile. Le groupe $\mathfrak S_{I \setminus \{4\}} \simeq \mathfrak S_3$ permute $0$, $1$, $\infty$ et agit sur $U$ par les six substitutions anharmoniques $g$, et sur la droite tangente $L_4$ au point mobile par la dérivée $g'(\lambda)$. Par la règle de dérivation des fonctions composées, $g \mapsto g'(\lambda)$ est un $1$-cocycle de $\mathfrak S_3$ à valeurs dans les unités de $\mathcal O(U)$. Comme $\mathrm{Pic}(U) = 0$, l'exposant cherché est l'ordre de sa classe : le plus petit $m \geq 1$ tel que $g'(\lambda)^m = h(g\lambda)/h(\lambda)$ pour une unité~$h$.

\begin{theoreme}[Grothendieck, page 70, colonne $n = 4$, pour $L_4$\piste{146-equivariant-trivialising-exponents}]\label{thm:146-six}
Soit $K$ un corps où $2$ et $3$ sont inversibles et qui contient une racine $\zeta$ de $\zeta^2 - \zeta + 1$. La classe de $L_4$ est d'ordre exactement $6$ : on a $g'(\lambda)^6 = h(g\lambda)/h(\lambda)$ avec $h = \lambda^4(1 - \lambda)^4$, et si $g'(\lambda)^m = h(g\lambda)/h(\lambda)$ pour tous $g$ et $\lambda \in U(K)$, pour une fonction $h$ quelconque sans zéro sur $U(K)$, alors $6 \mid m$.
\end{theoreme}

\begin{proof}
L'égalité pour $m = 6$ se vérifie sur les six substitutions ; par exemple, pour $g(\lambda) = 1/\lambda$, $g'(\lambda)^6 = \lambda^{-12}$ et $h(1/\lambda) = \lambda^{-8}(\lambda - 1)^4$. Réciproquement, en un point $\lambda_0$ fixé par $g$, le second membre vaut~$1$. Le point $-1$ est fixé par $g(\lambda) = 1/\lambda$, et $g'(-1) = -1$, d'où $(-1)^m = 1$ et $2 \mid m$. Le point $\zeta$ est fixé par $g(\lambda) = 1/(1 - \lambda)$, car $\zeta(1 - \zeta) = 1$, et $g'(\zeta) = 1/(1 - \zeta)^2 = \zeta^2$, racine primitive cubique de l'unité puisque $3 \neq 0$ ; d'où $3 \mid m$.
\end{proof}

La figure~\ref{fig:146-m04} montre où se trouvent ces points fixes. Sur la droite réelle, chacune des trois transpositions fixe un point de $U$ : $1/\lambda$ fixe $-1$, $1 - \lambda$ fixe $1/2$ et $\lambda/(\lambda - 1)$ fixe $2$, et la dérivée y vaut $-1$ dans les trois cas. Les deux $3$-cycles permutent circulairement ces trois points et ne fixent que $\zeta$ et $\bar\zeta$, les sommets des deux triangles équilatéraux de base $[0, 1]$, où la dérivée est une racine primitive cubique de l'unité. Ce sont les seuls points de $U$ de stabilisateur non trivial.

\begin{figure}[htbp]
\centering
\begin{tikzpicture}[x=2cm, y=2cm, >=stealth, every node/.style={font=\small}]
\draw[black!45] (-1.7,0) -- (2.8,0) node[right] {$\mathbf R$};
\draw[black!30, dashed] (0,0) -- (0.5,0.866) -- (1,0) (0,0) -- (0.5,-0.866) -- (1,0);
\foreach \x/\l in {0/0, 1/1} { \draw[fill=white] (\x,0) circle (2pt); \node[below=3pt] at (\x,0) {$\l$}; }
\node[right] at (2.8,0.25) {$\infty$ retiré};
\foreach \x/\l in {-1/-1, 0.5/\tfrac12, 2/2} { \fill (\x,0) circle (2pt); \node[below=3pt, fill=white, inner sep=1pt] at (\x,0) {$\l$}; }
\fill (0.5,0.866) circle (2pt) node[above right] {$\zeta$};
\fill (0.5,-0.866) circle (2pt) node[below right] {$\bar\zeta$};
\draw[->, shorten >=3pt, shorten <=3pt] (-1,0) to[bend left=35] (0.5,0);
\draw[->, shorten >=3pt, shorten <=3pt] (0.5,0) to[bend left=35] (2,0);
\draw[->, shorten >=3pt, shorten <=3pt] (2,0) to[bend right=32] node[pos=0.82, above left=-1pt] {\footnotesize $\frac{1}{1-\lambda}$} (-1,0);
\node[black!70] at (-1,-0.36) {\footnotesize $1/\lambda$};
\node[black!70, fill=white, inner sep=1pt] at (0.5,-0.38) {\footnotesize $1 - \lambda$};
\node[black!70] at (2,-0.36) {\footnotesize $\lambda/(\lambda - 1)$};
\node[align=left, anchor=west] at (0.75,0.86) {fixé par $\frac{1}{1-\lambda}$, dérivée $\zeta^2$};
\node[align=left, anchor=west] at (0.75,-0.86) {fixé par $\frac{1}{1-\lambda}$, dérivée $\bar\zeta^2$};
\end{tikzpicture}
\caption{$M_{0,4} = \mathbf P^1 \setminus \{0, 1, \infty\}$ et ses points de stabilisateur non trivial. Les points $-1$, $1/2$, $2$ sont fixés par les transpositions $1/\lambda$, $1 - \lambda$, $\lambda/(\lambda - 1)$ ; les flèches figurent le $3$-cycle $\lambda \mapsto 1/(1 - \lambda)$, qui les permute et fixe $\zeta$ et $\bar\zeta$. Le facteur $-1$ force $2 \mid m$, le facteur $\zeta^2$ force $3 \mid m$.}
\label{fig:146-m04}
\end{figure}

\begin{remarque}
La valeur $6$ du tableau tient, et la piste ne tombe pas. L'argument par les points fixes est celui que la lecture de la cote 140-1 donne pour $\mathcal O(1)$ sur $\mathbf P(V_J)$ (§\,\ref{sec:140-1}) ; il ne demande pas de calculer les unités de~$U$, et la minoration vaut même parmi toutes les fonctions sans zéro sur~$U(K)$.
\end{remarque}

\noindent La preuve vérifiée contient la loi de groupe des six substitutions et la règle de cocycle, $g \mapsto g'(\lambda)$ vérifiant $(gh)'(\lambda) = g'(h\lambda)\,h'(\lambda)$ (\texttt{anh\_mul}, \texttt{der\_mul}), l'égalité pour $m = 6$ (\texttt{der\_pow\_six}) et la divisibilité $6 \mid m$ (\texttt{six\_dvd}), pour tout $m \in \mathbf Z$. Elle ne contient ni le fibré $L_4$ ni le groupe de Picard équivariant : l'énoncé est celui du cocycle, et sa traduction en fibrés est la convention ci-dessus.

\begin{remarque}
La fibre de $L_4$ en $\lambda$ est la droite des vecteurs tangents en $\lambda$, c'est-à-dire l'ensemble des points base tangentiels de Deligne \cite{deligne1989} au point mobile, privé de zéro ; l'exposant $6$ dit que $L_4^{\otimes 6}$, et aucune puissance plus petite, admet une section partout non nulle compatible à $\mathfrak S_3$. Le groupe et l'action sont ceux de la section~\ref{sec:62}, où le quotient de $U$ par $\mathfrak S_3$ est la fonction $j$, et de l'épinglage de Legendre de la section~\ref{sec:64}, où $\mathfrak S_3$ opère sur $U_{0,3} = U$ et sur un $\mu_4$-torseur ; le groupe profini $\hat\pi$ de $U$ est l'objet de la section~\ref{sec:145}. Les points fixes $-1$ et $\zeta$ de la démonstration sont les points de $U$ au-dessus de $j = 0$ et $j = 1$ dans la normalisation de la section~\ref{sec:62}, la seule où le stabilisateur n'est pas trivial.
\end{remarque}

Passons à la seconde entrée de la colonne $n = 4$, celle du fibré $L = L_1 \otimes L_2 \otimes L_3 \otimes L_4$ sous le groupe $\mathfrak S_4$ tout entier. Une permutation des quatre points marqués induit un automorphisme de la fibre $\mathbf P^1$, et elle agit sur $L$ par le produit des dérivées de cet automorphisme aux quatre points. Deux remarques ramènent ce calcul à celui de $L_4$. D'abord, le groupe de Klein $V_4 \subset \mathfrak S_4$, formé des trois produits de deux transpositions disjointes, agit trivialement sur $U$ : la permutation $(12)(34)$ ne change pas le birapport. Il agit aussi trivialement sur $L$, car l'automorphisme échange les deux points de chaque paire et les dérivées en ces deux points ont pour produit~$1$. Le quotient $\mathfrak S_4/V_4$ s'identifie au stabilisateur $\mathfrak S_3$ du quatrième point. Ensuite, pour $g$ dans ce stabilisateur, les dérivées en $0$, $1$ et $\infty$ (dans la carte $1/\lambda$ en $\infty$) ont un produit constant, égal à la signature $\varepsilon(g)$, et la dérivée au point mobile est $g'(\lambda)$. Le cocycle de $L$ est donc $g \mapsto \varepsilon(g)\, g'(\lambda)$.

\begin{theoreme}[Grothendieck, page 70, colonne $n = 4$, pour $L$\piste{146-equivariant-trivialising-exponents}]\label{thm:146-trois}
Soit $K$ un corps où $3$ est inversible et qui contient une racine $\zeta$ de $\zeta^2 - \zeta + 1$. Le cocycle $g \mapsto \varepsilon(g)\,g'(\lambda)$ est d'ordre exactement~$3$ : sa puissance $m$-ième est le cobord $h(g\lambda)/h(\lambda)$ d'une fonction $h$ sans zéro sur $U(K)$ si et seulement si $3 \mid m$, et pour $m = 3$ on peut prendre $h = \lambda^2(1 - \lambda)^2$.
\end{theoreme}

\begin{proof}
Pour $m = 3$, on vérifie l'égalité sur les six substitutions ; pour $g(\lambda) = 1/\lambda$, le cocycle vaut $(-1)\cdot(-\lambda^{-2}) = \lambda^{-2}$, son cube $\lambda^{-6}$, et $h(1/\lambda)/h(\lambda) = \lambda^{-4}(\lambda - 1)^2/(\lambda^2(1 - \lambda)^2) = \lambda^{-6}$. Les multiples de $3$ suivent en prenant $h^{m/3}$. Réciproquement, au point $\zeta$ fixé par $g(\lambda) = 1/(1 - \lambda)$, une permutation paire, le cocycle vaut $\zeta^2$ et le second membre vaut~$1$, d'où $3 \mid m$ comme pour $L_4$.
\end{proof}

La signature tue exactement le facteur d'ordre~$2$ : au point $-1$, fixé par $1/\lambda$, le cocycle de $L$ vaut $(-1)\cdot(-1) = 1$, et il ne reste que l'ordre~$3$ venu de $\zeta$. La valeur $3$ du tableau tient donc. La page~72 n'affirme, elle, que $L^{\otimes 6} \simeq 1$, ce qui est vrai et plus faible.

\noindent Vérifié au niveau des cocycles (\texttt{sgn\_mul}, \texttt{derL\_mul}, \texttt{derL\_pow\_three}, \texttt{coboundary\_derL\_iff}). Lean ne démontre ni que $V_4$ agit trivialement, ni que le produit des dérivées en $0$, $1$, $\infty$ est la signature, ni que l'ordre sous $\mathfrak S_4$ est celui sous $\mathfrak S_3$ (injectivité de l'inflation $H^1(\mathfrak S_3, \cdot) \to H^1(\mathfrak S_4, \cdot)$) : ces trois points forment la traduction du fibré $L$ en cocycle, faite dans le texte ci-dessus.

Passons à la colonne $n = 5$. Le tableau y porte \q{$12\,?$} pour $L$ comme pour $L_i$, et, plus bas sur la même page, un calcul aboutit à $(L^4)^3 \simeq \mathcal O$, c'est-à-dire $L^{\otimes 12} \simeq \mathcal O$. La question est donc de savoir si $12$ est le meilleur exposant dans les deux cas.

\noindent\emph{Le modèle.} Un point de $M_{0,5}$ est une droite projective munie de cinq points distincts ; on envoie les trois premiers en $0$, $1$, $\infty$, et il reste deux coordonnées $(\lambda, \mu)$, avec $\lambda, \mu \notin \{0, 1\}$ et $\lambda \neq \mu$. Le groupe $\mathfrak S_5$ est engendré par les quatre transpositions $s_1 = (12)$, $s_2 = (23)$, $s_3 = (34)$, $s_4 = (45)$. Chacune permute les étiquettes ; on renvoie alors les trois premiers points en $0$, $1$, $\infty$ par une homographie $\varphi$, ce qui donne une substitution rationnelle :
\[
s_1 : (1 - \lambda,\ 1 - \mu), \quad s_2 : \Bigl(\frac{\lambda}{\lambda - 1},\ \frac{\mu}{\mu - 1}\Bigr), \quad s_3 : \Bigl(1 - \lambda,\ \frac{\mu(\lambda - 1)}{\lambda - \mu}\Bigr), \quad s_4 : (\mu, \lambda).
\]
L'homographie $\varphi$ agit aussi sur les droites tangentes aux points marqués, par sa dérivée. Sur $L_5$, la tangente au cinquième point, le facteur est $\varphi'(\mu)$ ; il n'a de sens que pour les permutations qui fixent le cinquième point, d'où le groupe $\mathfrak S_4$ engendré par $s_1, s_2, s_3$. Sur $L$, le facteur est le produit des dérivées aux cinq points (dans la carte $1/z$ en $\infty$). On trouve, pour $s_1, s_2, s_3, s_4$ :
\[
c_L = -1,\ \ \frac{-1}{(\lambda - 1)^2(\mu - 1)^2},\ \ \frac{\lambda(\lambda - 1)}{(\lambda - \mu)^2},\ \ 1 ; \qquad
c_5 = -1,\ \ \frac{-1}{(\mu - 1)^2},\ \ \frac{\lambda(\lambda - 1)}{(\lambda - \mu)^2}.
\]
Sur un produit de générateurs, le facteur se calcule par la règle de cocycle $c(gh)(x) = c(g)(hx)\,c(h)(x)$, qui n'est autre que la dérivation des fonctions composées. Comme pour $n = 4$, $M_{0,5}$ est le complémentaire d'un arrangement de droites, son groupe de Picard est nul, et l'exposant cherché est l'ordre de la classe du cocycle : le plus petit $m \geq 1$ tel que $c^m$ soit le cobord $h(gx)/h(x)$ d'une fonction $h$ sans zéro.

\noindent\emph{Le calcul.} Les fonctions inversibles sur $M_{0,5}$ sont, à une constante près, les monômes en $\lambda$, $\mu$, $1 - \lambda$, $1 - \mu$ et $\lambda - \mu$. Chercher $h$ revient à résoudre un système linéaire sur les exposants de ces cinq facteurs, plus une condition de signe sur la constante. Un calcul formel (sympy), qui retrouve d'abord les valeurs $3$ et $6$ pour $n = 4$, donne l'ordre $4$ pour $L$ et l'ordre $12$ pour $L_5$, avec les fonctions $h$ ci-dessous. Pour minorer, on raisonne comme pour $n = 4$ par les points fixes. Prenons $i$ avec $i^2 = -1$. Le $4$-cycle $s_1 s_2 s_3$ fixe le point $(\lambda, \mu) = (-1, i)$ : l'homographie correspondante est $z \mapsto (z + 1)/(1 - z)$, qui envoie $0 \mapsto 1 \mapsto \infty \mapsto -1 \mapsto 0$ et fixe $i$. Sa dérivée en $i$ vaut $2/(1 - i)^2 = i$, une racine primitive quatrième de l'unité. Le $3$-cycle $s_1 s_2$, lui, fixe $(1 - \zeta, \zeta)$, où $\zeta^2 - \zeta + 1 = 0$ ; l'homographie est $z \mapsto 1/(1 - z)$, et sa dérivée en $\zeta$ vaut $\zeta^2$.

La figure~\ref{fig:146-m05} dessine la partie réelle de ce modèle. Les cinq droites retirées sont les lieux d'annulation des cinq unités $\lambda$, $\mu$, $1 - \lambda$, $1 - \mu$, $\lambda - \mu$, d'où le système linéaire sur leurs exposants. Deux des générateurs s'y voient : $s_4$ est la symétrie par rapport à la diagonale, $s_1$ la symétrie de centre $(1/2, 1/2)$. Les deux points fixes qui servent de certificats sont complexes et ne figurent que par leurs coordonnées.

\begin{figure}[htbp]
\centering
\begin{tikzpicture}[x=1.4cm, y=1.4cm, >=stealth, every node/.style={font=\small}]
\fill[black!4] (-1.2,-1.2) rectangle (2.2,2.2);
\draw[thick] (0,-1.2) -- (0,2.2);
\draw[thick] (1,-1.2) -- (1,2.2) node[above] {$\lambda = 1$};
\draw[thick] (-1.2,0) -- (2.2,0);
\draw[thick] (-1.2,1) -- (2.2,1) node[right] {$\mu = 1$};
\draw[thick] (-1.2,-1.2) -- (2.2,2.2) node[above right] {$\lambda = \mu$};
\node[above left] at (0,2.2) {$\lambda = 0$};
\node[below right] at (2.2,0) {$\mu = 0$};
\fill (0.5,0.5) circle (1.6pt);
\draw[black!50] (0.5,0.5) -- (1.5,-0.6) node[right] {\footnotesize centre de $s_1$};
\draw[<->, black!60] (2.0,0.8) to[bend right=25] (0.8,2.0) node[left] {\footnotesize $s_4$};
\end{tikzpicture}
\qquad
\begin{minipage}[b]{0.36\textwidth}\small\raggedright
Points complexes fixes :\\[2pt]
$(-1, i)$, fixé par le $4$-cycle $s_1 s_2 s_3$, facteur $i$ sur $L_5$ et sur $L$ ;\\[2pt]
$(1 - \zeta, \zeta)$, fixé par le $3$-cycle $s_1 s_2$, facteur $\zeta^2$ sur $L_5$, $1$ sur $L$.\\[6pt]
\end{minipage}
\caption{La partie réelle de $M_{0,5}$ dans les coordonnées $(\lambda, \mu)$ : le complémentaire des cinq droites $\lambda = 0$, $\lambda = 1$, $\mu = 0$, $\mu = 1$, $\lambda = \mu$. Les points fixes qui donnent les minorations $4 \mid m$ et $3 \mid m$ ne sont pas réels.}
\label{fig:146-m05}
\end{figure}


\begin{theoreme}[conjecture de la page 70, colonne $n = 5$, pour $L_i$ (\q{$12\,?$}), démontrée par l'édition\piste{146-equivariant-trivialising-exponents}]\label{thm:146-douze}
Soit $K$ un corps où $2$ et $3$ sont inversibles, qui contient $i$ avec $i^2 = -1$ et une racine $\zeta$ de $\zeta^2 - \zeta + 1$. La puissance $m$-ième du cocycle $c_5$ de $L_5$ sous $\mathfrak S_4$ est le cobord d'une fonction sans zéro sur $M_{0,5}(K)$ si et seulement si $12 \mid m$. Pour $m = 12$ on peut prendre
\[
h = \frac{\mu^6 (1 - \mu)^6 (\lambda - \mu)^6}{\lambda^2 (1 - \lambda)^2}.
\]
\end{theoreme}

\begin{proof}
Pour $m = 12$, l'égalité $c_5(s)^{12} = h(sx)/h(x)$ se vérifie sur les trois générateurs, par exemple pour $s_1$ : $c_5 = -1$, et $h$ est invariante par $(\lambda, \mu) \mapsto (1 - \lambda, 1 - \mu)$. Elle passe aux produits de générateurs, puisque les deux membres suivent la même règle de cocycle. Réciproquement, au point $(-1, i)$, fixé par $s_1 s_2 s_3$, le second membre vaut $1$ et le cocycle vaut $i$, d'où $i^m = 1$ et $4 \mid m$ ; au point $(1 - \zeta, \zeta)$, fixé par $s_1 s_2$, il vaut $\zeta^2$, d'où $3 \mid m$.
\end{proof}

\begin{contrexemple}[page 70, colonne $n = 5$, pour $L$ : le \q{$12\,?$} n'est pas le meilleur exposant\piste{146-equivariant-trivialising-exponents}]\label{ce:146-quatre}
Sous les mêmes hypothèses (il suffit que $2$ soit inversible et que $i$ existe), la puissance $m$-ième du cocycle $c_L$ de $L$ sous $\mathfrak S_5$ est un cobord si et seulement si $4 \mid m$. Pour $m = 4$ on peut prendre $h = \bigl(\lambda\mu(1 - \lambda)(1 - \mu)(\lambda - \mu)\bigr)^2$. Le meilleur exposant pour $L$ est donc $4$, et non $12$.
\end{contrexemple}

\begin{proof}
Sur les générateurs, $c_L(s)^4 = h(sx)/h(x)$ se vérifie directement ; par exemple pour $s_4$, $c_L = 1$ et $h$ est symétrique en $\lambda$, $\mu$. Au point $(-1, i)$, le facteur de $L$ est encore $i$ : les quatre autres points forment un seul cycle, et le produit des dérivées le long d'un cycle de longueur $4$ est la dérivée de $\varphi^4 = \mathrm{id}$, soit $1$. D'où $4 \mid m$. L'ordre $3$ disparaît : au point $(1 - \zeta, \zeta)$, les dérivées aux deux points fixes $\zeta$ et $1 - \zeta$ sont inverses l'une de l'autre, comme la signature compensait la dérivée en $-1$ pour $n = 4$.
\end{proof}

Le $12$ de la page pour $L$ est donc un exposant qui trivialise, celui que donne le calcul $(L^4)^3 \simeq \mathcal O$, mais pas le meilleur ; c'est la même situation que pour $n = 4$, où la page~72 trouvait $L^{\otimes 6} \simeq 1$ quand l'ordre est $3$.

\begin{sloppypar}
\noindent Vérifié au niveau des cocycles (\texttt{cL\_pow\_four}, \texttt{coboundary\_cL\_iff}, \texttt{c5\_pow\_twelve}, \texttt{coboundary\_c5\_iff}). Lean manipule les mots en $s_1, \ldots, s_4$ : la substitution d'un mot est la composée, son facteur est donné par la règle de cocycle (\texttt{wAct}, \texttt{wCoc}), et l'énoncé \q{pour tout élément du groupe} devient \q{pour tout mot}. Que les mots passent au groupe, c'est-à-dire que substitutions et facteurs vérifient les relations de Coxeter de $\mathfrak S_5$, est démontré plus bas (énoncé \q{relations de Coxeter}, après la colonne $n = 6$). N'est pas démontrée en Lean la dérivation des facteurs $c_L$, $c_5$ à partir des homographies, faite ci-dessus.
\end{sloppypar}

Passons à la colonne $n = 6$, où la page porte \q{$20\,?$} pour $L$ et \q{$60\,?$} pour $L_i$.

\noindent\emph{Le modèle.} On envoie encore les trois premiers points en $0$, $1$, $\infty$ ; il reste trois coordonnées $(\lambda, \mu, \nu)$, hors de $\{0, 1\}$ et deux à deux distinctes. Les cinq transpositions $s_1, \ldots, s_5$ agissent comme pour $n = 5$, la troisième coordonnée suivant la deuxième :
\[
s_1 : (1 - \lambda,\ 1 - \mu,\ 1 - \nu), \qquad s_2 : \Bigl(\frac{\lambda}{\lambda - 1},\ \frac{\mu}{\mu - 1},\ \frac{\nu}{\nu - 1}\Bigr),
\]
\[
s_3 : \Bigl(1 - \lambda,\ \frac{\mu(\lambda - 1)}{\lambda - \mu},\ \frac{\nu(\lambda - 1)}{\lambda - \nu}\Bigr), \qquad s_4 : (\mu, \lambda, \nu), \qquad s_5 : (\lambda, \nu, \mu).
\] Le facteur sur $L_6$ est la dérivée de l'homographie au sixième point, pour le groupe $\mathfrak S_5$ engendré par $s_1, \ldots, s_4$ ; le facteur sur $L$ est le produit des six dérivées. On trouve, pour $s_1, \ldots, s_5$ et $s_1, \ldots, s_4$ :
\[
c_L = 1,\ \ \frac{1}{(\lambda - 1)^2(\mu - 1)^2(\nu - 1)^2},\ \ \frac{\lambda^2(\lambda - 1)^2}{(\lambda - \mu)^2(\lambda - \nu)^2},\ \ 1,\ \ 1 ;
\]
\[
c_6 = -1,\ \ \frac{-1}{(\nu - 1)^2},\ \ \frac{\lambda(\lambda - 1)}{(\lambda - \nu)^2},\ \ 1.
\]

\noindent\emph{Le calcul.} Les unités de $M_{0,6}$ sont, à une constante près, les monômes en neuf facteurs : $\lambda$, $\mu$, $\nu$, $1 - \lambda$, $1 - \mu$, $1 - \nu$, $\lambda - \mu$, $\lambda - \nu$, $\mu - \nu$. Chaque générateur envoie chacun d'eux sur un monôme, au signe près ; par exemple $s_2$ envoie $\lambda - \mu$ sur $(\mu - \lambda)/((\lambda - 1)(\mu - 1))$. Chercher $h$ revient donc encore à un système linéaire en neuf inconnues entières, plus une condition de signe. Un programme d'algèbre linéaire exacte sur $\mathbf Z$ le résout. Pour $L$, la solution est simple : $c_L^5$ est le cobord du carré du produit des neuf unités. Pour $L_6$, le système a une solution dès $m = 10$, avec
\[
g = \frac{\nu^4 (1 - \nu)^4 (\lambda - \nu)^4 (\mu - \nu)^4}{\lambda\mu(1 - \lambda)(1 - \mu)(\lambda - \mu)},
\]
mais le signe ne suit pas : $c_6(s)^{10} = -g(sx)/g(x)$ pour chacun des quatre générateurs. Une constante ne corrige pas ce signe, puisqu'elle disparaît du quotient $h(sx)/h(x)$. Il faut donc passer à $m = 20$, où $c_6^{20}$ est le cobord de $g^2$.

\noindent\emph{Les points fixes.} Pour minorer, on cherche comme pour $n = 5$ des points fixés par un élément d'ordre $5$ et par un élément d'ordre $4$. Le $5$-cycle $s_1 s_2 s_3 s_4$ correspond à une homographie $\psi$ d'ordre $5$ qui envoie $0 \mapsto 1 \mapsto \infty \mapsto \lambda \mapsto \mu \mapsto 0$ et fixe $\nu$. Une telle homographie est conjuguée à la rotation $z \mapsto \omega z$, où $\omega$ est une racine primitive cinquième de l'unité ; la configuration est celle de $0$ et des cinq racines cinquièmes de l'unité, à une homographie près. Dans nos coordonnées, avec $\omega^4 + \omega^3 + \omega^2 + \omega + 1 = 0$, c'est le point
\[
(\lambda, \mu, \nu) = (\omega^2 + \omega^3,\ 1 + \omega^2 + \omega^3,\ -\omega^4).
\]
Le facteur de $L_6$ y est la dérivée $\psi'(\nu)$, qui vaut $\omega$. Celui de $L$ aussi : les cinq autres points forment un seul cycle, et le produit des dérivées le long de ce cycle est la dérivée de $\psi^5 = \mathrm{id}$, soit $1$. Les coordonnées de ce point et les dénominateurs rencontrés en chemin sont des unités de $\mathbf Z[\omega]$ : il n'y faut aucune hypothèse sur le corps. Seule la conclusion $\omega^m = 1 \Rightarrow 5 \mid m$ demande que $5$ soit inversible. Le $4$-cycle $s_1 s_2 s_3$ correspond, comme pour $n = 5$, à $z \mapsto (z + 1)/(1 - z)$, qui fixe $i$ et $-i$ ; il fixe donc le point $(-1, -i, i)$. Le facteur de $L_6$ y vaut $i$. Celui de $L$ vaut $i \cdot (-i) = 1$, car les dérivées aux deux points fixes se compensent.

\begin{contrexemple}[page 70, colonne $n = 6$, pour $L$ : le \q{$20\,?$} n'est pas le meilleur exposant\piste{146-equivariant-trivialising-exponents}]\label{ce:146-cinq}
Soit $K$ un corps où $5$ est inversible et qui contient une racine $\omega$ de $\omega^4 + \omega^3 + \omega^2 + \omega + 1$. La puissance $m$-ième du cocycle $c_L$ de $L$ sous $\mathfrak S_6$ est le cobord d'une fonction sans zéro sur $M_{0,6}(K)$ si et seulement si $5 \mid m$. Pour $m = 5$ on peut prendre
\[
h = \bigl(\lambda\mu\nu(1 - \lambda)(1 - \mu)(1 - \nu)(\lambda - \mu)(\lambda - \nu)(\mu - \nu)\bigr)^2.
\]
Le meilleur exposant pour $L$ est donc $5$, et non $20$.
\end{contrexemple}

\begin{proof}
Sur les générateurs, $c_L(s)^5 = h(sx)/h(x)$ se vérifie directement. Par exemple pour $s_2$, le produit $H$ des neuf unités vérifie $H(s_2 x)/H(x) = \pm 1/((\lambda - 1)(\mu - 1)(\nu - 1))^5$ : pour $x = \lambda$, le facteur $\lambda - 1$ vient de l'image de $\lambda$, de celle de $1 - \lambda$, des images des deux différences où $\lambda$ figure, et du facteur $1 - \lambda$ de $H(x)$. Au carré, on trouve $c_L(s_2)^5$. Les mots en suivent par la règle de cocycle. Au point fixé par $s_1 s_2 s_3 s_4$, le second membre vaut $1$ et le cocycle vaut $\omega$, d'où $\omega^m = 1$ et $5 \mid m$.
\end{proof}

\begin{contrexemple}[page 70, colonne $n = 6$, pour $L_i$ : le \q{$60\,?$} n'est pas le meilleur exposant\piste{146-equivariant-trivialising-exponents}]\label{ce:146-vingt}
Soit $K$ un corps où $2$ et $5$ sont inversibles, qui contient $i$ avec $i^2 = -1$ et une racine $\omega$ de $\omega^4 + \omega^3 + \omega^2 + \omega + 1$. La puissance $m$-ième du cocycle $c_6$ de $L_6$ sous $\mathfrak S_5$ est le cobord d'une fonction sans zéro sur $M_{0,6}(K)$ si et seulement si $20 \mid m$. Pour $m = 20$ on peut prendre $h = g^2$, avec $g$ ci-dessus. Le meilleur exposant pour $L_i$ est donc $20$, et non $60$.
\end{contrexemple}

\begin{proof}
Sur les générateurs, $c_6(s)^{10} = -g(sx)/g(x)$, d'où $c_6(s)^{20} = g(sx)^2/g(x)^2$, et les mots en suivent. Au point fixé par $s_1 s_2 s_3 s_4$, le cocycle vaut $\omega$, d'où $5 \mid m$ ; au point $(-1, -i, i)$, fixé par $s_1 s_2 s_3$, il vaut $i$, d'où $4 \mid m$.
\end{proof}

Les deux valeurs de la page sont des exposants qui trivialisent, puisque $5 \mid 20$ et $20 \mid 60$, mais aucune n'est la plus petite. L'ordre $3$, que suggère le $60 = 3 \cdot 20$ de la page, n'apparaît pas : comme $c_6^{20}$ est un cobord, le facteur $f$ en un point fixé par un $3$-cycle vérifie $f^{20} = 1$ et $f^3 = 1$, donc $f = 1$. Sur les trois colonnes, $L$ est d'ordre $n - 1$ et $L_i$ d'ordre $(n - 1)(n - 2)$, le nombre de la première ligne du tableau.\footnote{Le groupe lui-même est connu : $H^1(\mathfrak S_n, \mathcal O(M_{0,n})^*) = \mathrm{Pic}\,[M_{0,n}/\mathfrak S_n]$ est cyclique d'ordre $2(n - 1)$ pour $n$ pair en caractéristique ne divisant pas $n$ (Gorchinskiy--Viviani \cite[th.~3.6]{gorchinskiyviviani2008} ; Arsie--Vistoli \cite[th.~5.1]{arsievistoli2004} calculent le groupe de Picard du champ des courbes hyperelliptiques, dont celui-ci est un sous-groupe d'indice $1$ ou $2$) ; les ordres de $L$ et des $L_i$ en découlent, mais ne sont énoncés pour ces fibrés dans aucun texte trouvé.}

\begin{sloppypar}
\noindent Vérifié au niveau des cocycles (\texttt{act6\_U6}, \texttt{cL6\_pow\_five}, \texttt{c6\_pow\_ten}, \texttt{fix\_five}, \texttt{fix\_four6}, \texttt{coboundary\_cL6\_iff}, \texttt{coboundary\_c6\_iff}), avec les mots en $s_1, \ldots, s_5$ comme pour $n = 5$ (\texttt{wAct}, \texttt{wCoc}). Les relations de Coxeter de $\mathfrak S_6$ pour ces substitutions et ces facteurs sont démontrées ci-dessous (énoncé \q{relations de Coxeter}). Ne sont pas démontrées en Lean la dérivation des facteurs à partir des homographies, et la résolution du système linéaire, dont Lean ne vérifie que la solution.
\end{sloppypar}

\noindent\emph{Les relations de Coxeter.} Les substitutions et les facteurs n'ont été donnés que sur les transpositions adjacentes, et les énoncés ci-dessus portent sur les mots. Pour qu'ils portent sur le groupe, il faut que deux mots qui représentent la même permutation aient même substitution et même facteur, c'est-à-dire que les générateurs vérifient les relations de Coxeter.

\begin{encadre}
\begin{enonce}[De l'édition : relations de Coxeter\piste{146-equivariant-trivialising-exponents}]
Sur tout corps $K$, les quatre familles de générateurs ci-dessus --- $s_1, \ldots, s_4$ avec $c_L$ et $s_1, s_2, s_3$ avec $c_5$ sur $M_{0,5}(K)$, $s_1, \ldots, s_5$ avec $c_L$ et $s_1, \ldots, s_4$ avec $c_6$ sur $M_{0,6}(K)$ --- vérifient les relations de Coxeter de type $A$ :
\[
s_i^2 = 1, \qquad s_i s_j s_i = s_j s_i s_j \ (|i - j| = 1), \qquad s_i s_j = s_j s_i \ (|i - j| \geq 2),
\]
pour la substitution et pour le facteur composé par la règle de cocycle. Les applications $(x, t) \mapsto (s_i x, c(s_i)(x)\, t)$ du fibré trivial $M_{0,n}(K) \times K$ définissent donc une action du groupe de Coxeter de type $A_{n-1}$, et la substitution et le facteur d'un mot ne dépendent que de son image dans ce groupe.
\end{enonce}
\end{encadre}

\begin{proof}
Chaque relation est une identité entre fractions rationnelles, à vérifier sur $M_{0,n}(K)$. Le calcul direct bute sur les dénominateurs emboîtés : dans $s_3 s_3$, par exemple, apparaît $1/\bigl((1 - \lambda) - \mu(\lambda - 1)/(\lambda - \mu)\bigr)$, dont il faut savoir qu'il ne s'annule pas. On nomme donc les points intermédiaires : pour $s_i s_j s_i = s_j s_i s_j$, on pose $q = s_i x$, $r = s_j q$, $q' = s_j x$, $r' = s_i q'$, qui sont dans $M_{0,n}(K)$ puisque les substitutions le préservent. L'identité, écrite en $r$ et $r'$, n'a pour dénominateurs que leurs coordonnées et leurs différences, non nulles ; on les chasse, on remplace $r$ et $r'$ par leurs expressions en $q$ et $q'$, on chasse de nouveau, puis on descend à $x$, où il reste une identité polynomiale. Les relations entraînent $(s_i s_j)^3 = 1$ et $(s_i s_j)^2 = 1$ dans le monoïde des applications du fibré, ce qui est la présentation du groupe de Coxeter de type $A_{n-1}$. Que ce groupe soit $\mathfrak S_n$ est classique.
\end{proof}

\begin{sloppypar}
\noindent Vérifié dans \href{\leanblob/Folder146.lean}{\texttt{Folder146.\allowbreak{}lean}} : \texttt{CoxRel} pour les relations sur les générateurs, \texttt{coxRel\_cL}, \texttt{coxRel\_c5}, \texttt{coxRel\_cL6}, \texttt{coxRel\_c6} pour les quatre familles, \texttt{CoxRel.isLiftable} et \texttt{CoxRel.lift} pour l'action du groupe de Coxeter (par \texttt{CoxeterSystem.lift} de Mathlib), \texttt{CoxRel.lift\_word} et \texttt{CoxRel.wAct\_eq} pour le passage des mots au groupe. Mathlib n'identifie pas le groupe de Coxeter de type $A_{n-1}$ à $\mathfrak S_n$ ; ce dernier pas n'est pas formalisé.
\end{sloppypar}

Le tableau~\ref{tab:146-exposants} met en regard les valeurs de la page et les ordres calculés.

\begin{table}[htbp]
\centering\small
\begin{tabular}{@{}lccc@{}}
\toprule
& $n = 4$ & $n = 5$ & $n = 6$ \\
\midrule
$L$, page~70 & $3$ & $12\,?$ & $20\,?$ \\
$L$, ordre calculé, $n - 1$ & $3$ & $\mathbf 4$ & $\mathbf 5$ \\
\addlinespace
$L_i$, page~70 & $6$ & $12\,?$ & $60\,?$ \\
$L_i$, ordre calculé, $(n - 1)(n - 2)$ & $6$ & $12$ & $\mathbf{20}$ \\
\midrule
statut & Lean & Lean & Lean \\
& th.~\ref{thm:146-six}, \ref{thm:146-trois} & th.~\ref{thm:146-douze}, c.-ex.~\ref{ce:146-quatre} & c.-ex.~\ref{ce:146-cinq}, \ref{ce:146-vingt} \\
\bottomrule
\end{tabular}
\caption{Le tableau de la page~70 et les ordres calculés. En gras, les valeurs qui diffèrent de celles de la page ; les points d'interrogation sont ceux du manuscrit.}
\label{tab:146-exposants}
\end{table}

\subsection*{Tous les $n$}

Les trois colonnes suggèrent une règle : $n - 1$ pour $L$ et $(n - 1)(n - 2)$ pour $L_i$. Elle se démontre pour tout $n$, à condition de changer de modèle. Les coordonnées normalisées des colonnes précédentes, où trois points sont envoyés en $0$, $1$ et $\infty$, obligent à écrire une homographie de renormalisation par permutation, et leur forme dépend de $n$. Le modèle homogène évite cette étape.

Un point de $\mathbb P^1(K)$ est un vecteur non nul $v = (v_1, v_2)$ de $K^2$, à un scalaire près. Deux vecteurs donnent le même point si et seulement si leur crochet $[v\,w] = v_1 w_2 - v_2 w_1$ est nul. Une configuration de $n$ points distincts est donc une famille $v_1, \ldots, v_n$ de vecteurs dont tous les crochets $[v_i\,v_j]$, $i \neq j$, sont non nuls. Une fonction sur $M_{0,n}(K)$ est une fonction de la configuration invariante par $\mathrm{GL}_2(K)$ et par le changement de chaque $v_i$ en un multiple. La droite tangente à $\mathbb P^1$ au point $\langle v\rangle$ est $\mathrm{Hom}(\langle v\rangle, K^2/\langle v\rangle)$, isomorphe à $\langle v\rangle^{\otimes -2} \otimes \det K^2$. Une section partout non nulle de $L_i^{\otimes m}$ devient ainsi, quitte à l'inverser, une fonction sans zéro qui est multipliée par $t^{2m}$ quand $v_i$ est multiplié par $t$, qui ne change pas quand on multiplie les autres vecteurs, et qui est multipliée par $\det(g)^m$ sous $g \in \mathrm{GL}_2(K)$. Pour $L = L_1 \otimes \cdots \otimes L_n$, les poids sont $t_i^{2m}$ pour chaque vecteur et $\det(g)^{mn}$. Trivialiser $L^{\otimes m}$ de façon compatible au groupe symétrique, c'est trouver une telle fonction invariante par toute renumérotation des points ; pour $L_n$, invariante par les renumérotations qui fixent le $n$-ième point. Comme dans les colonnes précédentes, la fonction n'est pas supposée régulière.

\begin{encadre}
\begin{theoreme}[énoncé de l'édition, d'après le tableau de la page 70\piste{146-equivariant-trivialising-exponents}]\label{thm:146-general}
Soit $n \geq 3$ et soit $K$ un corps qui contient une racine primitive $(n - 1)$-ième de l'unité $\omega$ et une racine primitive $(n - 2)$-ième de l'unité $\zeta$. Dans le modèle homogène :
\begin{enumerate}
\item $L^{\otimes m}$ se trivialise de façon compatible à $\mathfrak S_n$ si et seulement si $n - 1$ divise $m$ (pour cette partie, $n \geq 2$ et seule $\omega$ sert) ;
\item $L_n^{\otimes m}$ se trivialise de façon compatible au stabilisateur $\mathfrak S_{n-1}$ du $n$-ième point si et seulement si $(n - 1)(n - 2)$ divise $m$.
\end{enumerate}
Les fonctions qui trivialisent existent sur tout corps.
\end{theoreme}
\end{encadre}

Pour $n = 4$, $5$ et $6$ on retrouve $3$, $4$, $5$ et $6$, $12$, $20$, les ordres trouvés plus haut dans les coordonnées normalisées.

\begin{proof}
Les fonctions qui trivialisent sont des produits de crochets. Soit $D$ le produit des crochets $[v_i\,v_j]$ sur les couples ordonnés $i \neq j$ ; c'est, au signe près, le carré du produit de Vandermonde $\prod_{i < j}[v_i\,v_j]$, et le carré efface le signe que fait apparaître une permutation. Chaque indice figure dans $2(n - 1)$ facteurs : multiplier $v_i$ par $t_i$ multiplie $D$ par $t_i^{2(n-1)}$, et $g$ le multiplie par $\det(g)^{n(n-1)}$, car $[g v\,g w] = \det(g)\,[v\,w]$. Ce sont les poids de $L^{\otimes (n-1)}$ : $D$ trivialise $L^{\otimes(n-1)}$. Pour $L_n$, notons $p$ le $n$-ième point et $v_1, \ldots, v_k$ les $k = n - 1$ autres, et posons
\[
F = \frac{\bigl(\prod_i [v_i\,p]\bigr)^{2(k-1)}}{D(v_1, \ldots, v_k)}.
\]
Chaque $v_i$ figure $2(k - 1)$ fois au numérateur et $2(k - 1)$ fois au dénominateur, donc son poids est nul ; $p$ a le poids $2k(k - 1)$, et $\det(g)$ l'exposant $2k(k - 1) - k(k - 1) = k(k - 1)$. Ce sont les poids de $L_n^{\otimes k(k-1)}$, avec $k(k - 1) = (n - 1)(n - 2)$. Pour $n = 5$, avec $p = \mu$ et les autres points en $0$, $1$, $\infty$, $\lambda$, on reconnaît en coordonnées affines, au signe près, la fonction $\mu^6(1 - \mu)^6(\lambda - \mu)^6/(\lambda^2(1 - \lambda)^2)$ du théorème~\ref{thm:146-douze}.

Pour la minoration, on cherche des configurations qu'une renumérotation $\sigma$ envoie sur leur image par une matrice $g$ (figure~\ref{fig:146-rotations}). Si $F$ trivialise, $F(v) = F(v \circ \sigma) = F(g v)$, qui vaut $F(v)$ multiplié par le poids de $g$, et ce poids vaut donc $1$. Pour $L$, on prend le point $0$ et les $n - 1$ racines $(n-1)$-ièmes de l'unité, que la matrice $g = \mathrm{diag}(\omega, 1)$, de déterminant $\omega$, fait tourner ; on obtient $\omega^{mn} = 1$, donc $n - 1$ divise $mn$, et comme $n \equiv 1$ modulo $n - 1$, il divise $m$. Pour $L_n$, le $n$-ième point est en $0$. La même configuration donne $\omega^m = 1$, d'où $n - 1 \mid m$. La configuration formée de $0$, de $\infty$ et des racines $(n-2)$-ièmes de l'unité, que $\mathrm{diag}(\zeta, 1)$ fait tourner en fixant $0$ et $\infty$, donne $\zeta^m = 1$, d'où $n - 2 \mid m$. Le vecteur $(1, 0)$ de $\infty$ y est multiplié par $\zeta$, ce qui ne compte pas, car $F$ ne voit pas les multiples des autres points. Comme $n - 1$ et $n - 2$ sont premiers entre eux, leur produit divise $m$.
\end{proof}

\begin{figure}[htbp]
\centering
\begin{tikzpicture}[x=1.45cm, y=1.45cm, >=stealth, every node/.style={font=\small}]
% {0} U mu_5, tournée par z -> omega z
\draw[black!35] (0,0) circle (1);
\foreach \k/\l in {0/1, 1/\omega, 2/\omega^2, 3/\omega^3, 4/\omega^4} { \fill (\k*72:1) circle (2pt); \node at (\k*72:1.28) {$\l$}; }
\fill[piste] (0,0) circle (2.3pt); \node[piste, below=2pt] at (0,0) {$0$};
\draw[->, piste, thick] (0,0) -- (0:0.62) node[right=-1pt] {\footnotesize $v$};
\draw[->, piste, thick, dashed] (0,0) -- (72:0.62) node[above right=-2pt] {\footnotesize $\omega v$};
\draw[->, frise] (8:0.3) arc (8:64:0.3);
\node[align=center] at (0,-1.75) {$\{0\} \cup \mu_5$, tournée par $z \mapsto \omega z$ \\ \footnotesize ($L$, et $L_n$ avec le $n$-ième point en $0$)};
% {0, infini} U mu_4, tournée par z -> zeta z
\begin{scope}[xshift=6.6cm]
\draw[black!35] (0,0) circle (1);
\foreach \k/\l in {0/1, 1/\zeta, 2/\zeta^2, 3/\zeta^3} { \fill (\k*90:1) circle (2pt); \node at (\k*90:1.27) {$\l$}; }
\fill[piste] (0,0) circle (2.3pt); \node[piste, below=2pt] at (0,0) {$0$};
\draw[->, piste, thick] (0,0) -- (0:0.62) node[right=-1pt] {\footnotesize $v$};
\draw[->, piste, thick, dashed] (0,0) -- (90:0.62) node[right=-1pt] {\footnotesize $\zeta v$};
\draw[->, frise] (8:0.3) arc (8:82:0.3);
\fill (1.25,1.15) circle (2pt); \node[right] at (1.25,1.15) {$\infty$, fixe};
\node[align=center] at (0,-1.75) {$\{0, \infty\} \cup \mu_4$, tournée par $z \mapsto \zeta z$ \\ \footnotesize ($L_n$, le $n$-ième point en $0$)};
\end{scope}
\end{tikzpicture}
\caption{Les deux configurations de la minoration, pour $n = 6$. À gauche, $0$ et les $n - 1 = 5$ racines cinquièmes de l'unité ; la matrice $\mathrm{diag}(\omega, 1)$ les fait tourner, ce qui revient à les renuméroter, et fixe $0$. À droite, $0$, $\infty$ et les $n - 2 = 4$ racines quatrièmes de l'unité, que $\mathrm{diag}(\zeta, 1)$ fait tourner en fixant $0$ et $\infty$. Le point $0$, qui porte $L_n$, est fixe, mais son vecteur tangent $v$ tourne avec la figure et devient $\omega v$, ou $\zeta v$ ; une trivialisation compatible à la renumérotation doit donner la même valeur aux deux, et le poids $\det(g)^m$ de la matrice doit valoir~$1$ : $\omega^m = 1$ à gauche, $\zeta^m = 1$ à droite, d'où $5 \mid m$ et $4 \mid m$, donc $20 \mid m$ pour $L_6$.}
\label{fig:146-rotations}
\end{figure}

\begin{sloppypar}
\noindent Vérifié (\texttt{br}, \texttt{Conf}, \texttt{disc}, \texttt{TrivL}, \texttt{TrivLi}, \texttt{disc\_smul}, \texttt{disc\_lin}, \texttt{disc\_perm}, \texttt{trivL\_of\_dvd}, \texttt{trivLi\_of\_dvd}, \texttt{dvd\_of\_trivL}, \texttt{dvd\_of\_trivLi}, \texttt{trivL\_iff}, \texttt{trivLi\_iff}). Ne sont pas démontrés en Lean : le dictionnaire entre fibrés en droites équivariants sur $M_{0,n}$ et fonctions de poids sur les configurations, et le fait que le groupe de Picard équivariant soit le $H^1$ des unités. Mathlib n'a pas les espaces de modules $M_{0,n}$.
\end{sloppypar}

Pour $n$ pair, ces ordres sont dans la littérature. Edidin et Hu, partant de la description de Pernice \cite{pernice2022}, qu'ils présentent par un sous-groupe de Borel, décrivent $[M_{0,2g+2}/\mathfrak S_{2g+1}]$ comme le champ des formes binaires de degré $2g+2$ munies d'une racine marquée, et calculent son anneau de Chow entier sur un corps algébriquement clos de caractéristique ne divisant pas $2g+2$ : $\mathbf Z[l]/(2g(2g+1)\,l)$ pour $g \geqslant 2$ \cite[théorème~1.3]{edidinhu2025}. Le groupe de Picard est donc cyclique d'ordre $(n-1)(n-2)$ pour $n = 2g+2 \geqslant 6$. Leur générateur $l$ est la classe d'un caractère d'un tore ; comme $L_n$ y est d'ordre $(n-1)(n-2)$, il engendre aussi ce groupe, ce qu'ils n'énoncent pas. Pour $n = 4$, $M_{1,1}$ est une gerbe en $\mu_2$ au-dessus de $[M_{0,4}/\mathfrak S_3]$, et $\operatorname{Pic}(M_{1,1}) = \mathbf Z/12$ \cite{mumford1965,fultonolsson2010} donne l'ordre~$6$. Pour $n$ impair, en particulier pour la colonne $n = 5$ de la page, aucun énoncé imprimé n'a été trouvé, et D.~Edidin confirme que leur article ne traite que le cas pair et qu'il ne connaît pas de référence pour le cas impair~\cite{edidin2026}. Un argument par tranches donne pourtant le même ordre pour tout $n$, en caractéristique~$0$ : on place le $n$-ième point à l'infini, ce qui laisse le groupe affine agir sur les polynômes unitaires sans racine multiple de degré $m = n-1$ ; on impose ensuite aux racines d'être de somme nulle, et il reste $\mathbb G_m$, de poids $2, \ldots, m$ sur les coefficients. Le discriminant, irréductible et de poids $m(m-1)$, donne $\operatorname{Pic}[M_{0,n}/\mathfrak S_{n-1}] \cong \mathbf Z/(n-1)(n-2)$, engendré par la droite tangente au point à l'infini~\cite{mo516243}. Le théorème~70.7 en est la contrepartie dans le modèle homogène, le seul que Lean vérifie.

\subsection*{Les deux modèles s'accordent}

Les colonnes $n = 4$, $5$, $6$ ont été traitées par des cocycles en coordonnées normalisées, la règle générale par des fonctions de poids sur des configurations. Les deux calculs donnent les mêmes ordres, mais rien ne disait encore qu'ils parlent du même objet. On le vérifie ici en restreignant le modèle homogène aux configurations normalisées.

\noindent\emph{Restreindre.} Pour $n = 5$, la configuration normalisée de $(\lambda, \mu)$ est la famille de vecteurs
\[
(0, 1),\ (1, 1),\ (1, 0),\ (\lambda, 1),\ (\mu, 1),
\]
qui représente les points $0$, $1$, $\infty$, $\lambda$, $\mu$. Une fonction $F$ de poids, qui trivialise $L^{\otimes m}$ dans le modèle homogène, donne par restriction une fonction sans zéro sur $M_{0,5}(K)$,
\[
h(\lambda, \mu) = F\bigl((0,1), (1,1), (1,0), (\lambda,1), (\mu,1)\bigr).
\]
 La question est de savoir comment $h$ change sous les générateurs $s_1, \ldots, s_4$.

\noindent\emph{Un générateur.} Prenons $s_3$, qui échange les étiquettes de $\infty$ et de $\lambda$. Après échange, les trois premiers points sont $0$, $1$, $\lambda$, et la substitution de renormalisation est l'homographie $g(z) = (1 - \lambda)z/(z - \lambda)$, qui les envoie sur $0$, $1$, $\infty$ ; elle envoie le nouveau quatrième point, $\infty$, sur $1 - \lambda$, et $\mu$ sur $\mu(\lambda - 1)/(\lambda - \mu)$. C'est la substitution $s_3$ de la colonne $n = 5$. En vecteurs, $g$ est la matrice $\begin{pmatrix} 1 - \lambda & 0 \\ 1 & -\lambda \end{pmatrix}$, de déterminant $\lambda(\lambda - 1)$, et elle envoie chaque vecteur de la configuration renumérotée sur un multiple du vecteur normalisé correspondant : $(0, 1) \mapsto (0, -\lambda)$, $(1, 1) \mapsto (1 - \lambda)(1, 1)$, $(\lambda, 1) \mapsto \lambda(1 - \lambda)(1, 0)$, $(1, 0) \mapsto (1 - \lambda, 1)$ et $(\mu, 1) \mapsto (\mu - \lambda)\bigl(\mu(1 - \lambda)/(\mu - \lambda), 1\bigr)$. Les poids de $F$ donnent
\[
h(s_3(\lambda, \mu)) = \Bigl(\bigl(\textstyle\prod_i t_i\bigr)^2 \det(g)^5\Bigr)^m\, h(\lambda, \mu),
\qquad \prod_i t_i = \frac{-1}{\lambda^2(1-\lambda)^2(\mu - \lambda)},
\]
où les $t_i$ sont les inverses des multiples ci-dessus, et l'invariance de $F$ par renumérotation absorbe l'échange. Le facteur vaut $\lambda(\lambda - 1)/(\lambda - \mu)^2$ : c'est exactement le facteur de $s_3$ sur $L$ dans la colonne $n = 5$. Les autres générateurs se traitent de même, avec des matrices plus simples. Pour $L_5$, seul le cinquième vecteur porte un poids, et le facteur devient $t_5^2 \det(g)$, qui redonne le cocycle de $L_5$.

\begin{encadre}
\begin{enonce}[De l'édition : accord des deux modèles\piste{146-equivariant-trivialising-exponents}]
Pour $n = 4$, $5$, $6$, sur tout corps $K$, une trivialisation de $L^{\otimes m}$ (resp.\ de $L_n^{\otimes m}$ sous le stabiliseur du $n$-ième point) dans le modèle homogène se restreint aux configurations normalisées en une fonction sans zéro $h$ dont le cobord est la puissance $m$-ième du cocycle des coordonnées normalisées : $\mathrm{sgn}\,g \cdot g'(\lambda)$ et $g'(\lambda)$ pour $n = 4$, les cocycles de $L$ et de $L_5$ pour $n = 5$, ceux de $L$ et de $L_6$ pour $n = 6$. Sous les hypothèses sur $K$ des colonnes, les deux conditions sont équivalentes.
\end{enonce}
\end{encadre}

\begin{proof}
Pour chaque générateur, on écrit la matrice de renormalisation et les multiples, comme pour $s_3$ ci-dessus, et l'on vérifie que $(\prod_i t_i)^2 \det(g)^n$, resp.\ $t_n^2\det(g)$, est le facteur du cocycle ; pour $n = 4$, on le fait pour les six éléments de $\mathfrak S_3$. La relation de cobord passe des générateurs aux mots par la règle de cocycle. Pour la réciproque, une puissance $m$-ième du cocycle qui est un cobord force $m$ à être multiple de l'ordre calculé dans la colonne, et la fonction de poids de l'énoncé général trivialise alors $L^{\otimes m}$ ou $L_n^{\otimes m}$.
\end{proof}

La réciproque passe donc par les nombres, non par la construction : on ne prolonge pas $h$ en une fonction de poids sur toutes les configurations. Le sens direct suffit à relier les deux calculs : toute trivialisation du modèle homogène en donne une des cocycles normalisés, par simple restriction.

\begin{sloppypar}
\noindent Vérifié dans \href{\leanblob/Folder146.lean}{\texttt{Folder146.\allowbreak{}lean}} : \texttt{trivL\_step} et \texttt{trivLi\_step} pour le changement d'une fonction de poids sous une renormalisation, \texttt{cob\_of\_trivL} et \texttt{cob\_of\_trivLi} pour la restriction, \texttt{step4}, \texttt{step5}, \texttt{step5i}, \texttt{step6} et \texttt{step6i} pour les matrices et les multiples, \texttt{coboundary\_derL\_of\_trivL}, \texttt{coboundary\_der\_of\_trivLi}, \texttt{coboundary\_cL\_of\_trivL}, \texttt{coboundary\_c5\_of\_trivLi}, \texttt{coboundary\_cL6\_of\_trivL} et \texttt{coboundary\_c6\_of\_trivLi} pour le sens direct, et \texttt{trivL\_four\_iff}, \texttt{trivLi\_four\_iff}, \texttt{trivL\_five\_iff}, \texttt{trivLi\_five\_iff}, \texttt{trivL\_six\_iff}, \texttt{trivLi\_six\_iff} pour l'équivalence. Le dictionnaire avec les fibrés équivariants reste hors de portée.
\end{sloppypar}
\section[Cote 140-1 : le groupe $H^1(U_{0,3}, \mathfrak S_3; \mathbf G_m)$]{Cote 140-1 : le groupe $H^1(U_{0,3}, \mathfrak S_3; \mathbf G_m)$\protect\verifie{Folder140_1}}\label{sec:140-1}

La cote 140-1, brouillon de la \emph{Longue Marche}, trente-six pages que l'inventaire date \q{[à partir de 1978-à partir de 1982]}, encadre page~22 un lemme : pour $S$ régulier intègre, $\mathrm{Pic}(S) = 0$, de caractéristique générique $\neq 2$, le groupe $H^1(U_{0,3}, \mathfrak S_3; \mathbf G_m)$ des $\mathbf G_m$-torseurs $\mathfrak S_3$-équivariants sur $U_{0,3} = \mathbf P^1 - \{0, 1, \infty\}$ est $\mathbf Z/6$, engendré par $\mathcal O(1)$, et $\mathbf Z/3$ en caractéristique générique~$2$ (\lot{140-1}{2}{22}). Une note marginale le majore par deux suites exactes : $H^1$ équivariant $= H^1(\mathfrak S_3, \mathcal O(U_{0,3})^*)$, et $0 \to \mathcal O(S)^* \to \mathcal O(U_{0,3})^* \to V(J) \to 0$, où $V(J) = \mathrm{Ker}(\mathbf Z^J \to \mathbf Z)$ est le groupe des diviseurs des unités, $J$ l'ensemble des trois points retirés. Les calculs de $H^1(\mathfrak S_3, \cdot)$ qui concluent ne sont pas sur la page ; la lecture les ajoute.

\noindent\emph{Conventions.} $H^1$ est la cohomologie des groupes de mathlib, $H^1(G, M)$ pour la représentation de $G$ sur un groupe abélien $M$ ; Lean l'identifie aux cocycles modulo les cobords. Le groupe $\mathcal O(S)^*$ est remplacé par les unités $k^*$ d'un anneau intègre, avec l'action triviale.

\begin{theoreme}[énoncé de l'édition, d'après la note marginale de la page 22]\label{thm:140-1-majoration}
On a $H^1(\mathfrak S_3, V(J)) \simeq \mathbf Z/3$ et $H^1(\mathfrak S_3, k^*) \simeq \mu_2(k)$. Pour toute extension de $\mathfrak S_3$-modules $0 \to k^* \to M \to V(J) \to 0$, l'ordre de $H^1(\mathfrak S_3, M)$ divise~$6$, et divise~$3$ si $2 = 0$ dans~$k$.
\end{theoreme}

\noindent Vérifié tel quel (\texttt{H1\_VJ}, \texttt{card\_H1\_VJ}, \texttt{card\_H1\_triv}, \texttt{card\_mu2\_dvd}, \texttt{card\_H1\_dvd}). La classe d'un cocycle $f$ à valeurs dans $V(J)$ est $\sum_j m_j \bmod 3$, où $m_j = -f(\tau_j)_j$, $\tau_j$ la transposition de $0$ et~$j$ : c'est la forme explicite de $H^1(\mathfrak S_3, \mathbf Z^J) = 0$ et du bord $\mathbf Z \to H^1(\mathfrak S_3, V(J))$.

La majoration ne dit pas encore que le groupe vaut $\mathbf Z/6$ : il faut une classe d'ordre exactement~$6$. La page~24 la cherche du côté de $\mathcal O(1)$. On en prend ici une autre, plus facile à manier, la classe du fibré tangent, et l'on travaille dans un modèle explicite des unités.

\noindent\emph{Le modèle.} Sur un corps $k$, les unités de $U_{0,3} = \mathrm{Spec}\, k[\lambda, 1/\lambda, 1/(1-\lambda)]$ sont les $c\,\lambda^a(1-\lambda)^b$, $c \in k^*$, $a, b \in \mathbf Z$. On les code par le couple $(c, v)$, où $v = (a, b, -a-b) \in V(J)$ est le diviseur sur les points $0$, $1$, $\infty$. Une permutation $\sigma$ de ces trois points est induite par une unique substitution anharmonique, et $\sigma$ envoie $f$ sur $f \circ h$, où $h$ est la substitution qui induit $\sigma^{-1}$. Sur le diviseur, l'action permute les coordonnées. Sur la constante, elle fait apparaître des signes : par exemple $\lambda/(\lambda - 1) = -\lambda(1-\lambda)^{-1}$, de sorte que composer $\lambda^a$ avec cette substitution multiplie la constante par $(-1)^a$. C'est ce signe qui rend l'extension $0 \to k^* \to \mathcal O(U_{0,3})^* \to V(J) \to 0$ de la note marginale non scindée en général. Lean définit ce module, sur un anneau intègre~$k$, par cette formule, et vérifie sur un corps que son action est celle des substitutions : évaluées en un point $x$ de $U(k)$, les images de $\lambda$ et de $1 - \lambda$ par $\sigma$ valent $h(x)$ et $1 - h(x)$, et les constantes sont fixes.

La figure~\ref{fig:140-1-reseau} montre le réseau $V(J)$ des diviseurs d'unités, dessiné dans le plan $a + b + c = 0$ de $\mathbf Z^J$. Les six diviseurs les plus courts sont ceux de $\lambda$, $1 - \lambda$, $\lambda/(\lambda - 1)$ et de leurs inverses ; $\mathfrak S_3$ agit par les symétries d'axes les trois droites en tirets, une par transposition. Le $\mathfrak S_3$-module $V(J)$ ne voit pas les constantes : le signe de $\lambda/(\lambda - 1) = -\lambda(1 - \lambda)^{-1}$, que le modèle garde, est invisible sur le dessin, et c'est lui qui porte la partie d'ordre~$2$.

\begin{figure}[htbp]
\centering
\begin{tikzpicture}[x=0.95cm, y=0.95cm, >=stealth, every node/.style={font=\small}]
\foreach \p in {(2.598,-1.50), (0.000,-3.00), (0.866,-1.50), (1.732,0.00), (2.598,1.50), (-0.866,-1.50), (0.866,1.50), (-2.598,-1.50), (-1.732,0.00), (-0.866,1.50), (0.000,3.00), (-2.598,1.50)} \fill[black!35] \p circle (1.3pt);
\draw[dashed, black!50] (0,0)+(30:-3.6) -- +(30:3.6) node[right] {$1/\lambda$, $(0\ \infty)$};
\draw[dashed, black!50] (0,0)+(-30:-3.6) -- +(-30:3.6) node[right] {$1 - \lambda$, $(0\ 1)$};
\draw[dashed, black!50] (0,-3.4) -- (0,3.4) node[above] {$\lambda/(\lambda - 1)$, $(1\ \infty)$};
\fill (0,0) circle (1.6pt);
\draw[->, thick] (0,0) -- (-0.866,1.5) node[above left] {$\lambda$};
\draw[->, thick] (0,0) -- (0.866,-1.5) node[below right] {$\lambda^{-1}$};
\draw[->, thick] (0,0) -- (-1.732,0) node[left] {$1 - \lambda$};
\draw[->, thick] (0,0) -- (1.732,0) node[right] {$(1 - \lambda)^{-1}$};
\draw[->, thick] (0,0) -- (0.866,1.5) node[above right] {$\frac{\lambda}{\lambda - 1}$};
\draw[->, thick] (0,0) -- (-0.866,-1.5) node[below left] {$\frac{\lambda - 1}{\lambda}$};
\end{tikzpicture}
\caption{Le réseau $V(J) = \operatorname{Ker}(\mathbf Z^J \to \mathbf Z)$, $J = \{0, 1, \infty\}$, et les six unités de diviseur minimal : $\operatorname{div} \lambda = [0] - [\infty]$, $\operatorname{div}(1 - \lambda) = [1] - [\infty]$, $\operatorname{div} \frac{\lambda}{\lambda - 1} = [0] - [1]$. Chaque transposition, induite par la substitution indiquée, agit par la symétrie d'axe la droite en tirets correspondante.}
\label{fig:140-1-reseau}
\end{figure}


\noindent\emph{La classe tangente.} Le cocycle $\sigma \mapsto (h^{-1})'(\lambda)$, $h$ comme ci-dessus, décrit l'action de $\mathfrak S_3$ sur la droite tangente au point mobile ; c'est le cocycle de la cote~146 (§\,\ref{sec:146}). Dans le modèle, sa constante est la signature de $\sigma$ et son diviseur est $2[\infty] - 2[\sigma(\infty)]$. Par exemple, pour $h = 1/\lambda$, qui échange $0$ et $\infty$, on trouve $-\lambda^{-2}$.

\begin{theoreme}[énoncé de l'édition, pour la page 24]\label{thm:140-1-valeur}
Soit $k$ un anneau intègre. Si $2 \neq 0$ dans $k$, le groupe $H^1(\mathfrak S_3, \mathcal O(U_{0,3})^*)$ du modèle est cyclique d'ordre~$6$, engendré par la classe tangente. Si $2 = 0$, il est cyclique d'ordre~$3$, engendré par la même classe.
\end{theoreme}

\begin{proof}
L'ordre du groupe divise $6$, et $3$ si $2 = 0$, par le théorème~\ref{thm:140-1-majoration}. Il suffit de voir que si $m$ fois la classe tangente est nulle, alors $3 \mid m$, et $2 \mid m$ quand $2 \neq 0$. Supposons $m\,c = \delta(x)$, où $c$ est le cocycle tangent et $x$ une unité. Le diviseur de $c$ vaut $-2$ fois le cobord de $[\infty]$ dans $\mathbf Z^J$ ; avec la description de $H^1(\mathfrak S_3, V(J)) = \mathbf Z/3$ par la somme des potentiels, sa classe est $-2 \equiv 1 \pmod 3$, un générateur. Comme $m\,c$ est un cobord, son image $m$ est nulle dans $\mathbf Z/3$. Prenons ensuite pour $\sigma$ la transposition de $0$ et~$1$, induite par $h = 1 - \lambda$. Elle fixe $\infty$, et l'action de $\sigma$ sur la constante d'une unité ne fait apparaître aucun signe. La constante de $\sigma(x) - x$ vaut donc~$1$, alors que celle de $m\,c(\sigma)$ vaut $(-1)^m$. Si $2 \neq 0$, on a $-1 \neq 1$, et $m$ est pair.
\end{proof}

La minoration n'utilise ni racine de $\zeta^2 - \zeta + 1$ ni l'hypothèse $3 \neq 0$ : la caractéristique~$3$ est couverte, comme la lecture l'annonce. Dans la cote~146, l'ordre $6$ du même cocycle se lit aux points fixes $-1$ et $\zeta$ ; ici la partie d'ordre~$3$ se lit sur le diviseur et la partie d'ordre~$2$ sur la constante.

\begin{sloppypar}
\noindent Vérifié dans le modèle (\texttt{card\_H1\_units\_dvd}, \texttt{dvd\_of\_zsmul\_tan}, \texttt{H1\_units}, \texttt{H1\_units\_char\_two}) ; le modèle est comparé aux substitutions et aux dérivées de la cote~146 par \texttt{ev\_smul\_lam}, \texttt{ev\_smul\_lam'}, \texttt{smul\_incl} et \texttt{ev\_tan}. Que les unités de $U_{0,3}$ soient celles du modèle est le calcul classique des unités de $k[\lambda, 1/\lambda, 1/(1-\lambda)]$ ; il est démontré ci-dessous.
\end{sloppypar}

\begin{theoreme}[calcul classique, ajouté par l'édition]\label{thm:140-1-unites}
Soit $k$ un anneau intègre et $A = k[\lambda, 1/\lambda, 1/(1-\lambda)]$, le localisé de $k[\lambda]$ en $\lambda(1-\lambda)$. L'application $(c, a, b) \mapsto c\,\lambda^a(1-\lambda)^b$ est un isomorphisme de $k^* \times \mathbf Z \times \mathbf Z$ sur $A^*$ ; autrement dit $\mathcal O(U_{0,3})^*$ est le modèle $k^* \times V(J)$, les constantes s'envoyant sur les constantes. Si $k$ est un corps, $\mathrm{Pic}(A) = 0$.
\end{theoreme}

\begin{proof}
Les éléments $\lambda$ et $1 - \lambda$ sont premiers dans $k[\lambda]$ et ne se divisent pas l'un l'autre (évaluer en $0$ et en~$1$). Injectivité : si $c\,\lambda^a(1-\lambda)^b = 1$, on chasse les dénominateurs, $c\,\lambda^{a_+}(1-\lambda)^{b_+} = \lambda^{a_-}(1-\lambda)^{b_-}$ dans $k[\lambda]$, qui s'injecte dans $A$ ; un premier qui ne divise ni une unité ni l'autre premier se simplifie, d'où $a_+ = a_-$, $b_+ = b_-$ et $c = 1$. Surjectivité : une unité $u$ s'écrit $p/(\lambda(1-\lambda))^n$ et son inverse $q/(\lambda(1-\lambda))^m$, donc $pq = \lambda^N(1-\lambda)^N$ dans $k[\lambda]$. Par récurrence sur $N$, un diviseur d'un produit de premiers est associé à un sous-produit : $p = w\,\lambda^i(1-\lambda)^j$ avec $w \in k[\lambda]^* = k^*$ ($k$ intègre), et $u = w\,\lambda^{i-n}(1-\lambda)^{j-n}$. Sur un corps, $A$ est un localisé de l'anneau principal $k[\lambda]$, donc factoriel, et le groupe de Picard d'un anneau factoriel est nul.
\end{proof}

\noindent Vérifié tel quel (\texttt{dvd\_pow\_mul\_pow}, \texttt{C\_mul\_pow\_inj}, \texttt{unitOf\_eq\_one}, \texttt{exists\_unitOf}, \texttt{toUnits\_bijective}, \texttt{unitsEquiv}, \texttt{toUnits\_incl}, \texttt{pic\_O3\_subsingleton}). Lean ne définit pas l'action de $\mathfrak S_3$ sur $A$ par les substitutions anharmoniques et ne vérifie pas que \texttt{unitsEquiv} est équivariant ; l'action du modèle n'est comparée aux substitutions que point par point, par \texttt{ev\_smul\_lam} et \texttt{ev\_smul\_lam'}.

Ne sont pas démontrés ici : l'équivariance de l'identification des unités, $\mathrm{Pic}(U_{0,3}) = 0$ sur une base $S$ générale (il l'est sur un corps, théorème~\ref{thm:140-1-unites}) et la suite de Hochschild--Serre, qui identifient le groupe de Picard du champ quotient à ce $H^1$, et le choix de la page, qui prend pour générateur $\mathcal O(1)$ sur $\mathbf P(V_J)$ au lieu de la classe tangente. L'énoncé de la page reste donc ouvert sous sa forme géométrique :

\begin{encadre}
\begin{theoreme*}[Grothendieck, pages 22, 24 et 29, Picard du champ {$[U_{0,3}/\mathfrak S_3]$}\piste{140-1-equivariant-pic-u03}]\nonverifie
Soit $S$ régulier intègre avec $\mathrm{Pic}(S) = 0$. Le groupe de Picard du champ quotient $[(\mathbf P^1 - \{0, 1, \infty\})_S/\mathfrak S_3]$, $\mathfrak S_3$ agissant par les substitutions anharmoniques, est $\mathbf Z/6$, engendré par $\mathcal O(1)$ sur $\mathbf P(V_J)$, en caractéristique générique $\neq 2$, et $\mathbf Z/3$ en caractéristique générique~$2$.
\end{theoreme*}
\end{encadre}
{\small Le groupe $H^1(\mathfrak S_3, \mathcal O(U_{0,3})^*)$ est calculé au théorème~\ref{thm:140-1-valeur} pour $S$ le spectre d'un corps. Restent le passage de $H^1$ au groupe de Picard, la base $S$ générale et l'identification du générateur à $\mathcal O(1)$. Mathlib n'a pas les champs quotients ni leur groupe de Picard.\par}
\bigskip
\noindent Autres pistes de l'onglet Findings pour ce thème, dans des cotes qui n'ont pas de section ici :\par
\begin{itemize}\small\setlength{\itemsep}{0pt}
\item Cote~138 : critère pour qu'une partie $A$ de la sphère définisse par image réciproque une nouvelle structure de carte : $A$ connexe, et $A$ contient au plus un des points $0$, $1$, $\infty$ ; telle qu'elle est lue, la seconde condition est contredite par l'exemple $A = [0, 1]$, et la lecture de la page doit être vérifiée sur le fac-similé avant toute formalisation. Mathlib n'a pas les cartes sur les surfaces. On se reportera aux notes de Grothendieck (\lot{138}{7}{122}).\piste{138-operations-subset-criterion}
\end{itemize}

\begin{encadre}
\begin{theoreme*}[Grothendieck, pages 122 à 124 et 127, opérations sur les cartes\piste{138-operations-belyi-extending}]\nonverifie
Une opération sur les cartes orientées donnée par une partie $A$ de la sphère de référence, tirée en arrière le long du revêtement $f : X \to S$ de chaque carte, est, sauf un cas exceptionnel, la composition avec un revêtement $\varphi : S \to S$ ramifié seulement au-dessus de $0$, $1$, $\infty$, avec $\varphi^{-1}\{0, 1, \infty\} \supset \{0, 1, \infty\}$ et une ramification $2$ au-dessus de $1$, de sorte que $A = \varphi^{-1}([0, 1])$. La page demande ce qu'il advient dans le cas exceptionnel.
\end{theoreme*}
\end{encadre}
{\small Une carte orientée est un revêtement fini de la sphère non ramifié hors de $0$, $1$, $\infty$, la carte étant l'image réciproque de $[0, 1]$ ; c'est le dictionnaire des cartes et des revêtements de Jones et Singerman (1978) \cite{jonessingerman1978}. Par le théorème de Belyi (1979) \cite{belyi1979}, les courbes qui portent de tels revêtements sont exactement les courbes définies sur $\overline{\mathbf Q}$, et $\mathrm{Gal}(\overline{\mathbf Q}/\mathbf Q)$ opère sur les cartes par son action sur le groupe profini $\hat F_2$ de la section~\ref{sec:145}, qui se factorise par $\widehat{GT}$ (Drinfeld 1990 \cite{drinfeld1990} ; Ihara 1991 \cite{ihara1991}). L'opération de l'encadré est la composition avec un revêtement $\varphi$ du même type, ramifié seulement au-dessus de $0$, $1$, $\infty$. Mathlib n'a pas les revêtements de Belyi de la sphère. On se reportera aux notes de Grothendieck (\lot{138}{7}{122}).\par}