🔢 mathematics

Unbiasing symmetric monoidal categories in Lean

Cet article présente une formalisation en Lean 4 de l'« unbiasing » des catégories monoïdales symétriques, qui étend leur structure en un pseudofoncteur à valeurs dans les catégories défini sur les spans d'ensembles finis, en s'appuyant sur un théorème de cohérence de Mac Lane et une encodage des formules universelles via une bicatégorie de Kleisli.

Auteurs originaux : Robin Carlier

Publié 2026-03-03

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Robin Carlier

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

🎈 Titre : Démêler les nœuds du monde mathématique avec Lean

Imaginez que vous êtes un architecte qui construit des immeubles (des structures mathématiques). Jusqu'à présent, vous aviez une règle très stricte : pour assembler deux briques, vous deviez utiliser un mortier spécifique. Si vous vouliez assembler trois briques, vous deviez d'abord en assembler deux, puis ajouter la troisième. C'est ce qu'on appelle une approche "biaisée" (ou partiale).

Le problème ? Si vous avez 100 briques, cette méthode devient un cauchemar. Vous devez décider dans quel ordre les assembler, et prouver à chaque fois que le résultat final est le même, peu importe l'ordre. C'est fastidieux et source d'erreurs.

Ce papier, écrit par Robin Carlier, raconte comment il a appris à un ordinateur (le logiciel Lean 4) à construire ces immeubles d'une manière sans biais (ou "unbiased"). Il permet de prendre 100 briques et de les assembler toutes en même temps, sans se soucier de l'ordre, en garantissant mathématiquement que le résultat est unique et correct.

Voici les trois étapes clés de cette aventure, expliquées avec des métaphores.

1. Le problème : La "Cuisine" des mathématiques

Dans le monde des mathématiques classiques (les monoides commutatifs), on sait additionner des nombres. $2 + 3 + 4$ .

Approche biaisée : On fait $(2+3) + 4$ . On a un résultat.
Approche sans biais : On prend le tas $\{2, 3, 4\}$ et on dit "somme". Le résultat est le même, mais la définition est plus propre.

Dans le monde des catégories symétriques monoidales (une version très abstraite et puissante de ces règles de combinaison), c'est pareil. On a des objets qu'on peut "multiplier" (tensoriser).

Le souci : Les mathématiciens définissent habituellement la multiplication de deux objets à la fois. Pour multiplier trois, ils doivent inventer des règles de parenthésage (associateurs) et des règles pour échanger les objets (commutateurs).
La conséquence : Pour faire des calculs complexes (comme sommer sur un groupe entier ou créer des structures libres), il faut passer des heures à vérifier que toutes ces parenthèses et échanges s'annulent correctement. C'est comme essayer de monter un meuble IKEA avec des instructions qui changent à chaque fois que vous touchez une vis.

2. La solution : Le "Super-Liste" (Symmetric Lists)

Pour résoudre ce problème, l'auteur a utilisé une idée brillante : les listes symétriques.

Imaginez que vous avez une liste de courses.

Une liste normale : [Pommes, Bananes, Poires]. L'ordre compte.
Une liste symétrique : C'est comme un sac de fruits où l'ordre n'a pas d'importance, mais où vous pouvez avoir plusieurs fois le même fruit (une "multiset").

L'auteur a prouvé (et codé dans l'ordinateur) que n'importe quelle combinaison complexe d'objets mathématiques peut être réduite à une simple liste de ces objets, où l'ordre est géré par des "permutations" (des échanges de place).

L'analogie du chef d'orchestre :
Imaginez un chef d'orchestre (le théorème de cohérence de Mac Lane). Il dit : "Peu importe comment vous arrangez les musiciens sur la scène, tant que vous jouez la même partition, le son final est identique."
Robin Carlier a codé ce chef d'orchestre dans l'ordinateur. Il a montré que pour chaque permutation de vos objets, il existe une et une seule façon "canonique" de les réarranger. Cela transforme un chaos de règles complexes en une simple liste de permutations.

3. La magie finale : Les "Spans" et le pont vers le futur

Une fois que l'ordinateur comprend comment gérer les listes sans biais, il faut relier cela à la théorie moderne des catégories (les catégories supérieures ou $(\infty, 1)$ -catégories), qui sont le futur des mathématiques formelles.

L'auteur utilise une structure appelée Span (ou "pont").

Imaginez un pont entre deux rives. Une rive est votre catégorie mathématique de départ, l'autre est le monde des catégories de produits.
Le papier montre comment transformer n'importe quelle catégorie symétrique monoidale en un foncteur (un traducteur) qui voyage sur ces ponts.

L'analogie du traducteur universel :
Avant, si vous vouliez parler à un alien (une catégorie supérieure), vous deviez lui expliquer chaque mot un par un avec des règles compliquées.
Grâce à ce travail, l'auteur a créé un traducteur automatique. Il prend n'importe quelle catégorie symétrique monoidale (même celle définie de manière "biaisée" et simple) et la traduit instantanément en un langage que les catégories supérieures comprennent parfaitement, sans perdre aucune information.

Pourquoi est-ce important ?

Pour les mathématiciens : Cela permet de faire des calculs complexes (comme des puissances tensorielles ou des sommes sur des groupes infinis) sans se noyer dans les détails techniques des parenthèses. C'est comme passer d'un calcul à la main à l'utilisation d'une calculatrice scientifique.
Pour l'informatique (Lean) : C'est une étape cruciale pour que le logiciel Mathlib (la bibliothèque de mathématiques de Lean) puisse gérer les mathématiques de très haut niveau. Cela prépare le terrain pour formaliser des théories très avancées qui sont actuellement trop complexes pour les ordinateurs.
Pour le futur : C'est le premier pas vers la formalisation complète de la théorie des catégories supérieures, un domaine qui promet de révolutionner notre compréhension de l'espace, du temps et de la logique.

En résumé

Robin Carlier a pris un problème mathématique très épineux (comment gérer l'ordre et l'assemblage de nombreux objets sans se tromper), a inventé un système de "listes intelligentes" pour simplifier les règles, et a codé tout cela dans un ordinateur pour prouver que tout fonctionne parfaitement.

C'est comme si on avait appris à un robot à cuisiner un gâteau géant non pas en ajoutant les ingrédients un par un avec des règles strictes, mais en lui donnant un bol où il peut tout mettre d'un coup, avec la certitude mathématique que le gâteau sera parfait, quelle que soit la façon dont il a mélangé les cuillères. 🎂🤖

1. Problématique

L'article aborde un défi fondamental dans la formalisation des mathématiques, en particulier dans la bibliothèque Mathlib (pour l'assistant de preuve Lean 4) : la transition d'une définition « biaisée » (biased) à une définition « non biaisée » (unbiased) des catégories monoïdales symétriques.

Le problème du biais : La définition classique d'une catégorie monoïdale symétrique (introduite par Mac Lane) spécifie un produit tensoriel binaire ( $\otimes : \mathcal{C} \times \mathcal{C} \to \mathcal{C}$ ) ainsi que des isomorphismes naturels d'associativité, d'unité et de commutativité (tressage). Bien que suffisante pour la théorie de base, cette approche devient rapidement lourde et peu pratique pour les constructions de haute arité (produits tensoriels de $n$ objets, sommes sur des ensembles finis arbitraires, etc.).
La nécessité du non-biaisage : Pour des applications avancées (comme la définition de monoides commutatifs libres, les puissances tensorielles, ou la théorie des catégories $(\infty, 1)$ ), il est crucial de pouvoir traiter les produits tensoriels d'arités arbitraires de manière intrinsèque, sans dépendre d'une parenthésation ou d'un ordre spécifique des facteurs.
Le contexte Lean : Dans Mathlib, les catégories monoïdales sont actuellement définies de manière biaisée. Cela rend difficile la formalisation de constructions complexes et empêche une connexion fluide avec les perspectives de la théorie des catégories supérieures (où les structures sont naturellement définies via des foncteurs pseudo-fonctoriels sur des catégories de diagrammes).

2. Méthodologie

L'auteur propose une formalisation complète en Lean 4 qui transforme une catégorie monoïdale symétrique classique en un pseudo-foncteur à valeurs dans Cat, défini sur la catégorie (2,1) des spans d'ensembles finis. La méthodologie repose sur trois piliers principaux :

A. Le Théorème de Cohérence via les Listes Symétriques

Pour gérer l'arbitraire des parenthèses et des permutations, l'auteur formalise le théorème de cohérence de Mac Lane en utilisant une présentation combinatoire :

Listes Symétriques (SList) : Inspiré par le travail de Piceghello (en HoTT), l'auteur définit une catégorie de « listes symétriques » sur un ensemble $J$ . Les objets sont des listes d'éléments de $J$ , et les morphismes sont générés par des opérations d'échange (swaps) soumises aux relations du groupe symétrique (relations de Coxeter de type $A_n$ ).
Équivalence avec les groupes de Coxeter : Une contribution majeure est la preuve formelle que les morphismes dans cette catégorie correspondent bijectivement aux permutations (via une pondération dans le groupe de Coxeter infini $A_\infty$ ). Cela permet de prouver que la catégorie des listes symétriques est équivalente à la catégorie libre monoïdale symétrique sur un ensemble.
Implémentation technique : L'auteur adapte la définition des types inductifs hauts (HoTT) vers le cadre non-HoTT de Mathlib, en gérant soigneusement les égalités d'objets et les problèmes de « DTT Hell » (cauchemar de la théorie des types dépendants) en évitant les égalités propositionnelles d'objets là où c'est possible.

B. Les Bicatégories de Spans et le Système Beck-Chevalley

L'objectif est de construire un pseudo-foncteur à partir de la catégorie des spans d'ensembles finis, notée $Pith(Span(Fin))$.

Structure des Spans : L'auteur formalise la bicatégorie des spans (diagrammes $c \leftarrow b \to c'$ ) et définit leur composition via des produits fibrés (pullbacks).
Système Pith-Beck-Chevalley : Pour définir un pseudo-foncteur hors de la « pith » (la sous-bicatégorie où les 2-morphismes sont des isomorphismes) d'une catégorie de spans, l'auteur introduit une structure de données appelée « système Pith-Beck-Chevalley ». Cela consiste en :
1. Deux pseudo-foncteurs (un covariant $U$ et un contravariant $V$ ) définis sur la catégorie de base.
2. Des isomorphismes de changement de base (base change isomorphisms) pour chaque carré cartésien, satisfaisant des conditions de cohérence (pasting horizontal et vertical).
Ce cadre permet de reconstruire le pseudo-foncteur global à partir de ces données locales.

C. Encodage via la Catégorie de Kleisli

L'auteur utilise la théorie des pseudo-monades pour encoder les formules universelles des catégories monoïdales symétriques.

Il définit une bicatégorie de Kleisli ( $K_{SList}$ ) associée à la pseudo-monade des listes symétriques.
Il démontre qu'une catégorie monoïdale symétrique $\mathcal{C}$ peut être vue comme un pseudo-foncteur de la bicatégorie de Kleisli opposée vers Cat.
La construction finale consiste à composer ce foncteur avec un pseudo-foncteur $\Lambda$ reliant les spans d'ensembles finis à la bicatégorie de Kleisli.

3. Résultats Clés

L'article présente plusieurs résultats théoriques et de formalisation :

Théorème 1.1 (Résultat Principal) : Toute catégorie monoïdale symétrique $\mathcal{C}$ définit un pseudo-foncteur $C^\otimes : Pith(Span(Fin)) \to Cat$ .
- Un ensemble fini $J$ est envoyé sur la catégorie produit $\mathcal{C}^J$ .
- Un span $A \xleftarrow{f} B \xrightarrow{g} J$ est envoyé sur le foncteur $g_! f^*$ , où $f^*$ est la précomposition et $g_!$ est le foncteur de somme tensorielle le long des fibres de $g$ .
- Cela réalise une version catégorique ordinaire d'une catégorie monoïdale symétrique de Lawvere (au sens de Cranch).
Théorème 1.3 (Cohérence) : La catégorie libre monoïdale symétrique sur un ensemble $J$ est équivalente à la catégorie des ensembles finis et bijections au-dessus de $J$ (via les listes symétriques).
- Cela formalise le lien entre les morphismes de listes symétriques et les permutations, en utilisant une identification précise via les groupes de Coxeter.
Construction de $\Lambda$ (Proposition 4.12) : Existence et unicité d'un système Pith-Beck-Chevalley sur les ensembles finis qui relie les spans aux listes symétriques.
- La preuve repose sur l'utilisation de la notion de « listes linéaires » (sans doublons) pour garantir l'unicité des isomorphismes nécessaires, évitant ainsi les ambiguïtés de cohérence.

4. Contributions Techniques

Formalisation du Théorème de Cohérence : C'est la première preuve mécanisée complète de la version de Mac Lane reliant les catégories libres aux structures combinatoires (listes symétriques/permutations) dans un cadre non-HoTT.
Infrastructure Mathlib :
- Définition complète des bicatégories de spans et de leurs compositions.
- Formalisation des pseudo-foncteurs et des systèmes de Beck-Chevalley.
- Développement d'une bibliothèque pour les catégories de Kleisli relatives aux pseudo-monades.
Gestion des Égalités : L'auteur propose des techniques robustes pour éviter les problèmes d'égalité d'objets dans les types dépendants (utilisation de eqToHom, gestion de la transparence des définitions), ce qui est crucial pour la maintenabilité des preuves complexes en Lean.
Taille du projet : Le code source fait environ 12 500 lignes (sans les commentaires), compilant avec la dernière version de Lean 4 et Mathlib.

5. Signification et Perspectives

Pour Mathlib : Ce travail fournit les « colles » nécessaires pour connecter la théorie des catégories classiques (déjà bien formalisée dans Mathlib) à la théorie des catégories supérieures. Il permet désormais de manipuler des sommes et produits tensoriels d'arités arbitraires de manière naturelle.
Pour la Théorie des Catégories Supérieures : En montrant que les catégories monoïdales symétriques ordinaires sont équivalentes à des pseudo-foncteurs sur les spans, l'article valide l'approche de Lawvere/Cranch dans un cadre formel. Cela ouvre la voie à la formalisation de la théorie des $(\infty, 1)$ -catégories dans Mathlib.
Applications Futures :
- Définition formelle des puissances tensorielles $x^{\otimes n}$ comme foncteurs équivariants.
- Unbiasing des objets monoides commutatifs internes.
- Équivalence de bi-catégories entre les pseudo-foncteurs préservant les produits et les catégories monoïdales symétriques.

En résumé, cet article représente une avancée majeure dans la formalisation des structures algébriques catégoriques, en résolvant le problème de l'« unbiasing » par une combinaison ingénieuse de théorie des catégories, de théorie des groupes (Coxeter) et d'ingénierie logicielle avancée en Lean.