Unbiasing symmetric monoidal categories in Lean

Título: Unbiasing symmetric monoidal categories in Lean (Desenviesamento de Categorias Monoidais Simétricas em Lean)

Autor: Robin Carlier
Data: 28 de fevereiro de 2026
Contexto: Formalização na biblioteca matemática Mathlib (Lean 4).

---

1. O Problema

Na teoria das categorias e na álgebra formalizada, existe uma distinção fundamental entre abordagens "viesadas" (biased) e "desenviesadas" (unbiased).

• Abordagem Viesada: Uma categoria monoidal simétrica é definida com um produto tensorial binário ($\otimes: C \times C \to C$), um objeto unidade e isomorfismos de coerência (associadores, unitores, tranças) para aridades baixas.
• Abordagem Desenviesada: Muitas aplicações avançadas (como somas sobre conjuntos finitos arbitrários, potências tensoriais $X^{\otimes n}$, ou a teoria de categorias de ordem superior $(\infty, 1)$) exigem a existência de produtos tensoriais para qualquer aridade finita, juntamente com suas coerências, sem depender de uma ordem específica ou de uma associação binária aninhada.

O problema central abordado neste trabalho é a formalização do processo de "desenviesamento" (unbiasing) no assistente de prova Lean 4. Embora a biblioteca Mathlib já possua uma definição clássica de categorias monoidais simétricas, ela não fornece nativamente os produtos tensoriais de alta aridade nem a estrutura necessária para lidar com simetrias de forma independente da ordem, o que é crucial para conectar a teoria de categorias ordinárias com a teoria de categorias de ordem superior (como $\infty$-operados).

2. Metodologia

O autor utiliza uma abordagem baseada na Teorema de Coerência de Mac Lane, formalizada através de uma representação combinatória específica. A metodologia divide-se em três pilares principais:

A. Listas Simétricas e o Teorema de Coerência

O trabalho adapta o trabalho de Piceghello (originalmente em Homotopy Type Theory) para o ambiente não-HoTT do Mathlib.

• Definição: Introduz a categoria de Listas Simétricas ($SList(J)$) sobre um conjunto $J$. Os objetos são listas de elementos de $J$, e os morfismos são gerados por trocas adjacentes (swap) e composição, sujeitos a relações que refletem o grupo simétrico (relações de Coxeter do tipo $A_n$).
• Coerência: Demonstra formalmente que a categoria de listas simétricas é equivalente à categoria monoidal simétrica livre gerada por $J$.
• Correspondência: Estabelece uma bijeção entre morfismos em $SList(J)$ e permutações (isomorfismos de conjuntos de índices), provando que dois morfismos são iguais se e somente se induzem a mesma permutação nos índices (Teorema 2.8).

B. Bicategorias de Spans e Pseudofuntores

Para capturar a estrutura de produtos tensoriais de alta aridade, o autor utiliza a estrutura de Spans (espanhas) na categoria de conjuntos finitos ($Fin$).

• Define uma bicategoria de spans onde os objetos são conjuntos finitos e os morfismos são spans $A \leftarrow B \to C$.
• Foca no pith (núcleo) desta bicategoria, onde apenas os morfismos de spans que são isomorfismos nos vértices são mantidos.
• Desenvolve um sistema de Pith-Beck-Chevalley, que permite construir um pseudofunctor a partir de dados definidos em categorias base e suas opostas, garantindo a compatibilidade com quadrados cartesianos (pullbacks).

C. A Categoria de Kleisli e a Universalidade

• Utiliza a noção de pseudomonad relativa para definir a categoria de Kleisli associada às listas simétricas ($K_{SList}$).
• Demonstra que uma categoria monoidal simétrica pode ser interpretada como um pseudofunctor com valores em $Cat$ definido no oposto da categoria de Kleisli.
• Constrói um pseudofunctor $\Lambda$ que mapeia o pith da bicategoria de spans de conjuntos finitos para a categoria de Kleisli de listas simétricas, efetivamente "codificando" a estrutura de produtos tensoriais de alta aridade.

3. Contribuições Chave

1. Primeira Formalização Mecanizada do Desenviesamento: Este é o primeiro trabalho a provar mecanicamente que uma categoria monoidal simétrica (definida classicamente) induz um pseudofunctor do pith da bicategoria de spans de conjuntos finitos para $Cat$, fornecendo produtos tensoriais de qualquer aridade.
2. Formalização do Teorema de Coerência em Mathlib: Adaptação e extensão do trabalho de Piceghello para o Lean 4, incluindo a prova de que os morfismos de listas simétricas correspondem fielmente a permutações via grupos de Coxeter ($A_\infty$).
3. Infraestrutura de Bicategorias: Implementação robusta de bicategorias de spans, incluindo a definição de composições via pullbacks e a construção de pseudofuntores baseados em sistemas de Beck-Chevalley, preenchendo lacunas na biblioteca Mathlib.
4. Abordagem via "Linearidade": Uso inteligente do conceito de "listas lineares" (sem elementos duplicados) para provar unicidade de isomorfismos e simplificar verificações de coerência, permitindo que táticas de automação (como subsingleton) fechem provas complexas.

4. Resultados Principais

• Teorema 1.1 (Principal): Dada uma categoria monoidal simétrica $(C, \otimes, 1, \alpha, \lambda, \rho, \beta)$, existe um pseudofunctor:
  $$C^\otimes: \text{Pith}(\text{Span}(\text{Fin})) \to \text{Cat}$$
  que envia um conjunto finito $J$ para o produto categórico $C^J$ e um span $A \xleftarrow{f} B \xrightarrow{g} C$ para o functor $g_! f^*$ (onde $f^*$ é a pré-composição e $g_!$ é o produto tensorial sobre as fibras de $g$).
• Teorema 1.3 (Coerência): A categoria livre monoidal simétrica sobre um conjunto $J$ é equivalente à categoria de conjuntos finitos e bijeções sobre $J$ (endowed com a estrutura monoidal cocartesiana), via a categoria de listas simétricas.
• Implementação: O código completo (aprox. 12.5k linhas) está disponível publicamente e compila com o Lean 4 e versões específicas do Mathlib.

5. Significado e Impacto Futuro

• Ponte para Categorias de Ordem Superior: O trabalho fornece a "cola" necessária para interpretar categorias monoidais simétricas ordinárias como objetos dentro da teoria de $(\infty, 1)$-categorias (especificamente, como $\infty$-operados de Lawvere). Isso é essencial para futuros desenvolvimentos do Mathlib em teoria de homotopia e $\infty$-cosmos.
• Operações de Alta Aridade: Permite a definição formal e segura de potências tensoriais $X^{\otimes n}$ e somas sobre conjuntos finitos arbitrários sem depender de escolhas de ordenação ou associação, resolvendo problemas de "DTT Hell" (inferência de tipos complexos devido a igualdades de objetos).
• Fundamentos para Álgebra Avançada: Facilita a formalização de objetos de monoides comutativos internos, representações de grupos e outras estruturas que dependem intrinsecamente da simetria e da aridade variável.
• Metodologia de Formalização: Demonstra como lidar com estruturas pseudoalgébricas (onde igualdades são substituídas por isomorfismos) em assistentes de prova baseados em tipos dependentes, oferecendo um roteiro para formalizar outras estruturas de alta coerência.

Em resumo, este artigo representa um marco na formalização da teoria das categorias, transformando uma construção teórica abstrata (o desenviesamento via teorema de coerência) em uma ferramenta prática e verificada para matemáticos que utilizam o Lean.