Technische Samenvatting: Formalisering van Abstracte Simpliciale Complexen & Stellaire Subdivisies in Lean

Probleemstelling

De theorie van simpliciale complexen is fundamenteel voor de algebraïsche en combinatorische topologie, en dient als een primaire tool voor het berekenen van invarianten zoals homologie en genus, en voor het bestuderen van homotopietypes via discrete Morse-theorie en collapse-algoritmen. Dergelijke klassieke definities vertrouwen vaak op geometrische inbeddingen in de Euclidische ruimte (met behulp van barycentrische coördinaten en affiene onafhankelijkheid), maar dergelijke benaderingen introduceren extra gegevens die de formele berekening bemoeilijken.

De auteurs identificeren een gat in het Lean proof assistant-ecosysteem: hoewel mathlib diverse formalisaties bevat die gerelateerd zijn aan simpliciale complexen, ontbreekt de onderlinge verbondenheid, en is er geen bestaande formalisering van stellaire subdivisies. Bovendien zijn bestaande formalisaties in andere assistenten (Rocq, ACL2) sterk georiënteerd op specifieke computationele toepassingen (bijv. persistente homologie, Alexander-dualen) in plaats van het bieden van een samenhangend combinatorisch fundament voor structurele stellingen zoals die van Alexander en Pachner met betrekking tot manifold-triangulaties. Het artikel adresseert de behoefte aan een puur combinatorisch kader in Lean 4 dat de rigoureuze verificatie van identiteiten betreffende stellaire subdivisies, links en joins ondersteunt, terwijl de compatibiliteit met bestaande bibliotheekinhoud en berekenbaarheid behouden blijft.

Methodologie

De auteurs hanteren een puur combinatorisch kader, waarbij ze Abstracte Simpliciale Complexen definiëren als verzamelingen van eindige verzamelingen (faces) die gesloten zijn onder de deelverzameling-relatie, onafhankelijk van enige ambivalente geometrische ruimte. Deze benadering elimineert de geometrische condities (affiene onafhankelijkheid, doorsneden van convexe hullen) die aanwezig zijn in de SimplicialComplex-structuur van mathlib, waardoor de overhead wordt verminderd en de type-signaturen worden vereenvoudigd.

Belangrijke methodologische keuzes omvatten:

• Type-casting en Coercions: Om operaties af te handelen die de onderliggende vertex-type veranderen (bijv. joins, subdivisies), definiëren de auteurs SimplicialCoe, een structuur die injectieve afbeeldingen op vertex-verzamelingen representeert. Dit maakt "verliesloze" herlabeling mogelijk zonder dat er globale bijeenfuncties op de ambivalente types nodig zijn.
• Disjoint Unions voor Joins: Om de join van twee complexen ($K \star L$) te definiëren zonder uit te gaan van disjuncte vertex-verzamelingen, maken de auteurs gebruik van een producttype $E \times k$ (waarbij $k$ een niet-triviale semiring is) om faces te indexeren, wat effectief disjuncte kopieën van de vertex-verzamelingen creëert.
• Stellaire Subdivisies: De subdivisie $\sigma_s K$ van een face $s$ wordt combinatorisch gedefinieerd door het binnenste van de star van $s$ te verwijderen en te vervangen door de join van de link van $s$, de boundary van $s$, en een nieuwe barycentrische vertex $x$.
• Formele Verificatie: Alle definities en stellingen zijn geïmplementeerd in Lean 4. De auteurs geven prioriteit aan het behoud van berekenbaarheid en het minimaliseren van aannames om toekomstige integratie met mathlib te faciliteren.

Belangrijkste Bijdragen

Het artikel presenteert de eerste formalisering van stellaire subdivisies in een enkele proof assistant. De specifieke bijdragen zijn:

1. Formalisering van Abstracte Simpliciale Complexen:

   • Definitie van de kernstructuur AbstractSimplicialComplex en de conversie ervan naar en van geometrische SimplicialComplex-instanties.
   • Formalisering van morfismen (SimplicialMap), isomorfismen (SimplicialIso) en coercions (SimplicialCoe).
   • Implementatie van standaardoperaties: unies, intersecties, subcomplexen en dimensieberekeningen.

2. Formalisering van Subcomplexen en Operaties:

   • Rigoureuze definities en bewijzen van eigenschappen voor links ($Lk(K, s)$), face boundaries ($\partial s$), stars ($St(K, s)$), star complements, cones en joins ($K \star L$).
   • Bewijs van distributieve wetten, associativiteit en commutativiteit (tot isomorfisme/coercion) voor joins.
   • Vaststelling van identiteiten die laten zien hoe deze operaties interageren met isomorfismen en coercions.

3. Formalisering van Stellaire Subdivisies:

   • Definitie van de stellaire subdivisie $\sigma_s K$ en de stellaire weld (de inverse operatie).
   • Definitie van stellaire equivalentie ($K \cong_{st} L$) als de transitieve afsluiting van stellaire moves.
   • Bewijs dat stellaire equivalentie behouden blijft onder injectieve type-casting (Theorem 3.2), wat garandeert dat de equivalentierelatie robuust is tegen veranderingen in vertex-labeling.

4. Nieuwe Stellingen en Identiteiten:

   • Afleiding van identiteiten die de interactie tussen stellaire subdivisies en links beschrijven. Met name Theorem 3.9 stelt vast dat voor een face $t$ in de link van de gesubdivideerde face, de link van $t$ in het gesubdivideerde complex de stellaire subdivisie is van de oorspronkelijke link: $Lk(\sigma_s K, t) = \sigma_{s \setminus t}(Lk(K, t))$.
   • De auteurs merken op dat deze specifieke identiteit, samen met verschillende andere met betrekking tot de "anticommutativiteit" van links en subdivisies, geen standaardreferentie in de literatuur heeft en tijdens het formalisatieproces is afgeleid.

Resultaten

De formalisering verifieert succesvol een reeks identiteiten die veel gebruikt worden bij de studie van getrianguleerde manifolds:

• Link Preservatie: Als een face $t$ buiten de gesubdivideerde star ligt, blijft de link ongewijzigd ($Lk(\sigma_s K, t) = Lk(K, t)$).
• Join Compatibiliteit: Stellaire subdivisies distribueren over joins op specifieke manieren, bijvoorbeeld: $(\sigma_s K) \star L = \sigma_{s \sqcup \emptyset}(K \star L)$.
• Equivalentie Preservatie: Stellaire equivalentie blijft behouden onder simpliciale isomorfismen en injectieve type-casting, mits het doeltype voldoende "ruimte" biedt voor nieuwe barycentrische labels.
• Code Volume: Het project bestaat momenteel uit ongeveer 14.000 regels Lean-code, die definities, utility lemmas en bewijzen beslaan.

Betekenis en Claims

De auteurs positioneren dit werk als een fundamentele stap naar de formalisering van de stellingen van Alexander en Pachner, die stellen dat triangulaties van manifolds homeomorf zijn dan en slechts dan als ze gerelateerd zijn door een sequentie van stellaire (of bistellaire) moves.

• Eerste in zijn soort: Het artikel claimt de eerste formalisering van stellaire subdivisies te zijn in een enkele proof assistant.
• Bruggen Slaan tussen Theorie en Berekening: Door een combinatorisch kader te adopteren, beoogt het werk de theorie van simpliciale complexen toegankelijker te maken voor computationele technieken en algoritmische toepassingen (bijv. in Topological Data Analysis en software zoals Regina).
• Catalogisering van Folklore: De auteurs beargumenteren dat veel technische identiteiten in de combinatorische topologie de status van "folklore" hebben gekregen vanwege de moeizame aard van hun bewijzen. Deze formalisering dient om deze resultaten te catalogiseren en te verifiëren, om ervoor te zorgen dat hun logische hiaten worden opgevuld.
• Bescheiden Omvang: De auteurs verklaren expliciet dat dit "initieel voorwerk" is. Ze claimen niet dat ze de stellingen van Pachner al hebben geformaliseerd, maar hebben de noodzakelijke infrastructuur (subdivisies, links, joins en equivalentierelaties) geleverd om dit te doen. Ze erkennen ook dat hoewel ze de combinatorische aspecten hebben geïsoleerd, toekomstig werk vereist is om deze resultaten volledig te integreren met de geometrische SimplicialComplex definities in mathlib en om de complexiteit van totale complexen (waar elke singleton een face is) te behandelen.

Het werk legt een nadruk op een ontwerpfilosofie die prioriteit geeft aan berekenbaarheid en compatibiliteit met mathlib, met als doel een gestroomlijnd fundament te creëren voor toekomstige ontwikkelingen in de combinatorische topologie binnen het Lean-ecosysteem.