🔢 mathematics

Unbiasing symmetric monoidal categories in Lean

Este artículo presenta una formalización en Lean 4, dentro de Mathlib, del proceso de desviación de categorías monoidales simétricas mediante la extensión de sus datos a un pseudofunctor Cat-valorado sobre spans de conjuntos finitos, apoyándose en el teorema de coherencia de Mac Lane y una codificación de fórmulas universales.

Autores originales: Robin Carlier

Publicado 2026-03-03

📖 5 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Robin Carlier

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina que tienes una caja de herramientas matemáticas llamada Lean, que es como un asistente muy estricto pero brillante que ayuda a los matemáticos a escribir pruebas que son imposibles de equivocarse. Dentro de esta caja, hay una sección llamada Mathlib, que es como una enorme biblioteca de conceptos matemáticos ya organizados.

El problema que resuelve este artículo es cómo enseñarle a esta biblioteca a manejar "cajas de herramientas" que no solo tienen dos herramientas, sino muchas, y que todas deben encajar perfectamente sin importar el orden en que las saques.

Aquí tienes la explicación paso a paso, usando analogías cotidianas:

1. El Problema: La Regla de "Dos a Dos"

Imagina que tienes una receta para hacer una ensalada. La receta básica te dice cómo mezclar dos ingredientes a la vez (por ejemplo, tomate + lechuga).

En matemáticas tradicionales (y en la versión antigua de Lean): Solo tienes la operación de mezclar dos cosas. Si quieres mezclar cuatro ingredientes (tomate, lechuga, pepino, zanahoria), tienes que hacerlo paso a paso: primero mezclas tomate y lechuga, luego ese resultado con el pepino, y luego con la zanahoria.
El problema: ¿Qué pasa si cambias el orden? ¿Es lo mismo mezclar (tomate+lechuga) con (pepino+zanahoria) que mezclar (tomate+pepino) con (lechuga+zanahoria)? En matemáticas, sí, pero para probarlo tienes que hacer un montón de pasos intermedios.
La necesidad: A veces, los matemáticos necesitan mezclar 100 ingredientes a la vez sin tener que escribir la receta paso a paso. Quieren una "mezcla universal" que funcione para cualquier cantidad de ingredientes, sin importar cómo los agrupes. A esto los autores le llaman "desviolar" (unbiasing): quitar la preferencia por hacerlo de dos en dos.

2. La Solución: El "Mago de los Listas" (Teorema de Coherencia)

Para lograr esto, los autores necesitan una regla mágica que les diga: "No importa cómo agrupes o reordenes estos ingredientes, el resultado final es esencialmente el mismo".

En matemáticas, esto se llama el Teorema de Coherencia de Mac Lane.

La analogía: Imagina que tienes un juego de cartas. Tienes reglas para intercambiar dos cartas (cambiar el orden) y reglas para agruparlas. El teorema dice que, si sigues las reglas, no importa cuántas veces intercambies o agrupes las cartas, siempre llegarás al mismo "estado" final.
El trabajo de los autores: Han traducido este teorema al lenguaje de Lean. Han creado una estructura llamada "Listas Simétricas".
- Piensa en una "Lista Simétrica" como una lista de compras donde el orden no importa (es una bolsa de compras, no una fila).
- Han demostrado formalmente que cualquier operación compleja con muchas cosas se puede reducir a una operación simple sobre estas listas, y que todas las "reglas de intercambio" (como cambiar el orden de los ingredientes) encajan perfectamente.

3. El Gran Truco: Los "Puentes" (Categorías de Espans)

Ahora viene la parte más ingeniosa. ¿Cómo conectamos la idea de "mezclar dos cosas" (que es lo que Lean ya sabe hacer) con "mezclar 100 cosas"?

Los autores usan una herramienta llamada Categoría de Espans (Spans).

La analogía: Imagina que tienes dos islas, la Isla A y la Isla B. Para viajar entre ellas, no hay un puente directo. Pero hay una isla intermedia, la Isla C.
- Puedes ir de A a C y de C a B.
- Un "Span" es como un viaje de ida y vuelta a través de una isla intermedia.
El truco: Los autores muestran que la estructura de "mezclar cosas" se puede ver como un viaje a través de estas islas intermedias.
- Si tienes un conjunto de ingredientes (un grupo de islas), pueden usar estos "puentes" para definir cómo mezclarlos todos a la vez.
- Han creado un "mapa" (un pseudofunctor) que toma cualquier categoría simétrica (tu caja de herramientas) y la convierte en un sistema donde puedes mezclar cualquier número de cosas de una sola vez, usando estos puentes.

4. ¿Por qué es importante? (El "Pegamento" para el Futuro)

Hasta ahora, Lean era como un chef experto que solo sabía cocinar platos de dos ingredientes. Podía hacer cosas muy complejas, pero si le pedías un banquete para 50 personas, tenía que hacerlo paso a paso, lo cual era lento y propenso a errores.

Con este trabajo:

Ahora Lean puede cocinar el banquete completo: Puede definir operaciones con cualquier número de ingredientes de una sola vez.
Preparación para el futuro: Los matemáticos están empezando a estudiar "categorías de nivel superior" (donde las reglas mismas tienen reglas). Para entender esas estructuras avanzadas, es obligatorio poder mezclar cosas de cualquier tamaño sin atascarse en pasos de dos en dos. Este trabajo es el "pegamento" que conecta el matemático de hoy con el matemático del futuro.

En resumen

Robin Carlier y sus colaboradores han construido un traductor universal dentro del software matemático Lean.

Antes: Solo sabías sumar dos números o mezclar dos objetos.
Ahora: Gracias a un teorema antiguo (Coherencia) y a un nuevo sistema de "puentes" (Espans), Lean puede entender y manipular operaciones con cualquier cantidad de objetos, asegurando que todo encaje perfectamente, sin importar el orden.

Es como si hubieran enseñado a un robot a dejar de pensar en "pares" y empezar a pensar en "grupos", lo cual es esencial para resolver los problemas matemáticos más complejos de nuestro tiempo.

A continuación presento un resumen técnico detallado del artículo "Unbiasing symmetric monoidal categories in Lean" (Desviación de categorías monoidales simétricas en Lean) de Robin Carlier, publicado en el contexto de la biblioteca matemática Mathlib de Lean 4.

1. El Problema: La Limitación del Enfoque "Sesgado" (Biased)

En la teoría de categorías estándar, una categoría monoidal simétrica se define de manera "sesgada" (biased): se especifica un producto tensorial binario ( $\otimes: C \times C \to C$ ), un objeto unidad, y isomorfismos naturales (asociador, unitores y trenzado) que satisfacen ciertas ecuaciones (pentágono, hexágono, etc.).

Limitación práctica: Aunque esta definición es suficiente para la teoría básica, resulta insuficiente para aplicaciones que requieren productos tensoriales de aridad superior (ej. $X_1 \otimes \dots \otimes X_n$ ) o sumas sobre conjuntos finitos arbitrarios sin un orden canónico.
El desafío de la formalización: En asistentes de prueba como Lean, definir operaciones de aridad superior directamente a partir de la definición binaria es tedioso y propenso a errores, ya que requiere demostrar constantemente que el resultado es independiente de la forma en que se parenthesizan los términos o el orden de los elementos (coherencia).
Necesidad de "Desviación" (Unbiasing): Se necesita un marco que trate las categorías monoidales simétricas como estructuras que admiten naturalmente operaciones sobre familias finitas de objetos, eliminando la dependencia de la aridad binaria. Esto es crucial para conectar la teoría de categorías ordinaria con la teoría de categorías de orden superior ( $\infty$ -categorías).

2. Metodología y Enfoque Formal

El autor formaliza el proceso de "desviación" (unbiasing) dentro de Mathlib (Lean 4), utilizando un enfoque basado en la teoría de bicategorías y el teorema de coherencia de Mac Lane. La metodología se divide en tres pilares principales:

A. Formalización del Teorema de Coherencia mediante "Listas Simétricas"

Para evitar el manejo directo de diagramas complejos de coherencia, el autor utiliza una presentación combinatoria de las categorías monoidales libres:

Listas Simétricas ($SList$): Se define una categoría donde los objetos son listas de elementos de un conjunto $J$ y los morfismos son generados por permutaciones de elementos adyacentes (swap).
Conexión con Grupos de Coxeter: Se demuestra que los morfismos en esta categoría corresponden biyectivamente a permutaciones (elementos del grupo simétrico $\Sigma_n$ o grupos de Coxeter de tipo $A_n$ ).
Teorema 1.3: Se formaliza que la categoría de listas simétricas sobre un conjunto $J$ es equivalente a la categoría monoidal simétrica libre generada por $J$ . Esto permite normalizar cualquier expresión tensorial compleja a una forma canónica basada en permutaciones.

B. Bicategorías de Espans (Spans) y Pseudo-funtores

El núcleo de la construcción es interpretar una categoría monoidal simétrica como un pseudo-functor desde una bicategoría de "espans" (diagramas de la forma $A \leftarrow B \to C$ ).

Pith de Span(Fin): Se trabaja con el pith (sub-bicategoría donde los 2-morfismos son isomorfismos) de la bicategoría de spans de conjuntos finitos.
Sistema Pith-Beck-Chevalley: Se introduce una estructura técnica (Definición 3.2) que permite construir pseudo-funtores desde el pith de los spans. Esta estructura requiere:
- Dos pseudo-funtores (uno covariante y uno contravariante) que coinciden en objetos.
- Isomorfismos de "cambio de base" (base-change) para cuadrados cartesianos (pullbacks).
Construcción del Functor: Se demuestra que una categoría monoidal simétrica dada induce un sistema Pith-Beck-Chevalley, lo que permite definir un pseudo-functor único hacia la categoría de categorías ($Cat$).

C. La Categoría de Kleisli y Dualidad

Para conectar los conjuntos finitos con las categorías monoidales, se utiliza la bicategoría de Kleisli asociada a la pseudomonada de listas simétricas:

Se define una dualidad ( $D_{J,K}$ ) que actúa como una "transposición" de matrices de listas simétricas.
Se demuestra que, al trabajar con listas "lineales" (sin elementos repetidos), los morfismos son únicos, lo que simplifica drásticamente las pruebas de coherencia mediante el uso de instancias Subsingleton en Lean.

3. Contribuciones Clave

Primera Formalización Mecanizada del Teorema 1.1: El artículo presenta la primera prueba formalizada en un asistente de prueba de que toda categoría monoidal simétrica (definida de forma sesgada) induce un pseudo-functor desde el pith de la bicategoría de spans de conjuntos finitos hacia $Cat$.
- Este funtor envía un conjunto finito $J$ a la categoría de productos $C^J$ .
- Envía un span $A \xleftarrow{f} B \xrightarrow{g} J$ al funtor $g_! f^*$ (donde $f^*$ es precomposición y $g_!$ es un producto tensorial sobre fibras).
Adaptación de Listas Simétricas a Lean/Mathlib:
- Se traduce el trabajo previo de Piceghello (realizado en Homotopy Type Theory) al marco no-HoTT de Mathlib.
- Se formaliza la correspondencia entre morfismos de listas simétricas y permutaciones utilizando grupos de Coxeter, resolviendo problemas técnicos de igualdad de objetos en teoría de tipos dependientes (evitando el "DTT Hell").
Infraestructura de Bicategorías y Pseudo-funtores:
- Se implementan definiciones robustas para bicategorías de spans, pseudo-funtores y sistemas de Beck-Chevalley, diseñadas para minimizar la dependencia de la elección de límites (pullbacks) y facilitar la automatización de pruebas.
Abstracción Universal: Se demuestra cómo las fórmulas universales de las categorías monoidales simétricas pueden codificarse en la bicategoría de Kleisli, permitiendo que las operaciones de aridad superior se definan de manera canónica y libre de ambigüedades.

4. Resultados Principales

Teorema 1.1 (Desviación): Existe un pseudo-functor $C^\otimes: \text{Pith}(\text{Span}(\text{Fin})) \to \text{Cat}$ que codifica la estructura de una categoría monoidal simétrica $C$ de manera "desviada" (unbiased).
Teorema 1.3 (Coherencia): La categoría de listas simétricas sobre un conjunto $J$ es equivalente a la categoría monoidal simétrica libre sobre $J$ .
Corolario 2.9: Los morfismos entre dos listas simétricas están en biyección con las biyecciones entre sus índices que preservan los valores, siempre que las listas sean isomorfas.
Lema 4.11 (Linealidad): Si una de las listas simétricas involucradas es "lineal" (sin duplicados), el morfismo entre ellas es único. Esto permite automatizar pruebas de igualdad de morfismos complejos.

5. Significado e Impacto

Puente hacia Categorías de Orden Superior: Este trabajo es fundamental para la futura integración de la teoría de categorías de orden superior ( $\infty$ -categorías) en Mathlib. La definición de categorías monoidales simétricas como pseudo-funtores desde spans es el modelo estándar en la teoría de $\infty$ -operados (Lurie) y conjuntos dendroidales.
Herramienta para Álgebra Avanzada: Permite definir y manipular objetos como potencias tensoriales simétricas ( $Sym^n(X)$ ) y monoides conmutativos internos de manera natural, sin tener que lidiar manualmente con la asociatividad y la conmutatividad en cada paso.
Calidad del Software Matemático: Demuestra cómo manejar la complejidad de las estructuras pseudo-algebraicas en un asistente de pruebas, ofreciendo un patrón para formalizar otras estructuras algebraicas de orden superior.
Disponibilidad: El código completo (aprox. 12.5k líneas) está disponible en un repositorio público y compila con la versión actual de Lean 4 y Mathlib, listo para ser utilizado por la comunidad.

En resumen, este artículo no solo resuelve un problema técnico de formalización (cómo definir sumas y productos de aridad arbitraria en Lean), sino que establece la infraestructura teórica necesaria para que la biblioteca Mathlib pueda soportar desarrollos avanzados en topología algebraica y teoría de homotopía que requieren un manejo riguroso de la simetría y la coherencia de orden superior.