\section[Cote 70 : l'icosaèdre en coordonnées universelles, fidèle en toute caractéristique, et sa conique modulo 5]{Cote 70 : l'icosaèdre sur $\mathbf Z[\alpha]$, fidèle en toute caractéristique, et sa conique modulo~$5$\protect\verifie{Folder70}}\label{sec:70}

La cote 70, \emph{Réalisations géométriques de structures combinatoires (vieilles rédactions)}, compte cent vingt-cinq pages. Sa section~VII, sous la chemise de la page~73, écrit l'icosaèdre régulier sur l'anneau $\mathbf Z[\alpha] = \mathbf Z[x]/(x^2 + x - 1)$ par trois réflexions dans le repère des sommets $(s_0, s_1 - s_0, s_2 - s_0, s_3 - s_0)$. Les pages~74 et~75 donnent les générateurs et les douze sommets (\lot{70}{4}{74}, \lot{70}{4}{75}), les pages~89 à~92 le centre et l'antipodisme $\iota$, avec sa forme en caractéristique~$2$ (\lot{70}{5}{91}). Les pages~93 et~94 veulent établir, \q{sur un corps de base quelconque}, que trois sommets distincts ne sont jamais alignés et qu'aucun sommet n'est dans le plan d'une face qui ne le contient pas ; elles traitent les droites issues de $s_0$ et le plan $z = 0$ de la face $(s_0, s_1, s_2)$, et invoquent l'homogénéité pour le reste (\lot{70}{5}{93}, \lot{70}{5}{94}). La page~95 donne la fonction quadratique invariante $q$, les pages~101 et~102 sa partie quadratique $q_0$ et ses discriminants (\lot{70}{6}{101}). Le tableau \q{Directions remarquables} de la page~78 compte $6$ directions de sommets, $15$ d'arêtes et $10$ de plans de faces, $31 = 5^2 + 5 + 1$, dit que \q{les 6 directions de sommets correspondent à la conique} et écrit $125 = 1 + 24 + 60 + 40$, avec \q{deux icos.} (\lot{70}{4}{78}). On démontre ici l'énoncé de la page~78 sur $\mathbf F_5$, les incidences des pages~93 et~94 sur tout anneau non nul où $\alpha^2 + \alpha = 1$, donc en toute caractéristique, $2$ et $5$ comprises, et, en fin de section, les formules universelles des pages~9 à~25 avec le critère d'ordre de la page~67 pour les ordres $3$, $4$ et $5$.

\noindent\emph{Conventions.} $R$ est un anneau commutatif, $\alpha \in R$, $\alpha' = -1 - \alpha$, et l'on écrit les points de $R^3$ en coordonnées $(x, y, z)$. Les générateurs sont
\[
\sigma_0(x, y, z) = \bigl(1 - (x + y + z), y, z\bigr), \quad \sigma_1(x, y, z) = (y + \alpha' z, x - \alpha' z, z), \quad \sigma_2(x, y, z) = (x, z, y),
\]
et $\iota(x, y, z) = (\alpha' - x, 1 - \alpha' - y, 1 - \alpha' - z)$. Les douze sommets sont, dans cet ordre, $s_0 = 0$, $s_1 = e_1$, $s_2 = e_2$, $s_3 = e_3$, $s'_3 = (\alpha', -\alpha', 1)$, $s''_3 = (0, -\alpha', 1)$ et leurs images par $\iota$. On pose
\[
q_0 = x^2 + y^2 + z^2 - \alpha yz + zx + xy, \qquad q = q_0 - (x + y + z),
\]
et $\varphi$ la forme polaire de $q_0$, de matrice $\begin{pmatrix} 2 & 1 & 1 \\ 1 & 2 & -\alpha \\ 1 & -\alpha & 2 \end{pmatrix}$. Les trente arêtes sont les paires de sommets à distance $q_0 = 1$ sur $\mathbf Q(\sqrt 5)$, listées dans le fichier ; les vingt faces sont les triangles d'arêtes. Sur $R$, on dit que $p$ est sur la droite $(r, u)$ s'il existe $a \in R$ avec $p - r = a(u - r)$, et dans le plan $(r, u, w)$ s'il existe $s, t \in R$ avec $p - r = s(u - r) + t(w - r)$ ; sur un corps, et pour $r \neq u$, c'est l'alignement et la coplanarité usuels. Sur $\mathbf F_5$, la seule racine de $x^2 + x - 1$ est $2$, de sorte que la réduction modulo~$5$ de la réalisation est celle de $\alpha = 2$, $\alpha' = 2$ ; on note alors $o = (1, 2, 2)$ et $\bar s = s - o$ pour un sommet $s$.

\begin{enonce}[Pages 74, 75, 91, 94 et 101, sur un anneau quelconque]
Supposons $\alpha^2 + \alpha - 1 = 0$ dans $R$.
\begin{enumerate}
\item Les douze sommets annulent $q$.
\item $\sigma_0$, $\sigma_1$, $\sigma_2$ permutent les douze sommets, par des permutations de $\{0, \dots, 11\}$ qui ne dépendent pas de $R$.
\item Pour chacune des trente arêtes $\{s, s'\}$, $q_0(s' - s) = 1$.
\item Les neuf sommets autres que $s_0$, $s_1$, $s_2$ ont une coordonnée $z$ inversible : $1$, $1 - \alpha' = 2 + \alpha$ ou $-\alpha' = 1 + \alpha$.
\item Sans hypothèse sur $\alpha$, si $2 = 0$ dans $R$, $\iota$ est la translation de vecteur $(\alpha', \alpha, \alpha)$.
\end{enumerate}
\end{enonce}

\begin{proof}
Chaque point est une identité polynomiale en $\alpha$ et en les coordonnées, vraie modulo $\alpha^2 + \alpha - 1$ : on l'écrit comme combinaison de la relation $\alpha^2 + \alpha - 1 = 0$, de coefficient $-2 - \alpha$ ou $-1 - \alpha$ pour $q(\iota s_0)$, $q(\iota s_1)$, $q(\iota s_2)$, $q(\iota s_3)$, $\pm 1$ pour $\sigma_1$, $-\alpha$ ou $1 + \alpha$ pour quatre des arêtes, nul ailleurs. Pour le point~4, $(2 + \alpha)(1 - \alpha) = 1$ et $(1 + \alpha)\alpha = 1$. Pour le point~5, la première coordonnée de $\iota(p) - p - (\alpha', \alpha, \alpha)$ vaut $-2x$, les deux autres $2(1 - y)$ et $2(1 - z)$.
\end{proof}

\begin{enonce}[Pages 93 et 94, fidélité en toute caractéristique\piste{70-icosahedron-integral-faithful}]
Soit $R$ un anneau commutatif non nul où $\alpha^2 + \alpha - 1 = 0$. Alors
\begin{enumerate}
\item les douze sommets sont distincts ;
\item pour trois sommets distincts $s, s', s''$, le point $s''$ n'est pas sur la droite $(s, s')$ ;
\item pour une face $(a, b, c)$ et un sommet $m$ distinct de $a$, $b$, $c$, le point $m$ n'est pas dans le plan $(a, b, c)$.
\end{enumerate}
\end{enonce}

\begin{proof}
Les applications $\sigma_k$ sont affines : si $p - r = s(u - r) + t(w - r)$, alors $\sigma_k p - \sigma_k r = s(\sigma_k u - \sigma_k r) + t(\sigma_k w - \sigma_k r)$, coordonnée par coordonnée. D'après l'énoncé précédent, un mot $w$ en les $\sigma_k$ envoie le sommet d'indice $i$ sur le sommet d'indice $\pi_w(i)$, où $\pi_w$ est le mot correspondant en les trois permutations, qui est une permutation de $\{0, \dots, 11\}$. Un mot transporte donc l'égalité de deux sommets, l'appartenance d'un sommet à la droite de deux autres, et à un plan de trois autres.

C'est l'homogénéité que la page invoque, rendue explicite par deux tables. Pour toute paire $(i, j)$ d'indices distincts, la table \texttt{pairWord} donne un mot $w$ tel que $\pi_w(i) = 0$ et $\pi_w(j) \in \{1, 5, 6\}$, c'est-à-dire qui envoie $(s_i, s_j)$ sur $(s_0, s_1)$, $(s_0, s''_3)$ ou $(s_0, \iota s_0)$ ; pour toute face $(a, b, c)$, la table \texttt{faceWord} donne un mot qui l'envoie, dans l'ordre, sur $(s_0, s_1, s_2)$. Ces $132 + 20$ propriétés portent sur des permutations de $\{0, \dots, 11\}$ et sont vérifiées par le noyau de Lean (\texttt{decide +kernel}).

Il reste les cas de base. Comme $s_0 = 0$, le sommet $s_k$ est sur la droite $(s_0, s_j)$ si et seulement si $s_k = a\,s_j$ pour un $a \in R$, ce qui annule les trois mineurs d'ordre~$2$ de la matrice de colonnes $s_k$, $s_j$. Pour $j \in \{1, 5, 6\}$ et chacun des trente $k \neq 0, j$, l'un de ces mineurs est une unité de $\mathbf Z[\alpha]$, à savoir $\pm 1$, $\pm(1 + \alpha)$, $\pm(2 + \alpha)$ ou $\pm(3 + 2\alpha)$, d'inverses $\pm\alpha$, $\pm(1 - \alpha)$ et $\pm(2\alpha - 1)$. Pour chaque cas, une identité $1 = u\,(m_{rs}) + c\,(\alpha^2 + \alpha - 1)$, où $m_{rs}$ s'écrit à partir des égalités de coordonnées, donne $1 = 0$, ce qui est exclu dans un anneau non nul. Le point~2 s'en déduit : si $s''$ est sur la droite $(s, s')$, le mot de la paire $(s, s')$ amène $s''$ sur un sommet $s_k$ de la droite $(s_0, s_j)$, avec $k \neq 0, j$ puisque $\pi_w$ est injective. Pour le point~1, le même mot ramène une égalité $s_i = s_j$ à $s_{j'} = 0$ pour $j' \in \{1, 5, 6\}$ ; or $s_1$ a pour première coordonnée $1$, $s''_3$ pour troisième coordonnée $1$, et $\iota s_0$ pour troisième coordonnée l'unité $2 + \alpha$. Pour le point~3, le mot de la face amène $m$ sur un sommet d'indice au moins $3$ dans le plan $(s_0, s_1, s_2)$, c'est-à-dire de coordonnée $z$ nulle, contre le point~4 de l'énoncé précédent.
\end{proof}

\begin{encadre}
\begin{theoreme}[D'après la page 78, forme complétée par l'édition, la conique de $\mathbf P^2(\mathbf F_5)$\piste{70-icosahedron-char5-conic}]
Sur $\mathbf F_5$, avec $\alpha = 2$ :
\begin{enumerate}
\item $2o = (\alpha', 1 - \alpha', 1 - \alpha')$, $o$ est fixe par $\sigma_0$, $\sigma_1$, $\sigma_2$ et $\iota$, et $q(o) = 0$ ;
\item les douze sommets sont isotropes pour $q_0$ centrée en $o$ : $q_0(\bar s) = 0$ ;
\item les vecteurs non nuls isotropes de $q_0$ sont les douze $\bar s$ et leurs doubles $2\bar s$ ; ces vingt-quatre vecteurs sont distincts ;
\item un point de $\mathbf P^2(\mathbf F_5)$ est sur la conique $q_0 = 0$ si et seulement si c'est l'une des six directions $\bar s_0, \dots, \bar s''_3$ ;
\item les six directions de sommets, les quinze directions $s' - s$ d'arêtes choisies et les dix directions $\bar a + \bar b + \bar c$ des faces $0$ à $9$ sont les trente et un points de $\mathbf P^2(\mathbf F_5)$, chacun une fois ; toute arête et toute face donne l'une de ces directions, tout sommet l'une des six ;
\item la direction $\bar a + \bar b + \bar c$ d'une face $(a, b, c)$ est $\varphi$-orthogonale à $b - a$ et à $c - a$, c'est-à-dire au plan de la face ;
\item par une direction d'arête passent exactement deux tangentes à la conique, par une direction de face aucune ; $q_0$ prend la valeur $1$ ou $4$ sur $60$ vecteurs, la valeur $2$ ou $3$ sur $40$.
\end{enumerate}
\end{theoreme}
\end{encadre}

\begin{proof}
L'unicité de la racine $2$ se vérifie sur les cinq éléments de $\mathbf F_5$. Le reste porte sur les $125$ vecteurs de $\mathbf F_5^3$ et sur des listes finies de sommets, d'arêtes et de faces, et chaque point est vérifié par le noyau de Lean. Pour le point~5, l'application qui envoie chacun des trente et un représentants sur son point de $\mathbf P^2(\mathbf F_5)$ est injective, car aucun représentant n'est multiple d'un autre, et surjective, car tout vecteur non nul est multiple de l'un d'eux ; on en tire aussi que $\mathbf P^2(\mathbf F_5)$ a $31$ points. Le point~4 est l'énoncé, vérifié sur les $124$ vecteurs non nuls, que $q_0(v) = 0$ si et seulement si $v$ est multiple d'un des six représentants de sommets. Au point~7, la tangente à la conique au point $\bar s$ est la droite $\varphi(\bar s, \cdot) = 0$, et l'on compte, pour chaque représentant, les six sommets dont la tangente le contient.
\end{proof}

\begin{remarque}
La page~78 donne le tableau des points~4 et~5 et le décompte $125 = 1 + 24 + 60 + 40$ ; les points~6 et~7 sont de l'édition. La vérification confirme ce tableau et la lecture : la réduction modulo~$5$ place les sommets sur le cône isotrope de sommet $o$, les six directions de sommets remplissent la conique, et les $6 + 15 + 10$ directions sont les $31$ points du plan. L'explication des quinze directions d'arêtes par les points extérieurs et des dix directions de faces par les points intérieurs, que la piste laissait à l'édition parce que les mots de la page y sont incertains, est démontrée au point~7, avec la définition par les tangentes ; les classes $\{1, 4\}$ et $\{2, 3\}$ des valeurs de $q_0$ en sont la forme arithmétique, et donnent le décompte $60 + 40$. Les vingt-quatre vecteurs isotropes non nuls sont les sommets de l'icosaèdre et de son homothétique de rapport~$2$ : ce sont les \q{deux icos.} de la page. Pour la fidélité, la démonstration n'utilise ni corps ni calcul de normes au-delà de trente mineurs inversibles : elle vaut sur tout anneau non nul où $\alpha^2 + \alpha = 1$, donc en caractéristique $2$ (sur une $\mathbf F_4$-algèbre) et $5$. L'argument d'homogénéité de la page suffit, une fois les deux tables de mots vérifiées, et la marge \q{c'est en fait faux en car.~$2$ !} ne vise donc ni le non-alignement ni le plan de la face. Le vecteur de translation de $\iota$ en caractéristique~$2$ est $(\alpha', \alpha, \alpha)$, et non le $(\alpha', 1, 1)$ lu sur la page~91.
\end{remarque}

\begin{enonce}[Pages 75 et 87, l'ordre du groupe\piste{70-icosahedron-integral-faithful}]
Soit $R$ un anneau commutatif non nul où $\alpha^2 + \alpha - 1 = 0$. Le groupe $G$ des permutations de $R^3$ engendré par $\sigma_0$, $\sigma_1$, $\sigma_2$ est d'ordre $120$ ; il agit fidèlement sur les douze sommets, et le groupe des permutations de $\{0, \dots, 11\}$ engendré par les trois permutations du premier énoncé est lui aussi d'ordre $120$.
\end{enonce}

\begin{proof}
Pour les permutations, une table de $120$ mots en $\pi_0$, $\pi_1$, $\pi_2$, de longueur au plus $15$, obtenue par un parcours en largeur, donne $120$ permutations distinctes, et une seconde table dit sur quel mot de la première la multiplication à gauche par chaque $\pi_k$ envoie chacun d'eux. Comme les $\pi_k$ sont des involutions, l'ensemble de ces $120$ permutations contient $1$ et est stable par multiplication à gauche par les générateurs et leurs inverses : il contient le groupe engendré, qui le contient. Ces vérifications sont faites par le noyau de Lean (\texttt{decide +kernel}). Pour $G$, on compare les deux morphismes du groupe libre à trois générateurs, vers $G$ et vers le groupe des permutations des indices. Par récurrence sur les mots, l'image $g$ d'un mot dans $G$ envoie le sommet d'indice $i$ sur celui d'indice $\pi(i)$, où $\pi$ est l'image du même mot, et $g$ est affine, $g(x, y, z) = g(0) + x\,(g(e_1) - g(0)) + y\,(g(e_2) - g(0)) + z\,(g(e_3) - g(0))$, propriété stable par composition. Si $g = 1$, $\pi$ fixe tous les indices, puisque les sommets sont distincts ; si $\pi = 1$, $g$ fixe $s_0 = 0$, $s_1 = e_1$, $s_2 = e_2$, $s_3 = e_3$, donc $g = 1$. Les deux noyaux coïncident, et $G$ est isomorphe au groupe des permutations.
\end{proof}

Voir \texttt{card\_icoPermGroup} et \texttt{card\_icoGroup} dans \href{\leanblob/Folder70.lean}{\texttt{Folder70.\allowbreak{}lean}}. La page~87 admet l'ordre $120$ (\q{si nous admettons que $G$ est d'ordre $120$}) ; il vaut sur tout anneau non nul où $\alpha^2 + \alpha = 1$, caractéristiques $2$ et $5$ comprises. Ne sont pas démontrés ici : que $G$ soit le groupe de Coxeter $H_3 \simeq \mathfrak A_5 \times \mathbf Z/2$, et que les trente paires listées soient l'orbite de l'arête $\{s_0, s_1\}$ (le fichier montre seulement que les générateurs permutent les sommets et que ces paires sont à distance $q_0 = 1$) ; la quadrique des pages~101 et~102 fait l'objet de l'énoncé suivant ; les relations $\Delta = \alpha\Delta'$ et $\Phi' = (2\alpha - 1)\Phi$ de la page~76 ; la proposition \q{régulière $\Rightarrow$ fidèle} de la page~109.

\begin{encadre}
\begin{exemple}[Grothendieck, pages 101, 102 et 106, la quadrique de l'icosaèdre\piste{70-icosahedron-integral-faithful}]
Soit $R$ un anneau commutatif où $\alpha^2 + \alpha - 1 = 0$, et $q = x^2 + y^2 + z^2 - \alpha yz + zx + xy - (x + y + z)$.
\begin{enumerate}
\item $q$ est invariante par $\sigma_0$, $\sigma_1$, $\sigma_2$ et s'annule aux douze sommets ; toute fonction quadratique $F = a x^2 + \dots + k$ qui s'annule en $s_0, s_1, s_2, s_3, s'_3, s''_3, \iota s_0, \iota s_1, \iota s_2$ est égale à $a\,q$. La quadrique passant par les sommets est donc unique.
\item Sa partie quadratique $q_0$ a pour demi-discriminant $\delta'(q_0) = 1$ ; sa matrice polaire $\bigl(\begin{smallmatrix} 2 & 1 & 1 \\ 1 & 2 & -\alpha \\ 1 & -\alpha & 2 \end{smallmatrix}\bigr)$ a pour déterminant~$2$.
\item La quadrique projective $Q(x, y, z, t) = q_0(x, y, z) - (x + y + z)\,t$ a pour discriminant $-\alpha - 3$, de norme $(-\alpha - 3)(-\alpha' - 3) = 5$ ; il est inversible si et seulement si $5$ l'est, et alors le seul zéro commun des quatre dérivées partielles de $Q$ est $0$ : $Q$ est lisse.
\item Si $5 = 0$ et $\alpha = 2$, les zéros communs des dérivées partielles sont les multiples de $(1, 2, 2, 1)$, qui est sur $Q$ : la quadrique est un cône de sommet le centre $o = (1, 2, 2)$. Sur un corps, $Q$ a un point singulier si et seulement si la caractéristique est~$5$.
\end{enumerate}
\end{exemple}
\end{encadre}

\begin{proof}
L'invariance se vérifie en développant $q \circ \sigma_k$, pour tout $\alpha$. Pour l'unicité, une fonction quadratique a dix coefficients, et ses valeurs aux sommets sont des formes linéaires en ces coefficients. Sur les neuf sommets cités, le mineur d'ordre~$9$ pris hors de la colonne de $x^2$ vaut $13\alpha + 21$, unité de $\mathbf Z[\alpha]$ d'inverse $13\alpha - 8$ (de norme $-1$) : chacun des neuf coefficients restants, diminué de $a$ fois le coefficient correspondant de $q$, est une combinaison à coefficients dans $\mathbf Z[\alpha]$ des neuf valeurs, par exemple, pour la fonction $F$, $d + a = F(s_1) - F(s_0)$ et $k = F(s_0)$. La page fait le même calcul par l'invariance (\q{c'est clair}) ; ici l'invariance n'est pas même nécessaire, et l'énoncé vaut sur tout anneau, sans diviser par rien.

Le demi-discriminant de $a x^2 + b y^2 + c z^2 + u yz + v zx + w xy$ est le polynôme $4abc + uvw - au^2 - bv^2 - cw^2$, dont le double est le déterminant de la matrice polaire. Pour $q_0$, il vaut $4 - \alpha - \alpha^2 - 1 - 1 = 2 - (\alpha^2 + \alpha) = 1$ : c'est la \q{merveille} de la page~101, et elle vaut aussi en caractéristique~$2$. Le déterminant d'ordre~$4$ de la matrice (22), développé selon la première ligne, vaut $\alpha^2 - 4 = -\alpha - 3$. Comme $(-\alpha - 3)(\alpha - 2) = 5$ et $(-\alpha - 3)^2 = 5(\alpha + 2)$, le discriminant divise $5$ et $5$ divise son carré, de sorte que l'un est inversible si et seulement si l'autre l'est. Les lignes de la matrice sont les dérivées partielles de $Q$ (et $v \cdot Mv = 2Q(v)$) ; une matrice de déterminant inversible n'a pas de noyau, d'où la lissité. En caractéristique~$5$, $\alpha^2 + \alpha - 1 = (\alpha - 2)^2$, donc $\alpha = 2$ sur un corps ; le système $Mv = 0$ se réduit alors, modulo~$5$, à $x = t$, $y = z = 2t$, et $Q(1, 2, 2, 1) = 1 + 4 + 4 - 8 + 2 + 2 - 5 = 0$.
\end{proof}

\begin{remarque}
Voir \texttt{q\_sigma}, \texttt{quadric\_unique}, \texttt{halfDisc\_q}, \texttt{det\_qMat4}, \texttt{norm\_disc}, \texttt{isUnit\_det\_qMat4\_iff}, \texttt{qHom\_smooth}, \texttt{qMat4\_ker\_char\_five} et \texttt{qHom\_singular\_iff} dans \href{\leanblob/Folder70.lean}{\texttt{Folder70.\allowbreak{}lean}}. La lissité est formalisée par l'absence de zéro commun non nul des dérivées partielles, lues sur la matrice polaire ; on n'a pas construit le schéma projectif ni utilisé le critère jacobien de Mathlib. L'unicité est démontrée parmi les fonctions quadratiques affines, non parmi les quadriques projectives, ce qui revient au même ici puisque $Q$ est l'homogénéisée de $q$. Que le cône de caractéristique~$5$ soit un cône sur une conique lisse découle de $\delta'(q_0) = 1$ et de \texttt{conic\_iff} plus haut, mais n'est pas énoncé comme un théorème séparé.
\end{remarque}

Les pages~9 à~25 écrivent toute réalisation affine régulière par réflexions du polytope $\{p_1, \dots, p_n\}$ dans le repère des sommets $(s_0, \dots, s_{n+1})$, avec $n$ paramètres $\alpha_0, \dots, \alpha_{n-1}$ (\lot{70}{1}{15}, \lot{70}{2}{23}) ; la page~67 énonce pour $n = 2$, sans démonstration, \q{$\rho_s^p = \mathrm{id} \iff F_p(\alpha) = 0$} (\lot{70}{4}{67}). En coordonnées barycentriques $(t_0, \dots, t_{n+1})$ relatives à ce repère, sur un anneau commutatif $R$, on pose $\ell_i = t_i - t_{i+1} + (1 + \alpha_i)(t_{i+2} + \dots + t_{n+1})$, $\sigma_i = \mathrm{id} + \ell_i \otimes (s_{i+1} - s_i)$ pour $0 \leq i \leq n$, et $w_k = s_{k+1} - s_k$.

\begin{encadre}
\begin{theoreme}[D'après les pages 19, 23 à 25 et 67, forme générale de l'édition, formules universelles\piste{70-universal-formulae-double-cosines}]
Soit $R$ un anneau commutatif, $n \geq 1$ et $\alpha_0, \dots, \alpha_{n-1} \in R$.
\begin{enumerate}
\item Quels que soient les $\alpha_i$, $\sigma_i^2 = 1$ et $\sigma_i\sigma_j = \sigma_j\sigma_i$ pour $i + 2 \leq j \leq n$ ; $\sigma_i$ conserve $t_0 + \dots + t_{n+1}$, $\sigma_i s_i = s_{i+1}$, $\sigma_i s_j = s_j$ pour $j < i$, et $\sigma_i s_j = s_j + (1 + \alpha_i) w_i$ pour $i + 2 \leq j \leq n + 1$.
\item Pour $k \leq n - 1$, l'image de $\sigma_k\sigma_{k+1} - 1$ est contenue dans le plan $\langle w_k, w_{k+1}\rangle$, et $(t - 1)(t^2 - \alpha_k t + 1)$ annule $\sigma_k\sigma_{k+1}$.
\item Si $R$ est non nul, $\sigma_k\sigma_{k+1}$ est d'ordre exactement $3$, $4$ ou $5$ si et seulement si, respectivement, $\alpha_k = -1$, $\alpha_k = 0$ ou $\alpha_k^2 + \alpha_k - 1 = 0$.
\end{enumerate}
\end{theoreme}
\end{encadre}

\begin{proof}
Comme $\ell_i(w_i) = -2$, $\ell_i(\sigma_i x) = -\ell_i(x)$, d'où $\sigma_i^2 = 1$. Pour $i + 2 \leq j \leq n$, $\ell_i(w_j) = (1 + \alpha_i)(1 - 1) = 0$ et $\ell_j(w_i) = 0$, de sorte que $\sigma_i\sigma_j x = x + \ell_i(x) w_i + \ell_j(x) w_j = \sigma_j\sigma_i x$. Les coordonnées de $w_i$ sont de somme nulle, et le tableau se lit sur les valeurs $\ell_i(s_j)$.

Soit $\rho = \sigma_k\sigma_{k+1}$. On a $\rho x = x + \ell_k(\sigma_{k+1}x)\, w_k + \ell_{k+1}(x)\, w_{k+1}$, et, puisque $\ell_{k+1}(w_k) = 1$ et $\ell_k(w_{k+1}) = 2 + \alpha_k$,
\[
\rho w_k = (1 + \alpha_k) w_k + w_{k+1}, \qquad \rho w_{k+1} = -(2 + \alpha_k) w_k - w_{k+1}.
\]
Sur $W = \langle w_k, w_{k+1}\rangle$, $\rho$ a pour trace $\alpha_k$ et pour déterminant $1$ : $\rho^2 - \alpha_k\rho + 1$ est nul sur $W$, qui contient l'image de $\rho - 1$, d'où le point~2. Pour le point~3, $\rho^m x = x + \sum_{j < m} \rho^j(\rho x - x)$ ; sur $W$, $\sum_{j < 3} \rho^j = (1 + \alpha_k)\rho$, $\sum_{j < 4} \rho^j = \alpha_k\bigl((1 + \alpha_k)\rho - 1\bigr)$ et $\sum_{j < 5} \rho^j = (\alpha_k^2 + \alpha_k - 1)(\alpha_k\rho - 1)$, nuls sous l'hypothèse correspondante, de sorte que $\rho^p = 1$. Réciproquement, $\rho s_k = s_{k+1}$, $\rho s_{k+1} = s_{k+2} + (1 + \alpha_k) w_k$, $\rho s_{k+2} = s_k$ : sur $\langle s_k, s_{k+1}, s_{k+2}\rangle$, $\rho(a, b, c) = \bigl(c - (1 + \alpha)b, a + (1 + \alpha)b, b\bigr)$, $\alpha = \alpha_k$. Les itérés de $s_k = (1, 0, 0)$ sont $(0, 1, 0)$, $(-1 - \alpha, 1 + \alpha, 1)$, $(-2\alpha - \alpha^2, \alpha + \alpha^2, 1 + \alpha)$, puis des vecteurs de dernières coordonnées $(\alpha^3 + \alpha^2 - \alpha, \alpha + \alpha^2)$ et, avec $P = \alpha^2 + \alpha - 1$, $\bigl((\alpha^2 - 1)P, \alpha P\bigr)$. Ainsi $\rho^3 s_k = s_k$ force $1 + \alpha = 0$ ; $\rho^4 s_k = s_k$ force $\alpha + \alpha^2 = 0 = \alpha^3 + \alpha^2 - \alpha$, d'où $\alpha = \alpha(\alpha + \alpha^2) - (\alpha^3 + \alpha^2 - \alpha) = 0$ ; $\rho^5 s_k = s_k$ force $\alpha P = 0 = (\alpha^2 - 1)P$, d'où $P = \alpha \cdot \alpha P - (\alpha^2 - 1)P = 0$. Sous chaque hypothèse, les itérés d'ordre $m < p$ ont une coordonnée égale à $1$ (ou à $\alpha + \alpha^2 = 1$) là où $s_k$ a $0$, de sorte que $\rho^m \neq 1$ dès que $R$ est non nul.
\end{proof}

La figure~\ref{fig:70-ordres} montre le point~3 sur $\mathbf R$. Le plan affine $s_k + W$ contient $s_k$, $s_{k+1} = s_k + w_k$ et $s_{k+2} = s_{k+1} + w_{k+1}$, et $\rho$ le conserve, puisque $\rho x - x \in W$. Sa partie linéaire, de trace $\alpha_k$ et de déterminant~$1$, est conjuguée à la rotation d'angle $2\pi/p$ quand $\alpha_k = 2\cos(2\pi/p)$ : les valeurs $-1$, $0$ et $(\sqrt 5 - 1)/2$, racine de $\alpha^2 + \alpha - 1$, donnent $p = 3$, $4$, $5$. L'orbite de $s_k$ est alors un polygone régulier à $p$ sommets, sur lequel $s_{k+1} = \rho s_k$ suit $s_k$ et $s_{k+2} = \rho^{-1} s_k$ le précède.

\begin{figure}[htbp]
\centering
\begin{tikzpicture}[x=1cm, y=1cm, >=stealth, every node/.style={font=\small}]
\foreach \p/\dx/\al in {3/0/{\alpha_k = -1}, 4/4.2/{\alpha_k = 0}, 5/8.4/{\alpha_k^2 + \alpha_k = 1}} {
  \begin{scope}[xshift=\dx cm]
  \pgfmathsetmacro{\stp}{360/\p}
  \pgfmathsetmacro{\anA}{90+\stp}
  \pgfmathsetmacro{\anB}{90-\stp}
  \fill[black!8] (-90:1.25) \foreach \j in {1,...,\p} { -- ({-90+\j*\stp}:1.25) } -- cycle;
  \draw[black!55] (-90:1.25) \foreach \j in {1,...,\p} { -- ({-90+\j*\stp}:1.25) } -- cycle;
  \fill[black!45] (0,0) circle (1.1pt);
  \draw[->, black!70] ({-90+0.18*\stp}:0.5) arc[start angle={-90+0.18*\stp}, end angle={-90+0.82*\stp}, radius=0.5];
  \node[black!70] at ({-90+0.5*\stp}:0.25) {\footnotesize $\rho$};
  \foreach \j in {1,...,\p} \fill ({-90+\j*\stp}:1.25) circle (1.6pt);
  \node[below=2pt] at (-90:1.25) {$s_k$};
  \node[anchor=\anA, inner sep=3pt] at ({-90+\stp}:1.25) {$s_{k+1}$};
  \node[anchor=\anB, inner sep=3pt] at ({-90-\stp}:1.25) {$s_{k+2}$};
  \node at (0,-2.05) {$p = \p$, \ $\al$};
  \end{scope}
}
\node[anchor=south, inner sep=3pt] at ([shift={(4.2,0)}]90:1.25) {$\rho^2 s_k$};
\node[anchor=234, inner sep=3pt] at ([shift={(8.4,0)}]54:1.25) {$\rho^2 s_k$};
\node[anchor=306, inner sep=3pt] at ([shift={(8.4,0)}]126:1.25) {$\rho^3 s_k$};
\end{tikzpicture}
\caption{L'orbite de $s_k$ sous $\rho = \sigma_k\sigma_{k+1}$ dans le plan affine $s_k + W$, sur $\mathbf R$, dans une coordonnée affine où la partie linéaire de $\rho$ est une rotation. Le centre est le point fixe de $\rho$ dans ce plan. Pour $p = 3$, $\rho^2 s_k = s_{k+2}$. L'autre racine de $\alpha^2 + \alpha - 1$, $-(1 + \sqrt 5)/2 = 2\cos(4\pi/5)$, donne la rotation d'angle $4\pi/5$ et le pentagone étoilé.}
\label{fig:70-ordres}
\end{figure}

\begin{remarque}
Voir \texttt{usig\_mul\_self}, \texttt{usig\_comm}, \texttt{sum\_usig}, \texttt{rho\_cubic}, \texttt{orderOf\_rho\_eq\_three}, \texttt{orderOf\_rho\_eq\_four} et \texttt{orderOf\_rho\_eq\_five} dans \href{\leanblob/Folder70.lean}{\texttt{Folder70.\allowbreak{}lean}}. La lecture démontre le critère sur un corps où $p$ est inversible ; pour $p = 3$, $4$, $5$, les seules valeurs des polytopes réguliers finis, il vaut sur tout anneau, en toute dimension, caractéristiques $2$, $3$ et $5$ comprises. Les générateurs des pages~74 et~75 sont le cas $n = 2$, $(\alpha_0, \alpha_1) = (-1, \alpha)$ (\texttt{usig\_emb}, \texttt{ico\_orderOf}) ; tétraèdre $(-1, -1)$, cube $(0, -1)$, octaèdre $(-1, 0)$ et dodécaèdre $(\alpha, -1)$ sont les autres solides de Platon, et l'autre racine de $\alpha^2 + \alpha - 1$, celle des polyèdres étoilés de la page~69, vérifie les mêmes identités. Le critère pour $p$ quelconque fait l'objet de l'énoncé suivant ; n'est pas démontré le passage de la définition d'une réalisation régulière à la forme normale (pages~7 à~18).
\end{remarque}

\begin{encadre}
\begin{theoreme}[D'après la page 67, forme de l'édition, le critère pour tout $p$\piste{70-universal-formulae-double-cosines}]
Soit $n \geq 1$, $k \leq n - 1$ et $\rho = \sigma_k\sigma_{k+1}$.
\begin{enumerate}
\item Si $R$ est non nul, pour tout $m \geq 0$, $\rho^m = 1$ si et seulement si $\chi = (t - 1)(t^2 - \alpha_k t + 1)$ divise $t^m - 1$ dans $R[t]$.
\item Pour $p \geq 3$, soit $\Psi_p \in \mathbf Z[x]$ le polynôme minimal de $2\cos(2\pi/p)$, de degré $d$. Alors $x^d\,\Psi_p(x + x^{-1}) = \Phi_p(x)$, le $p$-ième polynôme cyclotomique ; en particulier $2d = \deg \Phi_p$, l'indicatrice d'Euler de $p$.
\item Si $R = K$ est un corps de caractéristique~$0$ et $p \geq 3$, $\rho$ est d'ordre exactement $p$ si et seulement si $\Psi_p(\alpha_k) = 0$.
\end{enumerate}
\end{theoreme}
\end{encadre}

\begin{proof}
Pour le point~1, $\chi(\rho) = 0$ par le point~2 du théorème précédent, d'où une implication. Réciproquement, si $\rho^m = 1$, le reste $r = r_0 + r_1 t + r_2 t^2$ de la division de $t^m - 1$ par $\chi$, unitaire, vérifie $r(\rho) = 0$ ; appliqué à $s_k$, il donne $r_0 s_k + r_1 s_{k+1} + r_2\bigl(s_{k+2} + (1 + \alpha_k) w_k\bigr) = 0$, et les coordonnées $k + 2$, $k + 1$, $k$ donnent $r_2 = r_1 = r_0 = 0$ : le vecteur $s_k$ est cyclique.

Pour le point~2, soit $\zeta = e^{2i\pi/p}$, de sorte que $c = \zeta + \zeta^{-1} = 2\cos(2\pi/p)$. Le polynôme $T = \sum_{i \leq d} c_i\, x^{d-i}(x^2 + 1)^i$, où $\Psi_p = \sum c_i x^i$, est à coefficients entiers, de degré au plus $2d$, de terme constant $c_d = 1$, et vaut $z^d\,\Psi_p(z + z^{-1})$ en tout $z \neq 0$ ; il s'annule en $\zeta$, donc $\Phi_p$, polynôme minimal de $\zeta$ sur $\mathbf Z$, le divise : $T = \Phi_p\, g$. Le corps $\mathbf Q(c)$ est réel et ne contient pas $\zeta$, dont la partie imaginaire $\sin(2\pi/p)$ n'est pas nulle ; comme $\mathbf Q(c) \subset \mathbf Q(\zeta)$, $\deg \Phi_p = [\mathbf Q(\zeta) : \mathbf Q] = d\,[\mathbf Q(\zeta) : \mathbf Q(c)] \geq 2d$. Ainsi $g$ est constant, et $g = T(0)/\Phi_p(0) = 1$.

Pour le point~3, soit $\zeta$ une racine de $t^2 - \alpha_k t + 1$ dans une clôture algébrique $L$ de $K$ ; $\zeta \neq 0$ et $\alpha_k = \zeta + \zeta^{-1}$. La divisibilité du point~1 se lit dans $L[t]$, où $\chi = (t - 1)(t - \zeta)(t - \zeta^{-1})$ et où $t^m - 1$, pour $m \geq 1$, est à racines simples : $\rho^m = 1$ si et seulement si $\zeta^m = 1$ et $\zeta^2 \neq 1$. Si $\zeta^2 = 1$, $\rho$ est d'ordre infini et $\zeta$ n'est pas racine primitive $p$-ième de l'unité ; sinon $\rho$ et $\zeta$ ont le même ordre. Donc $\rho$ est d'ordre $p$ si et seulement si $\zeta$ est racine primitive $p$-ième, c'est-à-dire $\Phi_p(\zeta) = 0$, soit, par le point~2, $\zeta^d\,\Psi_p(\alpha_k) = 0$.
\end{proof}

\begin{remarque}
Voir \texttt{rho\_pow\_eq\_one\_iff}, \texttt{chi\_dvd\_iff}, \texttt{recip\_minpoly\_cos} et \texttt{orderOf\_rho\_eq\_iff} dans \href{\leanblob/Folder70.lean}{\texttt{Folder70.\allowbreak{}lean}}. C'est le \q{$\rho_s^p = \mathrm{id} \iff F_p(\alpha) = 0$} de la page~67, en toute dimension, avec $F_p = \Psi_p$ ; $\Psi_3 = x + 1$, $\Psi_4 = x$, $\Psi_5 = x^2 + x - 1$ redonnent le théorème précédent sur $\mathbf Q$. La caractéristique~$0$ sert deux fois : $t^m - 1$ est à racines simples, et les racines de $\Phi_p$ sont exactement les racines primitives $p$-ièmes. Pour $p = 3$, $4$, $5$, le théorème précédent vaut en toute caractéristique ; en caractéristique positive, le critère pour $p$ quelconque n'est pas démontré ici.
\end{remarque}
\section[Cote 86 : les cinq trièdres de l'icosaèdre et l'icosaèdre gauche]{Cote 86 : les cinq trièdres de l'icosaèdre et l'icosaèdre gauche\protect\verifie{Folder86}}\label{sec:86}

La cote 86, \emph{[Polyèdres réguliers] : notes manuscrites (s.d.)}, trente-deux pages, reprend l'icosaèdre comme un objet purement combinatoire. Sous la chemise \q{Cours}, la page~18 définit une permutation $\rho$ des quinze directions d'arêtes par le côté du pentagone d'un sommet opposé à l'arête, et la page~19 affirme $\rho^3 = \mathrm{id}$ (\lot{86}{1}{18}, \lot{86}{1}{19}). Ses orbites sont les cinq \q{trièdres distingués}. La page~20 montre que deux arêtes orthogonales n'ont pas de sommet commun et que les cinq arêtes d'un sommet ont des trièdres distincts (\lot{86}{1}{20}). Les pages~21 et~22 en tirent que le groupe $G$ des automorphismes opère sur les trièdres par permutations paires et munissent l'ensemble $T$ des trièdres d'une orientation canonique (\lot{86}{2}{21}, \lot{86}{2}{22}). La conclusion des pages~23 à~25 est que $G \to \mathfrak S_T$ a pour image $\operatorname{Alt}_T$ et pour noyau le sous-groupe engendré par l'antipodisme (\lot{86}{2}{23}, \lot{86}{2}{25}). Les pages~26 à~30 reconstruisent l'icosaèdre gauche $\bar\Pi = \Pi/\iota$, aujourd'hui l'hémi-icosaèdre, à partir de l'ensemble orienté $T$, et les pages~31 et~32, d'une autre encre, donnent le tableau des ensembles de drapeaux et les trois involutions sur les numérotations $(a_1, \ldots, a_5)$ (\lot{86}{2}{26}, \lot{86}{2}{30}, \lot{86}{2}{31}, \lot{86}{2}{32}).

\noindent\emph{Conventions.} Les sommets sont $\{0, \ldots, 11\}$ : $0$ et $11$ sont deux sommets opposés, $1, \ldots, 5$ et $6, \ldots, 10$ les deux pentagones de leurs voisins ; la liste des voisins est donnée une fois pour toutes, et tout le reste est calculé à partir de l'adjacence. Pour une face $\{x, y, z\}$, $\operatorname{o}(x, y, z)$ est le troisième sommet de l'autre face qui borde $\{x, y\}$ ; l'antipode $\iota x$ est l'unique sommet qui n'est ni $x$, ni un voisin de $x$, ni un voisin d'un voisin de $x$. $G$ est le groupe des bijections de l'ensemble des sommets qui conservent l'adjacence dans les deux sens. Un drapeau est un triangle orienté $(s, t, u)$ : le sommet $s$, l'arête $\{s, t\}$, la face $\{s, t, u\}$ ; il y en a $120$. Une arête est un couple de sommets adjacents, considéré à l'ordre près ; deux arêtes ont même direction si elles sont égales ou antipodales. Pour une arête $\{s, t\}$ de faces $\{s, t, u\}$ et $\{s, t, v\}$, on pose $\rho_0(s, t) = \{\operatorname{o}(s, u, t), \operatorname{o}(s, v, t)\}$, le côté $\{\Pi_{s,u}, \Pi_{s,v}\}$ de la page~18. Les numérotations de $T$ sont les bijections $\{1, \ldots, 5\} \to T$, composées à droite par les permutations des places : $(a \circ \tau)(k) = a(\tau(k))$.

\begin{enonce}[Pages 18 à 20 et 23, les trièdres distingués\piste{86-combinatorial-five-triedres}]
\begin{enumerate}
\item $\rho_0(s, t)$ est une arête et ne dépend pas de celle des deux faces que l'on appelle $u$ ; $\rho_0(t, s)$ est l'antipode de $\rho_0(s, t)$ ; si deux arêtes ont même direction, leurs images aussi. On obtient une permutation $\rho$ des quinze directions, avec $\rho^3 = \mathrm{id}$, sans point fixe, et $\rho^2\overline{\{s, t\}} = \overline{\{u, \iota v\}}$.
\item Il y a cinq orbites, les trièdres ; deux arêtes de même trièdre et de directions différentes n'ont aucun sommet commun ; en chaque sommet, les cinq arêtes ont des trièdres deux à deux distincts, et chaque trièdre est représenté. Chaque trièdre est donc une partition des douze sommets en six arêtes.
\item (Page~23) Pour une face $\{u, v, w\}$, avec $u_1 = \operatorname{o}(v, w, u)$, $v_1 = \operatorname{o}(w, u, v)$, $w_1 = \operatorname{o}(u, v, w)$, les directions $\overline{\{u, v_1\}}$, $\overline{\{v, w_1\}}$, $\overline{\{w, u_1\}}$ sont dans un même trièdre, $\overline{\{u, w_1\}}$, $\overline{\{v, u_1\}}$, $\overline{\{w, v_1\}}$ dans un autre, et ces deux trièdres et ceux des trois côtés de la face sont les cinq trièdres. Les arêtes $\{u, v\}$ et $\{v, w_1\}$ ne sont jamais dans le même trièdre.
\end{enumerate}
\end{enonce}

\begin{proof}
Ce sont des énoncés finis sur l'icosaèdre, vérifiés par le noyau de Lean (\texttt{decide}), sans évaluation compilée. Pour~(2), on étiquette les trente arêtes par $\{0, \ldots, 4\}$ et l'on vérifie que deux arêtes ont la même étiquette si et seulement si la direction de l'une est celle de l'autre, de son image par $\rho$ ou de son image par $\rho^2$ : les étiquettes sont alors les orbites, et l'étiquetage n'est qu'un nom donné à chacune.
\end{proof}

L'icosaèdre des conventions, projeté depuis le sommet $11$ : $0$ au centre, le pentagone $1, \ldots, 5$ autour, le pentagone $6, \ldots, 10$ à l'extérieur, et $11$ à l'infini, joint à $6, \ldots, 10$ par les segments radiaux. En trait épais, l'un des cinq trièdres : les six arêtes $\{0,1\}$, $\{9,11\}$, $\{3,4\}$, $\{6,7\}$, $\{2,8\}$, $\{5,10\}$, deux à deux sans sommet commun, en trois directions formées chacune de deux arêtes antipodales.
\begin{center}
\begin{tikzpicture}[x=1cm, y=1cm, every node/.style={font=\small}]
\coordinate (v0) at (0,0);
\foreach \k in {1,...,5} { \coordinate (v\k) at ({90-72*(\k-1)}:1.15); }
\coordinate (v7) at ({90-36}:2.5); \coordinate (v8) at ({90-108}:2.5); \coordinate (v9) at ({90-180}:2.5);
\coordinate (v10) at ({90-252}:2.5); \coordinate (v6) at ({90-324}:2.5);
\foreach \a/\b in {0/1,0/2,0/3,0/4,0/5,1/2,2/3,3/4,4/5,5/1,1/6,1/7,2/7,2/8,3/8,3/9,4/9,4/10,5/10,5/6,6/7,7/8,8/9,9/10,10/6} \draw[black!55] (v\a)--(v\b);
\foreach \k/\ang in {7/54,8/-18,9/-90,10/-162,6/126} { \draw[black!55] (v\k)--(\ang:3.15); \node[black!55, font=\scriptsize] at (\ang:3.4) {$11$}; }
\foreach \a/\b in {0/1,3/4,6/7,2/8,5/10} \draw[line width=1.6pt] (v\a)--(v\b);
\draw[line width=1.6pt] (v9)--(-90:3.15);
\foreach \k in {0,...,10} \fill (v\k) circle (1.5pt);
\node[below right=-1pt] at (v0) {$0$};
\foreach \k in {1,...,5} { \node at ({90-72*(\k-1)+20}:1.3) {$\k$}; }
\foreach \k/\ang in {7/54,8/-18,9/-90,10/-162,6/126} { \node at (\ang+12:2.75) {$\k$}; }
\end{tikzpicture}
\end{center}

\begin{encadre}
\begin{theoreme}[Grothendieck, pages 20 à 25, l'action sur les trièdres\piste{86-combinatorial-five-triedres}]
\begin{enumerate}
\item Un automorphisme est déterminé par l'image du drapeau $(0, 1, 2)$, et tout drapeau est l'image de $(0, 1, 2)$ par un automorphisme : $G$ a $120$ éléments.
\item Tout automorphisme $g$ commute à $\iota$ et à $\rho$, et l'application qui envoie le trièdre d'une arête $a$ sur celui de $g(a)$ définit un homomorphisme $G \to \mathfrak S_T$.
\item Son image est contenue dans $\operatorname{Alt}_T$ et lui est égale.
\item Son noyau est $\{1, \iota\}$.
\end{enumerate}
\end{theoreme}
\end{encadre}

\begin{proof}
(1) Si $g$ conserve l'adjacence, $g(\operatorname{o}(x, y, z)) = \operatorname{o}(gx, gy, gz)$, car $\operatorname{o}(x, y, z)$ est l'unique voisin commun de $x$ et $y$ distinct de $z$. Les douze sommets s'obtiennent à partir de $0$, $1$, $2$ par neuf applications de $\operatorname{o}$ ; $g$ est donc déterminé par $(g0, g1, g2)$. Réciproquement, pour chaque drapeau $(x, y, z)$, la même suite d'applications de $\operatorname{o}$ définit une application dont on vérifie qu'elle est bijective et conserve l'adjacence. (2) $\iota x$ est caractérisé par l'adjacence, donc $g\iota = \iota g$. Comme $\rho_0(s, t)$ est formé de deux valeurs de $\operatorname{o}$ et ne dépend pas du choix de $u$, $g$ envoie $\rho_0(s, t)$ sur $\rho_0(gs, gt)$ ; $g$ conserve donc la relation \q{même trièdre}, et l'action sur les cinq étiquettes est bien définie et multiplicative. (3) et (4) Par~(1), tout $g$ est l'automorphisme associé à un drapeau, et la permutation de $T$ qu'il induit se calcule à partir de ce drapeau. On vérifie sur les $120$ drapeaux que ces permutations sont paires, qu'elles sont au nombre de $60$, ce qui est l'ordre de $\operatorname{Alt}_T$, et que seuls les drapeaux $(0, 1, 2)$ et $(\iota 0, \iota 1, \iota 2)$ donnent l'identité.
\end{proof}

\begin{remarque}
La démonstration de la page suit un autre chemin : la parité par les générateurs $\bar\sigma_0$, $\bar\sigma_1$, $\bar\sigma_2$ et le cas $n \equiv 1 \pmod 4$ du polygone, l'image par les ordres $6$, $10$ et $4$ des images des stabilisateurs d'une face, d'un sommet et d'une arête. Ici l'énoncé est établi par le décompte des drapeaux ; seule la parité des symétries d'un pentagone, vues comme permutations de ses sommets, est vérifiée pour elle-même (énoncé suivant). La vérification confirme le calcul de $\rho^2$ et de $\rho^3$, que la page ne détaille pas, et la correction de la lecture à la page~23 : avec $\{u, v\}$, la page met dans un même triple deux arêtes de trièdres différents. Les deux choix de $u$ dans la définition de $\rho_0$ donnent la même arête, et le passage de $s$ à $t$ donne l'arête antipodale : $\rho$ est bien défini sur les directions, comme la page l'affirme.
\end{remarque}

\begin{encadre}
\begin{theoreme}[D'après les pages 21 et 26 à 32, forme complétée par l'édition, l'icosaèdre gauche par l'ensemble orienté $T$\piste{86-hemi-icosahedron-five-set-model}]
À un drapeau $(s, t, u)$, avec $v = \operatorname{o}(s, t, u)$, associons la numérotation $\nu(s, t, u)$ de $T$ formée des trièdres des arêtes $\{s, t\}$, $\{s, v\}$, $\{s, \Pi_{s,v}\}$, $\{s, \Pi_{s,u}\}$, $\{s, u\}$ : les cinq arêtes de $s$ dans l'ordre du pentagone, à partir de $t$, dans le sens qui s'éloigne de $u$ (page~30).
\begin{enumerate}
\item Pour $g \in G$, $\nu(gs, gt, gu)$ est $\nu(s, t, u)$ composée à gauche par la permutation de $T$ induite par $g$.
\item Toutes les numérotations $\nu(s, t, u)$ ont la même parité ; elles définissent donc une orientation $\varpi$ de $T$ qui ne dépend d'aucun choix. Toute numérotation compatible avec $\varpi$ est de la forme $\nu(s, t, u)$, et $\nu(s, t, u) = \nu(s', t', u')$ si et seulement si $(s', t', u')$ est $(s, t, u)$ ou $(\iota s, \iota t, \iota u)$. Les $60$ drapeaux de $\bar\Pi$ sont ainsi les $60$ numérotations compatibles avec $\varpi$.
\item Changer le sommet, l'arête ou la face d'un drapeau, c'est-à-dire $(s, t, u) \mapsto (t, s, u)$, $(s, u, t)$, $(s, t, v)$, revient à composer $\nu$ à droite par
\[ \tau_0 = (2\,4)(3\,5), \qquad \tau_1 = (1\,5)(2\,4), \qquad \tau_2 = (2\,5)(3\,4) \]
(permutations des places) : $\sigma_0(a) = (a_1, a_4, a_5, a_2, a_3)$, $\sigma_1(a) = (a_5, a_4, a_3, a_2, a_1)$, $\sigma_2(a) = (a_1, a_5, a_4, a_3, a_2)$.
\item Le $\sigma_1$ de la page~31, $(a_2, a_1, a_5, a_4, a_3)$, est $\tau_1' = (1\,2)(3\,5) = \tau_2\tau_1\tau_2$, et $\tau_2$ commute à $\tau_0$. Le triple de la page est donc l'action des trois mêmes changements sur la numérotation $(s, t, u) \mapsto \nu(s, t, v)$.
\item Avec le triple de la page, $\sigma_1\sigma_0 : a \mapsto (a_4, a_1, a_3, a_2, a_5)$, $\sigma_2\sigma_1 : a \mapsto (a_2, a_3, a_4, a_5, a_1)$ et $\sigma_0\sigma_2 : a \mapsto (a_1, a_3, a_2, a_5, a_4)$ sont d'ordres $3$, $5$ et $2$, et $\sigma_0\sigma_1$ est d'ordre $3$.
\item Deux drapeaux ont le même sommet dans $\bar\Pi$ si et seulement si leurs numérotations tracent le même pentagone sur $T$ ; la même arête si et seulement si elles donnent la même partition $\{a_1\} \sqcup \{a_2, a_3\} \sqcup \{a_4, a_5\}$ de type $(2, 2, 1)$ ; la même face si et seulement si elles donnent la même partie $\{a_1, a_3, a_5\}$.
\item Les symétries du pentagone $1\,2\,3\,4\,5$ sont des permutations paires des places. Par suite une numérotation de $T$ trace le pentagone d'un sommet de $\bar\Pi$ si et seulement si elle est compatible avec $\varpi$. On obtient $6$ pentagones, $15$ partitions de type $(2, 2, 1)$, c'est-à-dire toutes, et les $10$ parties à trois éléments.
\end{enumerate}
\end{theoreme}
\end{encadre}

\begin{proof}
(1) Les cinq arêtes de $s$ s'écrivent avec $\operatorname{o}$, que $g$ respecte, et $g$ opère sur les trièdres par l'énoncé précédent. (2) Par~(1), $\nu(g0, g1, g2)$ est la permutation de $T$ induite par $g$, composée avec $\nu(0, 1, 2)$ ; avec l'étiquetage choisi, $\nu(0, 1, 2)$ est la permutation des places $\tau_2 = (2\,5)(3\,4)$, qui est paire, et toute permutation paire s'obtient ainsi par la surjectivité sur $\operatorname{Alt}_T$. Deux drapeaux $g(0,1,2)$ et $h(0,1,2)$ ont la même numérotation si et seulement si $g^{-1}h$ est dans le noyau $\{1, \iota\}$, c'est-à-dire $h = g$ ou $h = g\iota$, et $g\iota(0,1,2) = \iota g(0,1,2)$. (3) Les changements de drapeau sont $g \mapsto g s_i$, où $s_0$, $s_1$, $s_2$ sont les automorphismes qui envoient $(0, 1, 2)$ sur $(1, 0, 2)$, $(0, 2, 1)$, $(0, 1, 5)$ ; par~(2), il suffit de vérifier les trois égalités de permutations $\pi(s_i)\,\nu(0,1,2) = \nu(0,1,2)\,\tau_i$, où $\pi(s_i)$ est la permutation de $T$ induite. (4) et (5) sont des calculs de permutations ; par~(3), $\nu(\sigma_2(\sigma_1 r)) = \nu(r)\tau_1\tau_2 = \nu(\sigma_2 r)\,\tau_2\tau_1\tau_2$, puisque $\tau_2^2 = 1$. (6) Par~(1), en remplaçant les deux drapeaux par leurs images sous $g^{-1}$, où $g$ envoie $(0, 1, 2)$ sur le premier, on se ramène au cas où le premier est $(0, 1, 2)$ : les trois conditions sur les drapeaux sont conservées par $g$, et les trois conditions sur les numérotations par la composition à gauche avec une permutation de $T$. Le cas du drapeau $(0, 1, 2)$ se vérifie sur les $120$ drapeaux. (7) On vérifie que les numérotations qui tracent le pentagone $1\,2\,3\,4\,5$ sont les dix éléments du groupe diédral et que ces dix permutations sont paires ; si deux numérotations $a$, $b$ tracent le même pentagone, $a^{-1}b$ trace le pentagone standard, donc $a$ et $b$ ont même parité. Les trois décomptes sont des calculs sur les $120$ drapeaux.
\end{proof}

\begin{remarque}
L'orientation $\varpi$ est celle des pages~21 et~22 : la parité de $\nu(s, t, u)$ ne dépend ni du drapeau ni du sens de parcours, grâce au cas $n \equiv 1 \pmod 4$ du pentagone, dont les dix symétries sont paires ; pour un hexagone, la symétrie qui échange les extrémités de deux côtés opposés est un produit de trois transpositions, donc impaire. Les pages~26 à~32 donnent les bijections et les ensembles de la page~31 sans les incidences ; les incidences du point~6 et les points~4 et~5 sont de l'édition. La vérification confirme les remarques de la lecture sur les pages~31 et~32. Le $\sigma_1$ de la page n'est pas celui que donne le dictionnaire de la page~30 ; il s'en déduit par conjugaison par $\sigma_2$, et correspond au dictionnaire qui lit le pentagone de $s$ à partir de $t$ en direction de $u$. Les deux triples définissent donc des ensembles à opérateurs isomorphes. L'étiquette \q{$\sigma = \sigma_0\sigma_1$} de la page~32 accompagne la valeur de $\sigma_0\sigma_2$, d'ordre~$2$. L'étiquetage des trièdres a été choisi de sorte que $\varpi$ soit la classe des numérotations paires ; un autre étiquetage changerait la classe, non l'énoncé.
\end{remarque}

Ne sont pas démontrés ici : les axiomes des polyèdres combinatoires de la page~2 et le théorème de pleine fidélité des pages~10 à~16, l'icosaèdre étant donné par sa liste de voisins ; l'identification des trièdres aux repères orthogonaux et aux cinq octaèdres inscrits de l'icosaèdre régulier ; la décomposition $G = \{1, \iota\} \times G^{+}$ et l'isomorphisme $G^{+} \simeq \operatorname{Alt}_T$ du corollaire de la page~26, faute d'une définition de l'orientation de $\Pi$ ; la description des arêtes par les triplets $(t, \gamma, \alpha)$ de la page~27 et les incidences a) à d) des pages~28 et~29 sous cette forme, que l'on a remplacées par les partitions et les parties à trois éléments de la page~31 ; les lignes $\vec A$, $A^{\uparrow}$, $A^{\wedge}$, $\tilde S$, $\tilde A$, $\tilde F$ du tableau de la page~31 ; la génération de $\operatorname{Alt}_5$ par $\tau_0$, $\tau_1$, $\tau_2$ et leur action simplement transitive sur les $60$ numérotations, qui suivraient de la connexité du graphe des drapeaux, non vérifiée.
\section[Cote 72 : réalisations par pseudo-réflexions d'un polytope régulier]{Cote 72 : réalisations par pseudo-réflexions d'un polytope régulier\protect\verifie{Folder72}}\label{sec:72}

La cote 72, \emph{Polyèdres réguliers et hyperpolyèdres réguliers (calculs en dimension quelconque)}, que l'inventaire date \q{[à partir de 1978]}, étudie les réalisations du polytope régulier universel de rang $n+1$ par des pseudo-réflexions $\tau_i = \mathrm{id} + a'_i \otimes a_i$ ($0 \leq i \leq n$) d'un module $E$ de rang $n+2$ sur une base quelconque, les $\tau_i$ non consécutifs commutant. Avec le point de départ $s_0$, $s_{i+1} = \tau_i s_i$ et $a_i = s_{i+1} - s_i$, les accouplements sont $\langle a_{i-1}, a'_i\rangle = 1$, $\langle a_i, a'_i\rangle = \mu_i = \lambda_i - 1$, $\langle a_{i+1}, a'_i\rangle = \beta_i$, les autres nuls. On travaille ici dans la base $(s_0, a_0, \dots, a_n)$ de $E = R^{n+2}$, $R$ un anneau commutatif ; $\pi$ est la première coordonnée et $\tilde c$ l'unique vecteur annulé par tous les $a'_i$ dont la coordonnée sur $a_n$ vaut~$1$, obtenu par substitution remontante.

Page~37, $\mathcal U_\rho = \operatorname{Spec} \mathcal O_S[T]_{(1+\rho T)}$, de loi $\lambda * \lambda' = \lambda + \lambda' + \rho\lambda\lambda'$, opère par $u_\lambda = \mathrm{id} + \lambda\, \pi \otimes \tilde c$, où $\rho = \pi(\tilde c)$ ; le \q{Théorème} de la page~38 affirme sans démonstration que $\mathbb G_m \times \mathcal U_\rho \to \operatorname{Aut}(E, (\tau_i))$ est un isomorphisme et que $D_0 \smallsetminus \{c, d\}$, $D_0 = H_1 \cap \dots \cap H_n$, est un torseur sous $\mathcal U_\rho$ trivialisé par $s_0$ (\lot{72}{2}{38}). Les pages~87 et~88 le reprennent sous forme projective.

\begin{theoreme}[D'après les pages 37 et 38, en coordonnées, sur les points\piste{72-automorphisms-deform-gm-to-ga}]
Les $\lambda \in R$ avec $1 + \rho\lambda$ inversible forment un groupe commutatif $\mathcal U_\rho(R)$ ; $\lambda \mapsto 1 + \rho\lambda$ est surjectif sur les inversibles de toute $R$-algèbre si et seulement si $\rho$ est inversible, et $\mathcal U_0 = \mathbb G_a$. On a $u_\lambda u_{\lambda'} = u_{\lambda * \lambda'}$, $\det u_\lambda = 1 + \rho\lambda$, et un endomorphisme de $E$ commute à tous les $\tau_i$ si et seulement s'il s'écrit $c + t\, \pi \otimes \tilde c$, avec $(c, t)$ unique ; il est inversible si et seulement si $c$ et $c + t\rho$ le sont. D'où $R^\times \times \mathcal U_\rho(R) \simeq \operatorname{Aut}(E, (\tau_i))$, $(c, \lambda) \mapsto c\, u_\lambda$. Les points de $D_0$ sont les $a s_0 + t \tilde c$, et ceux qui évitent $c$ et $d$, normalisés par $\langle s, a'_0\rangle = 1$, sont exactement les $u_\lambda s_0 = s_0 + \lambda \tilde c$, chacun pour un seul $\lambda$, avec $u_\mu(u_\lambda s_0) = u_{\lambda * \mu} s_0$.
\end{theoreme}

\noindent L'énoncé tient sur les points, pour tout anneau : voir \texttt{forall\_surjective\_iff}, \texttt{u\_mul}, \texttt{det\_u}, \texttt{commute\_iff}, \texttt{isUnit\_iff}, \texttt{centraliserEquiv}, \texttt{mem\_startPoints\_iff} et \texttt{u\_e0\_injective} dans \href{\leanblob/Folder72.lean}{\texttt{Folder72.\allowbreak{}lean}}. Le test de la réciproque est l'anneau des nombres duaux, où $1 + \varepsilon$ n'est atteint que si $\rho$ est inversible. Pour $n = 1$, $\rho = \mu_0\mu_1 - \beta_0$, soit $4 - \beta_0$ pour des réflexions, comme à la page~41.

Les points de $D_0$ sont la direction $c$ de $\tilde c$, le centre, et les $s_0 + \lambda\tilde c$ ; le point $d = D_0 \cap C$ est celui où $\pi(s_0 + \lambda\tilde c) = 1 + \rho\lambda$ s'annule. Comme $u_\mu(s_0 + \lambda\tilde c) = s_0 + (\lambda * \mu)\tilde c$ et $\lambda * \mu + 1/\rho = (1 + \rho\mu)(\lambda + 1/\rho)$ quand $\rho$ est inversible, $u_\mu$ agit sur la coordonnée $\lambda$ par l'homothétie de centre $d$ et de rapport $1 + \rho\mu$ ; pour $\rho = 0$, $d$ et $c$ se confondent et $u_\mu$ est la translation de~$\mu$ (figure~\ref{fig:72-torseur}).

\begin{figure}[htbp]
\centering
\begin{tikzpicture}[x=2.2cm, y=1cm, >=stealth, every node/.style={font=\small}]
\begin{scope}
\draw[black!55, <->] (-2.25,0) -- (3.2,0) node[right] {$c$};
\draw[fill=white] (-1,0) circle (2.2pt);
\node[below=3pt] at (-1,0) {$d$};
\node[below=16pt, black!60] at (-1,0) {\footnotesize $\lambda = -1/\rho$};
\foreach \x/\l in {0/s_0, 0.6/u_\mu s_0, 1.56/u_\mu^2 s_0} { \fill (\x,0) circle (2pt); \node[below=3pt] at (\x,0) {$\l$}; }
\draw[->, black!70, shorten >=3pt, shorten <=3pt] (0,0) to[bend left=40] (0.6,0);
\draw[->, black!70, shorten >=3pt, shorten <=3pt] (0.6,0) to[bend left=40] (1.56,0);
\node[anchor=west] at (-2.25,1.05) {$\rho$ inversible : homothétie de centre $d$, de rapport $1 + \rho\mu$ ; $\mathcal U_\rho \simeq \mathbb G_m$};
\end{scope}
\begin{scope}[yshift=-2.6cm]
\draw[black!55, <->] (-2.25,0) -- (3.2,0) node[right] {$c = d$};
\foreach \x/\l in {0/s_0, 0.8/u_\mu s_0, 1.6/u_\mu^2 s_0} { \fill (\x,0) circle (2pt); \node[below=3pt] at (\x,0) {$\l$}; }
\draw[->, black!70, shorten >=3pt, shorten <=3pt] (0,0) to[bend left=40] (0.8,0);
\draw[->, black!70, shorten >=3pt, shorten <=3pt] (0.8,0) to[bend left=40] (1.6,0);
\node[anchor=west] at (-2.25,1.05) {$\rho = 0$ : translation de $\mu$ ; $\mathcal U_0 = \mathbb G_a$};
\end{scope}
\end{tikzpicture}
\caption{La droite projective $D_0$ des points de départ, dans la carte $\langle s, a'_0\rangle = 1$, où $s_0 + \lambda\tilde c$ a pour coordonnée $\lambda$ et où le centre $c$ est à l'infini. En haut, $\rho$ inversible : $D_0 \smallsetminus \{c, d\}$ est l'orbite de $s_0$, et $u_\mu$ en multiplie la distance à $d$ par $1 + \rho\mu$. En bas, $\rho = 0$ : $c = d$, et $D_0 \smallsetminus \{c\}$ est une droite affine sur laquelle $\mathcal U_0$ agit par translations. Les points sont dessinés pour $\rho = 1$, $\mu = 0{,}6$, puis $\rho = 0$, $\mu = 0{,}8$.}
\label{fig:72-torseur}
\end{figure}

Aux pages~79 à~82, sur un corps $k$, la cote décrit les sous-espaces invariants (\lot{72}{4}{79}). Avec $Z'_i = H_0 \cap \dots \cap H_i$ et $Z^*_i = \operatorname{Lin}(h_{i+1}, \dots, h_n)$, $h_i = k a_i$ et $H_i = \operatorname{Ker} a'_i$ :

\begin{theoreme}[Grothendieck, page 79\piste{72-invariant-subspaces-string}]
Sur un corps, les $\mu_i$ quelconques (caractéristique~$2$ comprise), un sous-espace de $E$ est stable par tous les $\tau_i$ si et seulement s'il est $0$, $E$, la droite $k\tilde c$ du centre, l'hyperplan $C$ d'équation $\pi = 0$, ou bien $Z'_i$ ou $Z^*_i$ pour un $i < n$ tel que $\beta_i = 0$.
\end{theoreme}

\noindent La vérification porte sur l'énoncé tel quel (\texttt{invariant\_iff} dans \href{\leanblob/Folder72.lean}{\texttt{Folder72.\allowbreak{}lean}}) et sur le corollaire~(c) de la page~80 (\texttt{invariant\_iff\_of\_ne\_zero}). Pour $i < n$, $Z^*_i \subset Z'_i$ si et seulement si $\beta_i = 0$ (\texttt{Zs\_le\_Zp\_iff}) : c'est le \q{$\in$} de la marge de la page~79 que la lecture retient, non le \q{$\notin$} de la page~81.

Aux pages~80 à~82, la cote en tire l'irréductibilité de la représentation sur l'hyperplan $C$ ; le d) barré de la page~80 demande $\rho \neq 0$ et tous les $\beta_i \neq 0$, le c) de la page~82 omet $\rho \neq 0$.

\begin{theoreme}[D'après les pages 80 à 82, forme complétée par l'édition\piste{72-invariant-subspaces-string}]
Sur un corps, les $\mu_i$ quelconques, les sous-espaces de $C$ stables par tous les $\tau_i$ sont $0$, $C$, la droite $k\tilde c$ si $\rho = 0$, et, pour $i < n$ tel que $\beta_i = 0$, $Z^*_i$ et $Z'_i$ lorsque $Z'_i \subset C$. Si tous les $\beta_i$ sont non nuls, il ne reste que $0$, $C$ et, si $\rho = 0$, $k\tilde c$. La représentation sur $C$ est donc irréductible si et seulement si tous les $\beta_i$ sont non nuls et, pour $n \geq 1$, $\rho \neq 0$ ; pour $n = 0$, $C$ est une droite.
\end{theoreme}

\noindent Voir \texttt{invariant\_le\_Vh\_iff}, \texttt{invariant\_le\_Vh\_iff\_of\_ne\_zero} et \texttt{irreducible\_on\_C\_iff} dans \href{\leanblob/Folder72.lean}{\texttt{Folder72.\allowbreak{}lean}}. On intersecte la liste de \texttt{invariant\_iff} avec $C$ : $E \not\subset C$ puisque $\pi(s_0) = 1$, $k\tilde c \subset C$ si et seulement si $\pi(\tilde c) = \rho = 0$, et $Z^*_i \subset C$ toujours. Pour la nécessité, $Z^*_i$ contient $h_{i+1}$ et non $h_0$, qui est dans $C$ ; si $\rho = 0$ et $n \geq 1$, $k\tilde c$ est une droite de $C$ distincte de $C$, car $h_0 \in C$ n'est pas multiple de $\tilde c$, dont la dernière coordonnée vaut $1$. Le seul \q{tous les $\beta_i \neq 0$} du c) de la page~82 ne suffit donc pas : $\rho = 0$ laisse la droite invariante $k\tilde c \subset C$.

Aux pages~96 à~100, sur un anneau $k$, pour un $k$-module $E$, des pseudo-réflexions $\tau_i = \mathrm{id} + a'_i \otimes a_i$ et $s_0 \in E$, avec $\nu_i = \langle s_0, a'_0\rangle\langle a_0, a'_1\rangle \cdots \langle a_{i-1}, a'_i\rangle$, la cote démontre l'équivalence des conditions (A) (commutation des $\tau_i$ non consécutifs, $\tau_i s_0 = s_0$ pour $i \geq 1$, liberté des $s_i$) et (B) (accouplements nuls hors des indices consécutifs, $\langle s_0, a'_i\rangle = 0$ pour $i \geq 1$, liberté de $(s_0, a_0, \dots, a_n)$, $\nu_n$ inversible) ; la remarque de la page~102 la reprend avec des bases de $E$ (\lot{72}{5}{96}).

\begin{theoreme}[D'après les pages 96 à 100 et 102\piste{72-pinned-realisations-over-base}]
Sur tout anneau commutatif, (Ā) \q{les $\tau_i$ non consécutifs commutent, $\tau_i s_0 = s_0$ pour $1 \leq i \leq n$, $(s_0, \dots, s_{n+1})$ est une base de $E$} équivaut à (\ensuremath{\bar B}) \q{$\langle a_i, a'_j\rangle = 0$ pour $i, j$ non consécutifs, $\langle s_0, a'_i\rangle = 0$ pour $1 \leq i \leq n$, $(s_0, a_0, \dots, a_n)$ est une base de $E$, $\nu_n$ est inversible}.
\end{theoreme}

\noindent L'énoncé tient, sans l'hypothèse que les $a'_i$ soient partout non nulles : voir \texttt{condA\_iff\_condB} dans \href{\leanblob/Folder72.lean}{\texttt{Folder72.\allowbreak{}lean}}. Sous (Ā), $s_{i+1} - s_i = \langle s_i, a'_i\rangle a_i$ et les $s_i$ forment une base, donc chaque $\langle s_i, a'_i\rangle$ est inversible, ce qui tient lieu de cette hypothèse dans le passage de la commutation à $\langle a_i, a'_j\rangle = 0$ ; sous (10) et (11), $\langle s_i, a'_i\rangle = \nu_i$, et dans les deux sens la matrice de passage est triangulaire à diagonale inversible.

\begin{theoreme}[Énoncé de l'édition, d'après la marge de la page 13 et les pages 91 à 100]
Une réalisation qui vérifie (\ensuremath{\bar B}), normalisée par $\langle s_0, a'_0\rangle = 1$ et $\langle a_{i-1}, a'_i\rangle = 1$, est isomorphe, par un unique isomorphisme qui envoie $s_0$ sur $e_0$ et conjugue les $\tau_i$, à la réalisation en coordonnées de paramètres $\mu_i = \langle a_i, a'_i\rangle$, $\beta_i = \langle a_{i+1}, a'_i\rangle$. Celle-ci vérifie (\ensuremath{\bar B}) pour tous $\mu$, $\beta$, et $\tau_i$ y est inversible si et seulement si $\lambda_i = 1 + \mu_i$ l'est. Une application linéaire compatible à $s_0$ et aux $\tau_i$ entre deux réalisations normalisées force l'égalité des $(\mu_i, \beta_i)$. Les réalisations épinglées non dégénérées sur $E$ libre de rang $n+2$ sont donc classées, rigidement, par les $2n+1$ paramètres $(\lambda_0, \beta_0, \lambda_1, \dots, \beta_{n-1}, \lambda_n)$, les $\lambda_i$ inversibles et les $\beta_i$ quelconques.
\end{theoreme}

\noindent Les déclarations \texttt{pinned\_classification}, \texttt{pinned\_rigid}, \texttt{model\_condB}, \texttt{model\_isUnit\_iff} et \texttt{invariants\_eq} vérifient l'énoncé. Les invariants se lisent sur $(\tau_i, s_0)$ seuls : normalisée, $a_i = s_{i+1} - s_i$, $\tau_i a_i = \lambda_i a_i$ et $\tau_i a_{i+1} = a_{i+1} + \beta_i a_i$.

Aux pages~96 à~100, \q{libre} s'entend au sens fort de la page~103 : une famille est libre si elle est indépendante et engendre un facteur direct.

\begin{theoreme}[D'après les pages 96 à 100 et 103\piste{72-pinned-realisations-over-base}]
Sur tout anneau commutatif $k$ et pour tout $k$-module $E$, libre ou non, (A) \q{les $\tau_i$ non consécutifs commutent, $\tau_i s_0 = s_0$ pour $1 \leq i \leq n$, $(s_0, \dots, s_{n+1})$ est libre} équivaut à (B) \q{$\langle a_i, a'_j\rangle = 0$ pour $i, j$ non consécutifs, $\langle s_0, a'_i\rangle = 0$ pour $1 \leq i \leq n$, $(s_0, a_0, \dots, a_n)$ est libre, $\nu_n$ est inversible}, \q{libre} au sens fort. Au sens faible (indépendance seule), (A) n'entraîne pas (13) : sur $\mathbb Z$, $n = 0$, $s_0 = e_0$, $a_0 = e_1$, $a'_0 = 2e_0^*$, la famille $(s_0, s_1) = (e_0, e_0 + 2e_1)$ est indépendante et $\nu_0 = 2$. Enfin (Ā) force $E$ à être libre.
\end{theoreme}

\noindent Voir \texttt{condAs\_iff\_condBs}, \texttt{not\_condAw\_imp} et \texttt{free\_of\_condA} dans \href{\leanblob/Folder72.lean}{\texttt{Folder72.\allowbreak{}lean}}. On se ramène au sous-module $N$ engendré par la famille, où elle est une base, et au théorème précédent. Sous (A), la coordonnée sur $s_{i+1}$ de la projection sur $N$ parallèlement au supplémentaire vaut $1$ en $s_{i+1}$ et $0$ en $s_i$, donc $\langle s_i, a'_i\rangle$ est inversible et $a_i \in N$ ; les $\tau_i$ se restreignent à $N$. Sur un $E$ localement libre non libre, il n'y a donc pas de point de départ global : l'existence des pages~102 à~105 n'est que locale.

La proposition des pages~102 à~105 ne demande b) que pour $i < j$ : c'est la moitié triangulaire de (10), qui intervient dans les conditions (\ensuremath{\bar B}$'$) du corollaire des pages~97 et~98 ; (\ensuremath{\bar B}) est (\ensuremath{\bar B}$'$) plus l'autre moitié de (10), qui ne fait pas intervenir $s_0$.

\begin{theoreme}[D'après les pages 102 à 105\piste{72-pinned-realisations-over-base}]
Sur un anneau local $k$, il existe $s_0$ vérifiant (\ensuremath{\bar B}$'$) \q{$\langle a_i, a'_j\rangle = 0$ pour $i + 2 \leq j$, $\langle s_0, a'_i\rangle = 0$ pour $1 \leq i \leq n$, $(s_0, a_0, \dots, a_n)$ est une base, $\nu_n$ est inversible} si et seulement si a) $(a_0, \dots, a_n)$ se complète en une base par un vecteur, a$'$) $x \mapsto (\langle x, a'_i\rangle)_{0 \leq i \leq n}$ est surjective, b) $\langle a_i, a'_j\rangle = 0$ pour $i + 2 \leq j$, c) les $\langle a_i, a'_{i+1}\rangle$ sont inversibles ; avec en plus $\langle a_j, a'_i\rangle = 0$ pour $i + 2 \leq j$, il existe $s_0$ vérifiant (Ā). Si $E$ est libre de rang $n + 2$, a) et a$'$) au sens \q{strictement libre} de la page (dans $E$ et dans $E^\vee$) donnent ces formes-ci. Sur un anneau quelconque, si $(v, a_0, \dots, a_n)$ est une base et $\varphi$ la coordonnée sur $v$, $s_0$ vérifie (\ensuremath{\bar B}$'$) si et seulement si $s_0$ est dans le noyau commun $F$ des $a'_i$ ($1 \leq i \leq n$) et si $\langle s_0, a'_0\rangle$ et $\varphi(s_0)$ sont inversibles.
\end{theoreme}

\noindent Voir \texttt{exists\_condB'\_iff}, \texttt{exists\_condA\_iff}, \texttt{exists\_completion}, \texttt{surjective\_of\_strict}, \texttt{exists\_condB'\_of\_strict} et \texttt{condB'\_iff\_of\_basis} dans \href{\leanblob/Folder72.lean}{\texttt{Folder72.\allowbreak{}lean}}. La dernière assertion est le \q{$s_0 \notin D$, $s_0 \notin \Delta$} de la page~105 : $(s_0, a_0, \dots, a_n)$ est triangulaire dans $(v, a_0, \dots, a_n)$, de diagonale $(\varphi(s_0), 1, \dots, 1)$, et $\nu_n = \langle s_0, a'_0\rangle c_0 \cdots c_{n-1}$. Par b) et c), une substitution remontante sur $a_{n-1}, \dots, a_0$ donne $s \in F$ avec $\varphi(s) = \varphi(v) = 1$, et a$'$) donne $t \in F$ avec $\langle t, a'_0\rangle = 1$ ; dans un anneau local, l'un de $t$, $s$, $s + t$ convient, ce qui vaut même si le corps résiduel est $\mathbb F_2$. Pour la nécessité de a$'$), la matrice des $\langle x, a'_j\rangle$ pour $x = s_0, a_0, \dots, a_{n-1}$ est triangulaire de déterminant $\nu_n$, comme à la page~103. Pour a), le supplémentaire de $k(a_0, \dots, a_n)$ est projectif de type fini sur un anneau local, donc libre, de rang~$1$.

Ne sont pas démontrés ici : le schéma en groupes $\mathcal U_\rho$ et sa lissité, l'énoncé projectif sur une base (automorphismes de $X = \mathbf P(E)$ commutant aux $\tau_i$ projectifs), le torseur des drapeaux de la page~87, les comptes des pages~79 et~80, et l'existence du point de départ sous forme locale sur un anneau quelconque (après localisation en un premier, ou sur un recouvrement de Zariski), que l'énoncé sur un anneau local ne formule qu'aux anneaux locaux.