🔢 mathematics

Unbiasing symmetric monoidal categories in Lean

Dit artikel presenteert een formalisatie in Lean 4 van het onbevooroordeeld maken van symmetrisch monoidale categorieën door de data uit te breiden tot een Cat-waarde pseudofunctor over spannen van eindige verzamelingen, waarbij gebruik wordt gemaakt van Mac Lane's coherentiestelling en een Kleisli-bicategorie voor universele formules.

Oorspronkelijke auteurs: Robin Carlier

Gepubliceerd 2026-03-03

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Robin Carlier

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat je een enorme, complexe machine bouwt: een wiskundig universum waarin je dingen kunt optellen, vermenigvuldigen en combineren. In de wiskunde noemen we dit een symmetrisch monoidale categorie. Klinkt eng? Laten we het vergelijken met een keuken.

De Keuken van de Wiskunde

Stel je een keuken voor waar je gerechten maakt.

De ingrediënten zijn de objecten (bijv. eieren, bloem, suiker).
Het koken is het "tensorproduct": het samenvoegen van ingrediënten tot een gerecht.
De recepten zijn de regels die zeggen hoe je dingen mag combineren.

In de oude manier van werken (de "vooringenomen" manier, zoals de auteurs het noemen), had je een recept dat alleen zei: "Meng eerst eieren en bloem, en voeg daarna suiker toe."
Dit werkt prima als je twee dingen hebt. Maar wat als je 100 ingrediënten hebt? Moet je dan 99 keer in je recept schrijven: "Meng eerst A en B, dan dat resultaat met C, dan met D..."?
Dat is onhandig. Het maakt het recept enorm lang, vol met haakjes en specifieke volgorde-regels. Als je de volgorde van twee ingrediënten verwisselt (eerst suiker, dan bloem), moet je een extra stap toevoegen om te zeggen: "Oh, dat mag ook, want het is symmetrisch."

Dit is het probleem waar de wiskundige Robin Carlier en zijn team in Lean (een computerprogramma dat wiskundige bewijzen controleert) mee worstelden. Hun "keukenbibliotheek" (Mathlib) kon goed werken met twee ingrediënten, maar werd een rommeltje als je met veel ingrediënten tegelijk wilde werken.

De Oplossing: De "Onvooringenomen" Keuken

De auteurs hebben een nieuwe manier bedacht om deze keuken te beschrijven. In plaats van te zeggen "meng A en B, en voeg C toe", zeggen ze nu: "Neem een mandje met alle ingrediënten die je nodig hebt, en kook ze samen."

Ze noemen dit unbiasing (het wegnemen van de voorkeur voor een specifieke volgorde).

Hoe hebben ze dit gedaan? Ze hebben een slimme truc gebruikt die lijkt op het kopen van een kant-en-klaar maaltijd in plaats van het zelf koken.

De Magische Lijst (Symmetrische Lijsten):
Ze hebben een nieuw soort lijst bedacht: een "symmetrische lijst". In een gewone lijst is de volgorde belangrijk: [A, B] is anders dan [B, A]. In een symmetrische lijst maakt de volgorde niet uit; het is gewoon een verzameling. Als je [A, B] hebt, is dat hetzelfde als [B, A].
Dit is alsof je in plaats van een recept met haakjes, een boodschappenlijstje hebt. Het maakt niet uit in welke volgorde je de items opschrijft; het resultaat (het gerecht) blijft hetzelfde.
De Magische Vertaler (De Coherentie-stelling):
De grootste uitdaging was: "Hoe weten we zeker dat het gerecht dat we maken met de boodschappenlijst precies hetzelfde smaakt als het gerecht dat we maken met het oude, ingewikkelde recept?"
De auteurs hebben bewezen dat er altijd precies één "magische vertaler" is die het oude recept omzet in de nieuwe boodschappenlijst, zonder dat de smaak verandert. Ze noemen dit de Coherentie-stelling.
- Analogie: Het is alsof je bewijst dat het niet uitmaakt of je eerst je sokken aantrekt en dan je schoenen, of andersom (als je sokken en schoenen los van elkaar zijn). Er is altijd een manier om het te doen zonder dat je struikelt.
De Bruggenbouwer (Spans en Pseudofunctors):
Om dit allemaal in de computer te laten werken, hebben ze een brug gebouwd tussen twee werelden:
- Wereld A: De wereld van de simpele boodschappenlijstjes (eindige verzamelingen).
- Wereld B: De wereld van de complexe kookkunst (symmetrische monoidale categorieën).
Ze hebben een systeem ontworpen (een "pseudofunctor") dat automatisch vertaalt: "Als je een boodschappenlijstje geeft, weet de computer precies welk gerecht je moet maken, ongeacht hoe groot de lijst is."

Waarom is dit belangrijk?

Voor een wiskundige (of een computer die wiskunde doet) is dit een revolutie.

Vroeger: Als je een formule wilde schrijven met 50 termen, moest je de computer duizenden regels geven om te zeggen hoe je die 50 termen moest groeperen.
Nu: Je kunt zeggen: "Hier is een groep van 50 dingen, tel ze op." De computer weet precies wat je bedoelt, zonder dat je hoeft te specificeren welke twee je eerst optelt.

Dit is essentieel voor de toekomst van wiskundige software. Het maakt het mogelijk om complexe structuren te bouwen die lijken op de manier waarop natuurkundigen en cryptografen denken: zonder zich zorgen te maken over de volgorde van haakjes, maar gewoon te focussen op de verzameling als geheel.

Samenvatting in één zin

De auteurs hebben een slimme vertaler gebouwd voor computers die het mogelijk maakt om wiskundige "recepten" met honderden ingrediënten te schrijven alsof het één simpele boodschappenlijst is, zonder dat de computer in de war raakt over de volgorde.

Dit werk is niet alleen een technische prestatie voor computers, maar ook een stap in de richting van een universele taal voor wiskunde die net zo flexibel is als onze eigen gedachten.

Titel: Unbiasing symmetric monoidal categories in Lean

Auteur: Robin Carlier
Context: Formele wiskunde in Lean 4 (Mathlib), categorietheorie, hogere categorietheorie.

1. Het Probleem

In de klassieke definitie van een symmetrische monoidale categorie wordt de tensorproduct-operatie ( $\otimes$ ) gedefinieerd als een binaire functor ( $C \times C \to C$ ), vergezeld van natuurlijke isomorfismen voor associativiteit ( $\alpha$ ), eenheid ( $\lambda, \rho$ ) en commutativiteit ( $\beta$ ). Hoewel deze "vooroordeelde" (biased) definitie eenvoudig is om te definiëren, is deze onvoldoende voor complexe wiskundige toepassingen die operatoren met hogere ariteit vereisen (bijv. het nemen van een tensorproduct van $n$ objecten, of het construeren van vrije commutatieve monoiden).

De uitdaging in software voor wiskundig bewijzen (zoals Lean) is het "unbiasen" van deze structuur: het uitbreiden van de binaire operatie naar een coherente familie van operatoren voor elke eindige verzameling van objecten, zonder dat de uitkomst afhangt van de volgorde van paren of de manier van groeperen (haakjes). Dit vereist een bewijs dat alle mogelijke manieren om een tensorproduct te construeren via associatoren en braidingen equivalent zijn (Mac Lane's coherentiestelling).

Bestaande formalisaties in Mathlib gebruiken de vooroordeelde definitie, wat complexe constructies bemoeilijkt en de brug naar hogere categorietheorie (zoals $(\infty, 1)$ -categorieën) blokkeert, waar objecten per definitie "onvooroordeeld" worden beschouwd als pseudofunctoren.

2. Methodologie

De auteur formaliseert het unbiasing-proces binnen Lean 4 en de Mathlib-bibliotheek door een brug te slaan tussen klassieke categorietheorie en de theorie van pseudofunctoren. De aanpak bestaat uit drie hoofdstappen:

Formalisatie van de Coherentiestelling via Symmetrische Lijsten:
- De auteur bouwt voort op het werk van Piceghello (uitgevoerd in Homotopy Type Theory) en past dit aan voor de niet-HoTT-omgeving van Mathlib.
- Er wordt een categorie gedefinieerd genaamd Symmetrische Lijsten ($SList(J)$), gepresenteerd via generators en relaties. De objecten zijn lijsten van elementen uit een verzameling $J$ , en de morfismen worden gegenereerd door het verwisselen van elementen (swap).
- Een cruciaal technisch aspect is het bewijzen dat morfismen in deze categorie corresponderen met permutaties. Dit wordt gedaan door morfismen te labelen met elementen van Coxeter-groepen (specifiek type $A_\infty$ ).
- Er wordt bewezen dat de categorie van symmetrische lijsten equivalent is aan de vrije symmetrische monoidale categorie op een verzameling.
Bicategorieën van Spans en Pseudofunctoren:
- De auteur introduceert de bicategorie van spans (diagrammen van de vorm $A \leftarrow B \to C$ ) over de categorie van eindige verzamelingen.
- Om een pseudofuncteur te construeren vanuit de "pith" (de sub-bicategorie met alleen invertibele 2-morfismen) van deze spans, wordt een structuur gedefinieerd genaamd een Pith-Beck-Chevalley-systeem. Dit systeem bestaat uit twee pseudofunctoren (een covariante en een contravariante) en een familie van isomorfismen die de "base change" eigenschap voor pullback-vierkanten garanderen.
Kleisli Bicategorie en Unbiasing:
- Symmetrische monoidale categorieën worden geïnterpreteerd als pseudofunctoren vanuit de tegengestelde Kleisli-bicategorie van symmetrische lijsten ( $K_{SList}^{op}$ ) naar de categorie van categorieën ($Cat$).
- De kern van het bewijs is het construeren van een specifieke pseudofuncteur $\Lambda$ van de pith van de spans-bicategorie naar de Kleisli-bicategorie.
- Door de coherentiestelling te gebruiken, wordt aangetoond dat operaties op symmetrische lijsten zich gedragen als matrixvermenigvuldiging met multisetten (verzamelingen met multipliciteiten). Dit maakt het mogelijk om te bewijzen dat de benodigde isomorfismen uniek zijn, zolang de betrokken lijsten "lineair" zijn (geen dubbele elementen).

3. Belangrijkste Bijdragen

Formalisatie van Mac Lane's Coherentiestelling: De eerste mechanisatie van de stelling dat de vrije symmetrische monoidale categorie op een verzameling $J$ equivalent is aan de categorie van symmetrische lijsten over $J$ . Dit omvat een volledig bewijs dat morfismen in deze categorie corresponderen met permutaties, gelabeld via Coxeter-groepen.
Constructie van de Unbiasing Pseudofuncteur: Het bewijs van Stelling 1.1: Elke symmetrische monoidale categorie $C$ $C$ definieert een pseudofuncteur $C^\otimes: \text{Pith}(\text{Span}(\text{Fin})) \to \text{Cat}$ $C^{\otimes} : Pith (Span (Fin)) \to Cat$ .
- Deze functeur stuurt een eindige verzameling $J$ naar het product $C^J$ .
- Een span $A \leftarrow B \to C$ wordt vertaald naar een functor die tensorproducten neemt over de vezels van de afbeeldingen.
Technische Innovaties in Lean:
- Het omzeilen van "DTT Hell" (problemen met gelijkheid van objecten in afhankelijke type-theorie) door het gebruik van definities die gelijkheid vermijden en in plaats daarvan werken met isomorfismen en "Subsingleton"-instanties voor unieke morfismen tussen lineaire lijsten.
- Het introduceren van een Kleisli bicategorie voor symmetrische lijsten om universele formules te coderen, wat de scheiding tussen universele theorie en specifieke instantiatie in een categorie $C$ mogelijk maakt.
Connectie met Hogere Categorietheorie: Het werk toont aan dat een gewone symmetrische monoidale categorie kan worden geïnterpreteerd als een Lawvere symmetrisch monoidale $(\infty, 1)$ -categorie (via Cranch's model), wat een essentiële stap is voor de toekomstige integratie van hogere categorietheorie in Mathlib.

4. Resultaten

Stelling 1.1 (Hoofdstelling): Er bestaat een unieke pseudofuncteur die een symmetrische monoidale categorie omzet in een "onvooroordeelde" structuur die tensorproducten van willekeurige eindige families van objecten ondersteunt.
Stelling 1.3 (Coherentiestelling): De categorie van symmetrische lijsten op een verzameling $J$ is equivalent aan de vrije symmetrische monoidale categorie op $J$ .
Corollarium 2.9: Er is een bijectie tussen morfismen tussen twee symmetrische lijsten en de bijecties tussen hun indexverzamelingen die de elementen behouden.
Implementatie: De volledige formalisatie (ongeveer 12.5k regels code, exclusief commentaar) is beschikbaar in een openbare repository en compileert met Lean 4 en de Mathlib-bibliotheek.

5. Betekenis en Toekomstperspectief

Fundamenteel voor Mathlib: Dit werk legt de basis voor het werken met complexe algebraïsche structuren in Lean, zoals vrije commutatieve monoiden en tensorpotten van objecten, zonder dat gebruikers handmatig haakjes en volgorde hoeven te beheren.
Brug naar Hogere Categorietheorie: Het biedt de noodzakelijke "lijm" om objecten uit de gewone categorietheorie (die al in Mathlib bestaan) te herinterpreteren als objecten in hogere categorietheorie, wat essentieel is voor de ontwikkeling van theorieën zoals $\infty$ -operads en tetracategories binnen de bibliotheek.
Toekomstige Toepassingen: De auteur verwacht dat dit werk zal leiden tot de formalisatie van:
- Tensorpotten van objecten ( $x^{\otimes n}$ ) als functoren naar equivariante objecten.
- Onvooroordeelde commutatieve monoiden binnen symmetrische monoidale categorieën.
- Een volledige biequivalentie tussen de bicategorie van pseudofunctoren en de bicategorie van symmetrische monoidale categorieën.

Samenvattend biedt dit artikel een robuuste, mechanisatie van een diep theoretisch resultaat uit de categorietheorie, wat de weg vrijmaakt voor geavanceerde algebraïsche en topologische toepassingen binnen het Lean-ecosysteem.