% Engendré par nonverifies.mjs — ne pas éditer à la main.
\section*{Énoncés non vérifiés en Lean}\addcontentsline{toc}{section}{Énoncés non vérifiés en Lean}

Les 127 énoncés marqués \textcolor{piste}{\ensuremath{\lozenge}} dans la marge, dans l'ordre du texte : la cote, l'énoncé tel que le titre le donne, la vérification autre que Lean, la page. La vérification est \emph{publié} quand la recherche bibliographique a trouvé l'énoncé imprimé, \emph{réfuté} quand un contre-exemple le contredit, \emph{problème ouvert} quand il est posé dans l'article des problèmes ouverts, \emph{calcul} quand un programme du dossier \texttt{computations/} le teste sur de petits cas, avec son verdict (accord, désaccord, ou non testable par calcul) ; un tiret signale qu'aucune vérification n'est prévue.

{\small
\begin{longtable}{@{}l>{\raggedright\arraybackslash}p{0.52\linewidth}>{\raggedright\arraybackslash}p{0.2\linewidth}r@{}}
\toprule
Cote & Énoncé & Vérification & Page\\
\midrule
\endhead
16 & page 49, variantes en dimension critique & problème ouvert & \pageref{nv:1}\\
36 & D'après les pages 9 à 16, forme corrigée par l'édition, théorème de Griffiths par voie $\ell$-adique & --- & \pageref{nv:2}\\
36 & pages 60 à 70, défaut des cycles invariants en $H^1$ & --- & \pageref{nv:3}\\
36 & pages 73 à 76, orthogonalité sur une base adique régulière & --- & \pageref{nv:4}\\
12 & pages 115 à 119, poids et niveau d'une immersion & problème ouvert & \pageref{nv:5}\\
13 & pages 33 et 34, invariants d'un double réseau & --- & \pageref{nv:6}\\
60 & pages 38 à 58, moyenne sur l'inertie et dualité & --- & \pageref{nv:7}\\
31 & pages 64 à 70, majoration de la dimension cohomologique ; voir M.~Artin, SGA~4, exposé~X, théorème~4.1 (1973) & publié & \pageref{nv:8}\\
31 & page 22, minoration de la dimension cohomologique & problème ouvert & \pageref{nv:9}\\
129 & page 95, annulation de $\mathrm{Ext}^2$ & problème ouvert & \pageref{nv:10}\\
161-2 & pages 39, 41 et 42, deux topos classifiants non cohérents & problème ouvert & \pageref{nv:11}\\
161-2 & D'après les pages 47 à 49, anneaux de caractéristique définie & --- & \pageref{nv:12}\\
161-2 & D'après les pages 92 à 95, le corps universel, forme complétée par l'édition & --- & \pageref{nv:13}\\
1 & Pages 71 et 72, opérateurs compacts & calcul, non testable & \pageref{nv:14}\\
43 & pages 165 à 169, $\mathrm{Ext}^1(\mathbf G_a, \mathbf Z/p\mathbf Z)$ et perfection & --- & \pageref{nv:15}\\
43 & D'après les pages 70 à 74, forme corrigée par l'édition, concentration de la cohomologie locale & --- & \pageref{nv:16}\\
101 & pages 10, 14 et 15, dualité locale en dimension deux & --- & \pageref{nv:17}\\
125 & pages 2, 4 et 7, dimension cohomologique du complémentaire & publié & \pageref{nv:18}\\
32 & pages 10 et 11, noyau de l'image réciproque et indice & --- & \pageref{nv:19}\\
58 & pages 40 à 43, permanence de la condition de Lefschetz & --- & \pageref{nv:20}\\
58 & pages 45 à 51, comparaison des Hom hors de $Y$ & --- & \pageref{nv:21}\\
128 & pages 8 et 9, corollaires 2 et 3 & --- & \pageref{nv:22}\\
128 & pages 19 à 29, descente infinitésimale & --- & \pageref{nv:23}\\
126 & pages 17 à 23, factorisation radicielle-étale & --- & \pageref{nv:24}\\
126 & D'après les pages 4 à 7, forme complétée par l'édition, quotient d'une déformation nilpotente & --- & \pageref{nv:25}\\
126 & pages 26 à 29, descente générique & --- & \pageref{nv:26}\\
161-3 & pages 3 à 8, 2-produit de topos & publié & \pageref{nv:27}\\
161-3 & pages 11 et 12, topos d'un produit infini & --- & \pageref{nv:28}\\
23 & pages 86 à 88, finitude de la normalisation & --- & \pageref{nv:29}\\
37 & page 22, quand $\mathrm{Ind}(C)$ est un topos & réfuté & \pageref{nv:30}\\
116 & pages 6 et 7, recollement de topos de préfaisceaux & publié & \pageref{nv:31}\\
100 & pages 2, 3 et 20, pleine fidélité et composantes connexes & --- & \pageref{nv:32}\\
100 & pages 22 à 24, descente des morphismes le long d'un épimorphisme propre & --- & \pageref{nv:33}\\
100 & pages 30 à 38, algébrisation par les courbes & --- & \pageref{nv:34}\\
100 & pages 47 à 52, prolongement vers un modèle de Néron & --- & \pageref{nv:35}\\
14 & pages 93 et 94, amplitude par la caractéristique d'Euler & publié & \pageref{nv:36}\\
59 & D'après les pages 1 à 22, forme corrigée par l'édition, section canonique par le déterminant & --- & \pageref{nv:37}\\
130 & pages 39 à 48, faisceau des quasi-fonctions & --- & \pageref{nv:38}\\
9 & pages 22 à 28, déterminants des parties étales & --- & \pageref{nv:39}\\
9 & pages 24 et 26, déterminant et racine du degré & --- & \pageref{nv:40}\\
14 & pages 23 à 29 et 33, équivalence d'Albanese & --- & \pageref{nv:41}\\
47 & pages 9 et 10, Riemann--Roch et transformation de Fourier sur une base & --- & \pageref{nv:42}\\
51 & pages 16, 17 et 20, bonne réduction de l'Albanese & --- & \pageref{nv:43}\\
57 & pages 98 et 99, section hyperplane générique & --- & \pageref{nv:44}\\
57 & pages 226 à 228 et 247 à 271, Picard analytique et complété & --- & \pageref{nv:45}\\
59 & pages 11 à 13, torseur de Picard en dimension 2 & problème ouvert & \pageref{nv:46}\\
49 & D'après la page 3, forme reconstituée par l'édition, critère de platitude & --- & \pageref{nv:47}\\
57 & pages 42 à 49, rigidité des sous-groupes & --- & \pageref{nv:48}\\
130 & pages 3 à 5, symbole local de Néron & --- & \pageref{nv:49}\\
133 & pages 42 et 43, quotient affine non constructible & --- & \pageref{nv:50}\\
162-5 & Quillen, d'après les pages 43 à 45, universalité des correspondances de bordisme & --- & \pageref{nv:51}\\
162-5 & pages 27 à 30, de Rham et Hochschild pour une catégorie formelle & --- & \pageref{nv:52}\\
162-5 & Quillen, d'après les pages 21 à 26, catégories formelles à conormal plat & --- & \pageref{nv:53}\\
41 & D'après les pages 3 et 8 à 10, composantes irréductibles des fibres, forme reconstituée par l'édition & --- & \pageref{nv:54}\\
102 & page 12, critère d'immersion ouverte & --- & \pageref{nv:55}\\
127 & pages 2 à 4, 15 et 19, critère valuatif de platitude d'une adhérence & --- & \pageref{nv:56}\\
127 & pages 7, 9, 10 et 12, ouverture de Hironaka sur une base réduite & --- & \pageref{nv:57}\\
127 & pages 2 et 3, descente non plate sur une base artinienne & --- & \pageref{nv:58}\\
131 & pages 1 à 5, 13 et 15, représentabilité par un schéma localement quasi-fini & --- & \pageref{nv:59}\\
94 & pages 8, 9 et 19, Tor génériques et suites régulières : l'ouvert dense & --- & \pageref{nv:60}\\
94 & pages 15 et 16, critère de représentabilité sur $\mathrm{Mod}(A)$ & --- & \pageref{nv:61}\\
2 & page 13, une classe non nulle de classe de Chern totale~$1$ & calcul, désaccord & \pageref{nv:62}\\
153 & Pages 3 et 9, co-opérations de $\mathrm{Int}$ relatif, forme corrigée par l'édition & calcul, accord & \pageref{nv:63}\\
5 & page 7, les quotients $W^{(\nu,r)}$ & calcul, accord & \pageref{nv:64}\\
5 & pages 49 et 50, dualité étale pour les sites annelés & publié & \pageref{nv:65}\\
4 & pages 1 et 4 à 7, valeurs propres unités de la cohomologie évanescente & --- & \pageref{nv:66}\\
6 & pages 52 à 56, modules des variétés abéliennes ordinaires & --- & \pageref{nv:67}\\
6 & pages 49 et 50, un groupe formel hors des variétés abéliennes & --- & \pageref{nv:68}\\
6 & pages 47 et 48, même groupe formel, non isogènes & --- & \pageref{nv:69}\\
137 & pages 39 à 44 et 48 à 56, propriété universelle des complexes libres & --- & \pageref{nv:70}\\
137 & pages 74 à 83, catégories polynomiales & --- & \pageref{nv:71}\\
90 & D'après les pages 13 à 23, sous-modules équivariants sur une base quelconque, forme précisée par la lecture & --- & \pageref{nv:72}\\
46 & pages 84 à 89, Hilbert~90 semi-local et inertie & --- & \pageref{nv:73}\\
53 & Page 9, forme corrigée par l'édition, critère d'irréductibilité géométrique & --- & \pageref{nv:74}\\
64 & pages 44 à 52, configurations octaédrales sur une base & --- & \pageref{nv:75}\\
64 & pages 74 à 79 et 84 à 91, épinglages de Legendre & --- & \pageref{nv:76}\\
80 & D'après les pages 24 et 26, cas latticiel, condition b) lue par l'édition & réfuté & \pageref{nv:77}\\
80 & pages 39 à 54, squelette d'un arrangement sans bigones & problème ouvert & \pageref{nv:78}\\
82 & page 78, (61) & calcul, accord & \pageref{nv:79}\\
84 & Pages 45 et 48, \emph{la forme globale} & publié & \pageref{nv:80}\\
84 & Pages 65 à 79, \emph{le produit intrinsèque} & --- & \pageref{nv:81}\\
10 & pages 11 à 16, polarisations hodgiennes & --- & \pageref{nv:82}\\
10 & pages 62 à 65, caractère numérique et tore de rang un & --- & \pageref{nv:83}\\
123 & pages 10 à 12, groupe de Picard de l'espace de Grothendieck--Springer & --- & \pageref{nv:84}\\
123 & pages 21, 28, 30 et 34, rigidifications de Kostant & problème ouvert & \pageref{nv:85}\\
123 & pages 10 à 13, pas de résolution de Steinberg sans changement de base & --- & \pageref{nv:86}\\
15 & pages 71 à 77, catégorie de Picard de Brandt & --- & \pageref{nv:87}\\
15 & pages 116 à 118, foncteurs fibres réels & --- & \pageref{nv:88}\\
27 & pages 27 à 36, semi-continuité des rangs & --- & \pageref{nv:89}\\
45 & pages 10 à 14, liens sur un corps de Tsen & --- & \pageref{nv:90}\\
45 & D'après les pages 3 à 10, forme corrigée par l'édition, surjectivité en $H^1$ en dimension un & --- & \pageref{nv:91}\\
55 & page 13, principe d'identité et lemme~B & --- & \pageref{nv:92}\\
93 & pages 193 et 194, la remarque & --- & \pageref{nv:93}\\
148 & pages 30 à 32 et 35, carte des structures spéciales de $M_{0,5}$ & --- & \pageref{nv:94}\\
62 & D'après les pages 41 à 53, trois descriptions des triplets & calcul, accord & \pageref{nv:95}\\
103 & pages 14 et 15, Gr-champs épinglés et cohomologie relative & --- & \pageref{nv:96}\\
134-1 & pages 3 à 5, suite exacte des champs de Picard épinglés & --- & \pageref{nv:97}\\
134-1 & page 5, réalisation de l'invariant de symétrie & problème ouvert & \pageref{nv:98}\\
85 & D'après les pages 4 à 7, modules des représentations de $G_2$, reformulation de l'édition & calcul, accord & \pageref{nv:99}\\
85 & pages 10 et 40, sous-groupes icosaédraux & calcul, accord & \pageref{nv:100}\\
132 & pages 1 à 3, groupoïde fondamental d'un produit fibré & publié & \pageref{nv:101}\\
132 & pages 16 à 20, extensions d'un groupe non connexe & --- & \pageref{nv:102}\\
132 & D'après les pages 5 à 8, forme complétée par l'édition, Gr-catégorie périphérique d'une surface & --- & \pageref{nv:103}\\
147 & pages 148 à 151, voisinage épointé et codimension deux & problème ouvert & \pageref{nv:104}\\
147 & D'après les pages 62 à 64, forme complétée par l'édition, classe stratifiée de $M_{1,1}$ sur $\mathbf Z$ & calcul, accord & \pageref{nv:105}\\
154 & pages 55 à 63, 85 et 86, monodromie diédrale & calcul, accord & \pageref{nv:106}\\
77 & pages 132 à 143 et 155 à 157, revêtement d'Arf par factorisation de Stein & --- & \pageref{nv:107}\\
29 & page 120, inertie modérée et matrice des multiplicités & --- & \pageref{nv:108}\\
29 & pages 190 à 193, axiome R2 des domaines de ramification & --- & \pageref{nv:109}\\
29 & page 197, proposition~6, homomorphismes de domaines de ramification, énoncée sans démonstration & problème ouvert & \pageref{nv:110}\\
29 & pages 87 à 97, $\pi_1$ modéré et auto-intersection & publié & \pageref{nv:111}\\
29 & pages 170 et 171, torseurs sous un groupe discret infini & --- & \pageref{nv:112}\\
34 & pages 167 et 175 à 180, monodromie modérée à plusieurs paramètres & --- & \pageref{nv:113}\\
149 & pages 36 à 39, le lemme du Complément & publié & \pageref{nv:114}\\
34 & pages 153 à 155, 1-asphéricité locale & --- & \pageref{nv:115}\\
105 & pages 42 à 45, excision pour deux cribles ouverts & --- & \pageref{nv:116}\\
108 & page 2, $\Delta^\circ$ et les catégories test & --- & \pageref{nv:117}\\
118 & D'après les pages 18 à 20, forme complétée par l'édition, sommes amalgamées le long d'opfibrations & --- & \pageref{nv:118}\\
136 & pages 161 à 179 et 189 à 199, schéma en groupes des automorphismes & --- & \pageref{nv:119}\\
136 & pages 5 à 10 et 226 à 232, ombres de la cohomologie entière & --- & \pageref{nv:120}\\
151 & pages 10 à 14 et 17, hyperrecouvrements indexés par une catégorie quelconque & publié & \pageref{nv:121}\\
151 & pages 38 à 42, $\Pi_1$ trop grossier pour la sphère & calcul, accord & \pageref{nv:122}\\
150 & pages 1 et 45 à 47, lissité des fibrations de drapeaux & --- & \pageref{nv:123}\\
150 & pages 47 à 66 et 70, le déploiement comme espace ordonné & --- & \pageref{nv:124}\\
119 & pages 144 et 145, quotients des feuilletages & problème ouvert & \pageref{nv:125}\\
140-1 & pages 22, 24 et 29, Picard du champ {$[U_{0,3}/\mathfrak S_3]$} & calcul, accord & \pageref{nv:126}\\
138 & pages 122 à 124 et 127, opérations sur les cartes & calcul, non testable & \pageref{nv:127}\\
\bottomrule
\end{longtable}}