\section[Cote 155 : le produit de Takeuchi comme quotient d'un idéalisateur]{Cote 155 : le produit de Takeuchi comme quotient d'un idéalisateur\protect\verifie{Folder155}}\label{sec:155}

La cote 155 porte sur les catégories tannakiennes dont le foncteur fibre n'existe que sur une extension $k'$ du corps de base $k$. La page~1 traduit une telle catégorie en une algèbre $A$ sur laquelle $k'$ agit de deux façons, et demande que la comultiplication de $A$ soit un morphisme d'anneaux (\lot{155}{1}{1}). Elle l'écrit d'abord à valeurs dans $A \mathbin{\hat\otimes}_{k'} A$, puis se corrige : les valeurs sont dans $\tilde{\mathcal J}/\mathcal J$, où $J = \mathrm{Ker}(k' \otimes_k k' \to k')$, $\mathcal J = J \cdot (A \mathbin{\hat\otimes}_k A)$ et $\tilde{\mathcal J} = \{\lambda \mid \lambda\mathcal J \subset \mathcal J\}$.

La correction est nécessaire : quand $k'$ n'est pas central dans $A$, le produit $(a \otimes b)(c \otimes d) = ac \otimes bd$ n'est pas bien défini sur $A \otimes_{k'} A$ : on peut faire passer un scalaire d'un facteur à l'autre avant de multiplier, et le résultat change. Le quotient $(A \otimes_k A)/\mathcal J$ est seulement un groupe abélien. On garde les éléments $\lambda$ qui préservent $\mathcal J$ par multiplication à gauche ; sur eux, le produit passe au quotient. La lecture reconnaît là le produit de Takeuchi $A \times_{k'} A$, formé des $\sum a_i \otimes b_i$ tels que $\sum a_i x \otimes b_i = \sum a_i \otimes b_i x$ pour tout $x \in k'$. La piste note que la littérature lue ne présente pas ce produit comme un quotient d'idéalisateur.

\noindent\emph{Conventions.} On travaille sans complétion. $k$ est un anneau commutatif, $K$ une $k$-algèbre commutative (le $k'$ de la page), $A$ un anneau muni d'un morphisme de $k$-algèbres $\iota : K \to A$ dont l'image n'est pas supposée centrale, et $A$ est un $K$-module par $x \cdot a = \iota(x)a$. Pour un sous-groupe $L$ d'un anneau $S$, on note $\mathbb I(L) = \{\lambda \in S \mid \lambda L \subset L\}$ son idéalisateur.

\begin{enonce}[Énoncé de l'édition, l'idéalisateur]
Si $L$ est un idéal à droite de $S$, $\mathbb I(L)$ est un sous-anneau de $S$ qui contient $L$, $L$ y est un idéal bilatère, et $\mathbb I(L)/L$ est un anneau. C'est le plus grand sous-anneau de $S$ où $L$ est un idéal bilatère.
\end{enonce}

\noindent Voir \texttt{idealiser}, \texttt{ringCon} et \texttt{le\_idealiser\_of}. La seule vérification est $ac - bd = a(c - d) + (a - b)d \in L$ pour $a, b \in \mathbb I(L)$, $a - b$ et $c - d$ dans $L$.

\begin{encadre}
\begin{theoreme}[D'après la page 1, sans complétion\piste{155-takeuchi-idealiser}]
Soit $S = A \otimes_k A$ et $\mathcal J$ l'idéal à droite engendré par les $\iota(x) \otimes 1 - 1 \otimes \iota(x)$, $x \in K$ ; c'est $J \cdot S$, pour $J$ le noyau de la multiplication $K \otimes_k K \to K$. L'application $a \otimes b \mapsto a \otimes b$ de $S$ vers $A \otimes_K A$ est surjective, de noyau $\mathcal J$. Un élément $\lambda$ de $S$ est dans $\tilde{\mathcal J}$ si et seulement si son image $\sum a_i \otimes b_i$ vérifie $\sum a_i\iota(x) \otimes b_i = \sum a_i \otimes b_i\iota(x)$ dans $A \otimes_K A$ pour tout $x \in K$. Ainsi $\tilde{\mathcal J}/\mathcal J$ s'identifie au produit de Takeuchi $A \times_K A$.
\end{theoreme}
\end{encadre}

\begin{proof}
Comme $J$ est engendré par les $x \otimes 1 - 1 \otimes x$ et que l'image de $K \otimes_k K$ dans $S$ est commutative, $J \cdot S$ est l'idéal à droite engendré par les $g_x = \iota(x) \otimes 1 - 1 \otimes \iota(x)$. L'application $a \otimes b \mapsto [a \otimes b]$ de $A \otimes_K A$ vers $S/\mathcal J$ est bien définie, car $\iota(x)a \otimes b - a \otimes \iota(x)b = g_x(a \otimes b)$ ; elle est inverse de la projection, d'où le noyau. Enfin $\lambda \in \tilde{\mathcal J}$ équivaut à $\lambda g_x \in \mathcal J$ pour tout $x$, puisque $\mathcal J$ est engendré à droite par les $g_x$, et l'image de $\lambda g_x$ dans $A \otimes_K A$ est $\sum a_i\iota(x) \otimes b_i - \sum a_i \otimes b_i\iota(x)$.
\end{proof}

\noindent La présentation de la page est donc juste dans ce cadre. La preuve n'utilise pas l'isomorphisme $\mathbb I(L)/L \simeq \mathrm{End}_S(S/L)$ que la piste invoquait. Lean ne vérifie ni le cas des produits tensoriels complétés de pro-objets, que mathlib n'a pas, ni la comultiplication elle-même.
\section[IHÉS 2ILL5 : objets \q{sereins} et objets dualisables]{IHÉS 2ILL5 : objets \q{sereins} et objets dualisables\protect\verifie[\leanblobmain]{Ihes2ILL5}}\label{sec:ihes-2ill5}

Comme les sections~\ref{sec:ihes-sga6-1-5} et~\ref{sec:ihes-sga6-2-3}, cette section porte sur une pièce du fonds Grothendieck--Illusie de l'IHÉS, \texttt{2ILL5} (\href{https://repo-archives.ihes.fr/FONDS_GROTHENDIECK_ILLUSIE/}{vue~2}). C'est un manuscrit au crayon de dix pages, sans date, intitulé \q{Motifs} : le plan d'une théorie des systèmes de coefficients comme cadre des motifs, avec une liste de conjectures. Il n'a pas de pendant dans le fonds de Montpellier, et aucune lecture modernisée n'en a été faite : seul l'énoncé de la définition des pages~2 et~3 est repris ici.

\emph{L'idée.} Dans une catégorie tensorielle, un objet $F$ a un dual faible, le hom interne $F^\vee = \underline{\mathrm{Hom}}(F, \mathbf 1)$, et une flèche canonique $F^\vee \otimes F \to \underline{\mathrm{End}}(F)$. Pour les espaces vectoriels, c'est la flèche $V^* \otimes V \to \mathrm{End}(V)$, $\varphi \otimes v \mapsto (w \mapsto \varphi(w)\,v)$, qui est un isomorphisme exactement quand $V$ est de dimension finie. Les pages~2--3 appellent \q{serein} un objet $F$ tel que $F^\vee \otimes F \simeq \underline{\mathrm{End}}(F)$. C'est la caractérisation usuelle des objets \emph{dualisables} : ceux qui ont un dual $Y$, avec une coévaluation $\eta : \mathbf 1 \to Y \otimes F$ et une évaluation $\varepsilon : F \otimes Y \to \mathbf 1$ qui vérifient les deux identités triangulaires (Dold--Puppe \cite{doldpuppe1980}, Lewis--May--Steinberger \cite{lms1986}, III.1.3).

\begin{encadre}
\begin{enonce}[Manuscrit, pp.~2--3]
Soient $\mathcal C$ une catégorie monoïdale et $F$ un objet qui a un hom interne. Posons $F^\vee = \underline{\mathrm{Hom}}(F, \mathbf 1)$, notons $\mathrm{ev} : F \otimes F^\vee \to \mathbf 1$ l'évaluation, et $\nu_X : F^\vee \otimes X \to \underline{\mathrm{Hom}}(F, X)$ la transposée de $\mathrm{ev} \otimes X$. Alors $F$ a un dual si et seulement si $\nu_F : F^\vee \otimes F \to \underline{\mathrm{End}}(F)$ est un isomorphisme. Dans ce cas tous les $\nu_X$ sont des isomorphismes, et $F^\vee$ est lui-même le dual de $F$, d'évaluation $\mathrm{ev}$.
\end{enonce}
\end{encadre}

\begin{proof}
Si $F$ a un dual $Y$, la flèche $Y \otimes X \to \underline{\mathrm{Hom}}(F, X)$ transposée de $\varepsilon \otimes X$ est inversible : son inverse est la transposée de $\underline{\mathrm{Hom}}(F,X) \to Y \otimes F \otimes \underline{\mathrm{Hom}}(F,X) \to Y \otimes X$, faite de $\eta$ et de l'évaluation, et les identités triangulaires donnent les deux composées. Pour $X = \mathbf 1$, elle identifie $Y$ à $F^\vee$ en envoyant $\varepsilon$ sur $\mathrm{ev}$, et $\nu_X$ s'en déduit. Réciproquement, si $\nu_F$ est inversible, on pose $\eta : \mathbf 1 \to \underline{\mathrm{End}}(F) \xrightarrow{\nu_F^{-1}} F^\vee \otimes F$, l'identité suivie de $\nu_F^{-1}$. La première identité triangulaire, pour $F$, est la définition même de $\nu_F$. La seconde, pour $F^\vee$, est le seul point non formel : on la ramène à la première en comparant les transposées, par la propriété universelle de $F^\vee$.
\end{proof}

\noindent Aucune tresse n'est nécessaire. Dans une catégorie tressée, un dual à gauche est aussi un dual à droite, de sorte que \q{serein}, dualisable à gauche et dualisable à droite y coïncident. L'énoncé lit le \q{$\simeq$} de la page comme \q{la flèche canonique est un isomorphisme} : un isomorphisme abstrait $F^\vee \otimes F \simeq \underline{\mathrm{End}}(F)$ serait en général plus faible, et la page ne dit pas lequel est visé.

\noindent\emph{Vérification en Lean.} La catégorie est monoïdale au sens de mathlib, et $F$ est fermé (\texttt{Closed F}) ; \texttt{MonoidalClosed C} n'est pas supposé. Avec la convention de mathlib, \texttt{tensorLeft F ⊣ ihom F}, le dual interne $F^\vee$ est un dual \emph{à gauche}, et un dual est un \texttt{ExactPairing Y F}. Les objets sont \texttt{dual}, \texttt{ev}, \texttt{canonicalMap} et \texttt{endMap}, pour $F^\vee$, $\mathrm{ev}$, $\nu_X$ et $\nu_F$. L'équivalence encadrée est \texttt{exists\_exactPairing\_iff\_isIso\_endMap}, et \texttt{nonempty\_hasLeftDual\_iff\_isIso\_endMap} sous la forme \texttt{HasLeftDual} ; \texttt{isIso\_endMap\_iff\_forall} dit que tous les $\nu_X$ sont alors inversibles, et \texttt{isIso\_canonicalMap\_of\_exactPairing} donne le sens direct pour un dual quelconque, avec \texttt{whiskerLeft\_comparison\_ev} pour l'identification de $Y$ à $F^\vee$. Le dual construit est \texttt{exactPairingOfIsIso}, à partir de \texttt{triangle\_one} et \texttt{triangle\_two}. Le cas tressé est \texttt{exists\_exactPairing\_right\_iff\_isIso\_endMap}. Un exemple vérifie que tout espace vectoriel de dimension finie sur un corps (\texttt{FGModuleCat K}) est serein. Les noms sont ceux de \href{\leanblobmain/Ihes2ILL5.lean}{\texttt{Ihes2ILL5.\allowbreak{}lean}}.

Ne sont pas démontrés ici : que le \q{$\simeq$} des pages~2--3 désigne la flèche canonique ; les modules libres de type fini sur un anneau commutatif quelconque, l'exemple ne portant que sur les espaces vectoriels ; et le reste du manuscrit.