Unbiasing symmetric monoidal categories in Lean

1. Il Problema: La Necessità di "Unbiasing" (Rimozione del Bias)

Nella teoria delle categorie e nell'algebra formale, le strutture come i monoidi commutativi sono spesso definite in modo "biased" (pregiudicato), ovvero basate su operazioni binarie (es. $a + b$) con leggi di associatività e commutatività espresse come proprietà o isomorfismi specifici tra oggetti binari.
Tuttavia, molte applicazioni matematiche (come le somme su insiemi finiti arbitrari o la costruzione di monoidi liberi) richiedono una visione "unbiased" (imparziale): operatori di arità superiore definiti su famiglie finite di oggetti senza un ordine canonico.

Nel contesto delle categorie monoidali simmetriche, la definizione classica (di Mac Lane) fornisce solo:

• Un prodotto tensoriale binario $\otimes: \mathcal{C} \times \mathcal{C} \to \mathcal{C}$.
• Isomorfismi naturali per l'associatività ($\alpha$), l'unità ($\lambda, \rho$) e la simmetria ($\beta$).
• Diagrammi di coerenza (pentagono, esagono, triangolo).

Il problema sorge quando si desidera estendere il prodotto tensoriale ad arità arbitrarie (es. $X_1 \otimes \dots \otimes X_n$) o quando si lavora con categorie di ordine superiore (come le $(\infty, 1)$-categorie). In questi contesti, la definizione classica non scala bene: richiederebbe una proliferazione di dati e identità di coerenza per ogni arità. L'obiettivo è dimostrare che una categoria monoidale simmetrica definita in modo "biased" può essere estesa in modo canonico a una struttura che codifica prodotti di tutte le arità e le loro coerenze, ovvero un pseudofunzionario da una categoria di span di insiemi finiti verso la categoria delle categorie.

2. Metodologia e Strumenti Formali

L'autore implementa questa costruzione nel linguaggio di dimostrazione Lean 4, utilizzando la libreria matematica Mathlib. La metodologia si articola in tre pilastri principali:

A. Teorema di Coerenza e Liste Simmetriche

Il cuore della dimostrazione risiede in una formalizzazione del Teorema di Coerenza di Mac Lane.

• Approccio: Invece di lavorare direttamente con la definizione classica, l'autore utilizza una presentazione della categoria monoidale simmetrica libera su un insieme $J$ tramite liste simmetriche (adattando il lavoro di S. Piceghello da Homotopy Type Theory a Lean/Mathlib).
• Struttura: La categoria delle liste simmetriche $SList(J)$ ha come oggetti liste di elementi di $J$ e come morfismi generati da scambi di elementi adiacenti ($sw_{a,b,l}$), soggetti a relazioni che riflettono le relazioni del gruppo simmetrico (gruppi di Coxeter di tipo $A_n$).
• Risultato Chiave (Teorema 1.3): La categoria libera su $J$ è equivalente alla categoria dei gruppi di insiemi finiti su $J$ ($Core(Fin/J)$). L'autore formalizza la corrispondenza biunivoca tra i morfismi delle liste simmetriche e le permutazioni (o equivalenze di insiemi di indici), dimostrando che due morfismi sono uguali se e solo se inducono la stessa permutazione sugli indici.

B. Bicategorie di Span e Pseudofunzionari

Per passare dalla definizione classica a quella "unbiased", l'autore utilizza la teoria delle bicategorie di span.

• Si considera la bicategoria $Span(Fin)$ degli span di insiemi finiti.
• Si lavora con il suo pith ($Pith(Span(Fin))$), ovvero la sottobicategoria ottenuta rimuovendo i 2-morfismi non invertibili (lasciando solo gli isomorfismi di span).
• L'obiettivo è costruire uno pseudofunzionario da $Pith(Span(Fin))$ verso $Cat$ (la 2-categoria delle categorie).

C. Il Teorema di Beck-Chevalley per il Pith

L'autore introduce una struttura chiamata Pith-Beck-Chevalley system (Definizione 3.2).

• Questo sistema permette di costruire uno pseudofunzionario da $Pith(Span(C))$ a partire da due pseudofunzionari $U: C \to B$ e $V: C^{op} \to B$ che soddisfano condizioni di compatibilità (isomorfismi di base change per i quadrati cartesiani).
• Questo teorema (Teorema 3.3) è fondamentale perché fornisce il "collante" per definire l'azione dello pseudofunzionario sugli span senza dover specificare manualmente ogni coerenza per ogni arità.

D. La Bicategoria di Kleisli

Per gestire le formule universali delle categorie monoidali simmetriche, l'autore utilizza la bicategoria di Kleisli ($K_{SList}$) associata al pseudomonad delle liste simmetriche.

• Gli oggetti sono insiemi.
• I morfismi $J \to K$ sono famiglie di liste simmetriche su $K$ indicizzate da $J$.
• Le categorie monoidali simmetriche sono interpretate come pseudoalgebre per questo pseudomonad, il che permette di codificarle come pseudofunzionari da $(K_{SList})^{op}$ verso $Cat$.

3. Contributi Chiave e Risultati

Il risultato principale del lavoro è la formalizzazione del seguente teorema (Teorema 1.1):

Teorema 1.1: Data una categoria monoidale simmetrica $(\mathcal{C}, \otimes, 1, \alpha, \lambda, \rho, \beta)$, esiste uno pseudofunzionario
$$\mathcal{C}^{\otimes}: Pith(Span(Fin)) \to Cat$$
che invia un insieme finito $J$ alla categoria prodotto $\mathcal{C}^J$ e uno span $A \xleftarrow{f} S \xrightarrow{g} J$ al funtore $g_! f^*$ (dove $f^*$ è la precomposizione e $g_!$ è il prodotto tensoriale lungo le fibre di $g$).

Dettagli tecnici dei contributi:

1. Formalizzazione della Coerenza: È stata realizzata una formalizzazione completa del teorema di coerenza per le categorie monoidali simmetriche in Lean, identificando i morfismi delle liste simmetriche con le permutazioni tramite gruppi di Coxeter (Teorema 2.8). Questo risolve il problema della gestione delle coerenze ad alta arità.
2. Costruzione dello Pseudofunzionario: L'autore costruisce esplicitamente lo pseudofunzionario $\Lambda: Pith(Span(Fin)) \to K_{SList}^{op}$ (Proposizione 4.12) che collega gli span di insiemi finiti alle liste simmetriche. La costruzione si basa sull'uso di liste "lineari" (senza duplicati) per garantire l'unicità degli isomorfismi necessari, sfruttando il fatto che le liste lineari formano un sottospazio dove le coerenze sono banali (Subsingleton).
3. Integrazione in Mathlib: Il lavoro estende significativamente la libreria Mathlib, fornendo:
   • Una definizione di categorie monoidali simmetriche "unbiased".
   • Strumenti per lavorare con prodotti tensoriali di arità arbitraria.
   • Una formalizzazione delle bicategorie di span e dei sistemi di Beck-Chevalley.
4. Codice: Il repository contiene circa 12.5k righe di codice (esclusi commenti) e compila con la toolchain Lean 4 v4.28.0.

4. Significato e Impatto Futuro

Questo lavoro è di fondamentale importanza per diversi motivi:

• Ponte verso le Categorie di Ordine Superiore: Le $(\infty, 1)$-categorie monoidali simmetriche sono spesso definite come pseudofunzionari da categorie di diagrammi (come gli insiemi finiti puntati o gli span). Questo lavoro dimostra che le categorie monoidali simmetriche "classiche" (di ordine 1) sono equivalenti a queste strutture di ordine superiore, fornendo il necessario "ponte" formale per reinterpretare oggetti di Mathlib nel contesto della teoria delle $(\infty, 1)$-categorie.
• Abilitazione di Costruzioni Complesse: La definizione "unbiased" è un prerequisito per formalizzare concetti avanzati come:
  • Le potenze tensoriali simmetriche $x^{\otimes n}$ come oggetti equivarianti sotto l'azione del gruppo simmetrico $\Sigma_n$.
  • Gli oggetti monoidali commutativi interni a categorie monoidali simmetriche.
  • Operazioni di arità superiore per strutture algebriche.
• Robustezza della Formalizzazione: Dimostra che è possibile gestire la complessità delle coerenze ad alta arità in un assistente di prova basato su tipi dipendenti, superando le difficoltà legate all'uguaglianza proposizionale degli oggetti (il cosiddetto "DTT Hell") attraverso un uso attento delle isomorfismi e delle proprietà di unicità (Subsingleton).

In sintesi, Carlier fornisce la prima prova meccanizzata che una categoria monoidale simmetrica classica definisce una struttura "unbiased" coerente, aprendo la strada a una formalizzazione più profonda e scalabile dell'algebra e della teoria delle categorie in Lean.