Resumen Técnico: Formalización de Complejos Simpliciales Abstractos y Subdivisiones Estelares en Lean

Planteamiento del Problema

La teoría de los complejos simpliciales es fundamental para la topología algebraica y combinatoria, sirviendo como una herramienta primaria para computar invariantes como la homología y el género, y para estudiar tipos de homotopía mediante la teoría de Morse discreta y algoritmos de colapso. Mientras que las definiciones clásicas suelen depender de incrustaciones geométricas en el espacio euclidiano (utilizando coordenadas baricéntricas e independencia afín), tales enfoques introducen datos extraños que complican la computación formal.

Los autores identifican una brecha en el ecosistema del asistente de pruebas Lean: aunque mathlib contiene diversas formalizaciones relacionadas con complejos simpliciales, estas carecen de interconexión, y no existe una formalización existente de las subdivisiones estelares. Además, las formalizaciones existentes en otros asistentes (Rocq, ACL2) están fuertemente orientadas hacia aplicaciones computacionales específicas (por ejemplo, homología persistente, dual de Alexander) en lugar de proporcionar una base combinatoria cohesiva para teoremas estructurales como los de Alexander y Pachner respecto a las triangulaciones de variedades. El artículo aborda la necesidad de un marco puramente combinatorio en Lean 4 que soporte la verificación rigurosa de identidades que involucran subdivisiones estelares, enlaces (links) y uniones (joins), manteniendo al mismo tiempo la compatibilidad con el contenido existente de la biblioteca y la computabilidad.

Metodología

Los autores adoptan un marco puramente combinatorio, definiendo los Complejos Simpliciales Abstractos como colecciones de conjuntos finitos (caras) cerradas bajo la relación de subconjunto, independientes de cualquier espacio geométrico ambiente. Este enfoque elimina las condiciones geométricas (independencia afín, intersecciones de envolventes convexas) presentes en la estructura SimplicialComplex de mathlib, reduciendo así la sobrecarga y simplificando las firmas de los tipos.

Las decisiones metodológicas clave incluyen:

• Conversión de Tipos y Coerción: Para manejar operaciones que cambian el tipo de vértice subyacente (por ejemplo, uniones, subdivisiones), los autores definen SimplicialCoe, una estructura que representa mapas inyectivos sobre conjuntos de vértices. Esto permite un reetiquetado "sin pérdida" sin requerir bijecciones globales sobre los tipos ambientes.
• Uniones Disjuntas para Uniones (Joins): Para definir la unión de dos complejos ($K \star L$) sin asumir conjuntos de vértices disjuntos, los autores utilizan un tipo producto $E \times k$ (donde $k$ es un semianillo no trivial) para indexar las caras, creando efectivamente copias disjuntas de los conjuntos de vértices.
• Subdivisiones Estelares: La subdivisión $\sigma_s K$ de una cara $s$ se define combinatoriamente eliminando el interior de la estrella de $s$ y reemplazándolo con la unión del enlace de $s$, la frontera de $s$ y un nuevo vértice baricentro $x$.
• Verificación Formal: Todas las definiciones y teoremas están implementados en Lean 4. Los autores priorizan la preservación de la computabilidad y la minimización de supuestos para facilitar la futura integración con mathlib.

Contribuciones Clave

El artículo presenta la primera formalización de subdivisiones estelares en cualquier asistente de pruebas. Las contribuciones específicas son:

1. Formalización de Complejos Simpliciales Abstractos:

   • Definición de la estructura central AbstractSimplicialComplex y su conversión de/a instancias de SimplicialComplex geométricas.
   • Formalización de morfismos (SimplicialMap), isomorfismos (SimplicialIso) y coerciones (SimplicialCoe).
   • Implementación de operaciones estándar: uniones, intersecciones, subcomplejos y cálculos de dimensión.

2. Formalización de Subcomplejos y Operaciones:

   • Definiciones rigurosas y pruebas de propiedades para enlaces ($Lk(K, s)$), fronteras de caras ($\partial s$), estrellas ($St(K, s)$), complementos de la estrella, conos y uniones ($K \star L$).
   • Prueba de leyes distributivas, asociatividad y conmutatividad (hasta isomorfismo/coerción) para las uniones.
   • Establecimiento de identidades que muestran cómo estas operaciones interactúan con isomorfismos y coerciones.

3. Formalización de Subdivisiones Estelares:

   • Definición de la subdivisión estelar $\sigma_s K$ y la soldadura estelar (la operación inversa).
   • Definición de equivalencia estelar ($K \cong_{st} L$) como el cierre transitivo de los movimientos estelares.
   • Prueba de que la equivalencia estelar se preserva bajo la conversión de tipo inyectiva (Teorema 3.2), asegurando que la relación de equivalencia es robusta frente a cambios en el etiquetado de los vértices.

4. Nuevos Teoremas e Identidades:

   • Derivación de identidades que describen la interacción entre subdivisiones estelares y enlaces. Notablemente, el Teorema 3.9 establece que para una cara $t$ en el enlace de la cara subdividida, el enlace de $t$ en el complejo subdividido es la subdivisión estelar del enlace original: $Lk(\sigma_s K, t) = \sigma_{s \setminus t}(Lk(K, t))$.
   • Los autores señalan que esta identidad específica, junto con otras varias respecto a la "anticomutatividad" de enlaces y subdivisiones, no tiene una referencia estándar en la literatura y fue derivada durante el proceso de formalización.

Resultados

La formalización verifica con éxito un conjunto de identidades comúnmente utilizadas en el estudio de variedades trianguladas:

• Preservación del Enlace: Si una cara $t$ se encuentra fuera de la estrella subdividida, su enlace permanece inalterado ($Lk(\sigma_s K, t) = Lk(K, t)$).
• Compatibilidad de la Unión: Las subdivisiones estelares se distribuyen sobre las uniones de formas específicas, por ejemplo, $(\sigma_s K) \star L = \sigma_{s \sqcup \emptyset}(K \star L)$.
• Preservación de la Equivalencia: La equivalencia estelar se preserva bajo isomorfismos simpliciales y conversión de tipo inyectiva, siempre que el tipo objetivo tenga suficiente "espacio" para las nuevas etiquetas de los baricentros.
• Volumen de Código: El proyecto comprende actualmente aproximadamente 14,000 líneas de código Lean, cubriendo definiciones, lemas de utilidad y pruebas.

Significado y Reivindicaciones

Los autores posicionan este trabajo como un paso fundacional hacia la formalización de los teoremas de Alexander y Pachner, que establecen que las triangulaciones de variedades son homeomorfas si y solo si están relacionadas por una secuencia de movimientos estelares (o bistelares).

• Primero en su Clase: El artículo afirma ser la primera formalización de subdivisiones estelares en cualquier asistente de pruebas.
• Puente entre Teoría y Computación: Al adoptar un marco combinatorio, el trabajo busca hacer la teoría de los complejos simpliciales más apta para técnicas computacionales y aplicaciones algorítmicas (por ejemplo, en Análisis de Datos Topológicos y software como Regina).
• Catalogación del Folclore: Los autores argumentan que muchas identidades técnicas en topología combinatoria han pasado al estatus de "folclore" debido a la laboriosidad de sus pruebas. Esta formalización sirve para catalogar y verificar estos resultados, asegurando que sus lagunas lógicas sean llenadas.
• Alcance Modesto: Los autores declaran explícamente que esto es un "trabajo inicial". No pretenden haber formalizado aún los teoremas de Pachner, sino que han proporcionado la infraestructura necesaria (subdivisiones, enlaces, uniones y relaciones de equivalencia) para hacerlo. También reconocen que, si bien han aislado los aspectos combinatorios, se requiere trabajo futuro para integrar plenamente estos resultados con las definiciones de SimplicialComplex geométricas de mathlib y para manejar la complejidad de los complejos totales (donbre cada singleton es una cara).

El trabajo enfatiza una filosofía de diseño que prioriza la computabilidad y la compatibilidad con mathlib, con el objetivo de crear una base simplificada para futuros desarrollos en topología combinatoria dentro del ecosistema de Lean.