The Synthetic Sierpinski Cone

1. Énoncé du problème

Le papier aborde une tension fondamentale en mathématiques synthétiques (spécifiquement dans la Théorie des Types Homotopiques, ou HoTT) concernant la relation entre les constructions géométriques et la classification logique des applications partielles.

• La coïncidence classique : En théorie des catégories classique et en théorie des domaines, le cône de Sierpi´nski ($X_\perp$), construit en collant un point fermé universel sous un espace $X$, est équivalent au classificateur d'applications partielles ($L^\circ(X)$). Ce dernier classe les applications partielles définies sur des sous-espaces ouverts. Cette équivalence est une pierre angulaire de la dualité entre logique et géométrie dans ces domaines.
• L'obstacle synthétique : Dans les cadres synthétiques basés sur la HoTT avec un intervalle générique $I$, affirmer que $X_\perp \simeq L^\circ(X)$ pour tous les types $X$ conduit à une dégénérescence de la théorie. Plus précisément, si cette équivalence vaut universellement, elle force l'intervalle $I$ à être « codiscrète » (triviale), effondrant la distinction entre sous-espaces ouverts et fermés et rendant tous les espaces synthétiques triviaux.
• La question centrale : Peut-on identifier un sous-univers non trivial de types où le cône de Sierpi´nski classe effectivement les applications partielles, et comment cela se rapporte-t-il aux notions existantes de complétude en théorie des catégories supérieures synthétiques (spécifiquement la complétude de Segal) ?

2. Méthodologie

Les auteurs travaillent dans les Fondements Univalents (HoTT) sans supposer d'axiomes forts sur l'intervalle $I$ (tels qu'il soit un ordre linéaire strict) ni utiliser de modalités globalement, sauf lorsque nécessaire pour des arguments spécifiques. Ils utilisent :

• Treillis distributifs : Ils paramètrent leur théorie sur un treillis distributif borné $\Sigma$ (représentant l'« intervalle » $I$) plutôt que de fixer un modèle spécifique.
• Théorie de la localisation : Ils emploient la théorie des localisations réfléchies accessibles (suivant Rijke et al.) pour définir des sous-univers de types « complets ».
• Orthogonalité : Ils définissent la complétude par orthogonalité à des classes spécifiques d'applications (inclusions de cornes, cônes, etc.).
• Cylindres d'application : Ils généralisent le cône de Sierpi´nski aux cylindres d'application ouverts (ou cylindres d'affichage ouverts) pour gérer les familles dépendantes de types.
• Modalités (limitées) : Ils utilisent brièvement une modalité de « points globaux » ($\flat$) pour analyser l'exponentiabilité des points globaux sans effondrer la logique interne.

3. Contributions et définitions clés

A. Hiérarchie de complétude

Le papier établit une hiérarchie stricte de conditions de complétude pour les types, affinant le travail de Pugh et Sterling :

1. Complète de Segal : Orthogonale à l'inclusion de la corne intérieure $\Lambda^2_1 \hookrightarrow \Delta^2$. C'est la condition standard pour les $\infty$-catégories synthétiques.
2. Complète de Segal basée : Orthogonale à la famille d'inclusions $\{(i=1)_\perp \hookrightarrow I/i \mid i:I\}$. C'est une condition plus forte.
3. Complète de Sierpi´nski petit : Orthogonale aux applications de comparaison « petites » $\sigma_{(i=1)}: (i=1)_\perp \to L^\circ(i=1)$.
4. Complète de Sierpi´nski : Orthogonale à la famille complète d'applications de comparaison $\sigma_X: X_\perp \to L^\circ(X)$ pour tout $X$.

B. L'équivalence principale

Les auteurs prouvent que la complétude de Sierpi´nski petit est équivalente à la complétude de Sierpi´nski.

• Signification : Pugh et Sterling avaient précédemment montré cette équivalence uniquement pour les types 0-tronqués (ensembles). Ce papier l'étend aux types non tronqués (groupoïdes supérieurs/$\infty$-catégories), prouvant que vérifier l'orthogonalité contre les petites applications « petites » suffit à garantir l'orthogonalité contre toutes les applications.

C. Séparation de la complétude de Segal et de la complétude de Segal basée

Le papier résout une conjecture d'Ulrik Buchholtz, prouvant que la complétude de Segal n'implique pas la complétude de Segal basée dans des contextes non triviaux.

• Ils montrent que si chaque type complet de Segal était aussi complet de Segal basé, l'intervalle $I$ deviendrait quotient-initial (s'effondrant en un ensemble à deux éléments), ce qui contredit les propriétés de modèles standards comme les espaces simpliciaux.
• Cela établit que la condition « Segal basée » est strictement plus forte et nécessaire pour que le cône de Sierpi´nski fonctionne comme un classificateur d'applications partielles.

D. Cylindres d'application et classificateurs d'applications partielles

Les auteurs étendent les résultats sur le cône de Sierpi´nski aux cylindres d'application ouverts ($M^\circ_Y(f)$).

• Ils démontrent que pour les types complets de Sierpi´nski, le cylindre d'application ouvert d'une fonction $f: X \to Y$ est équivalent au classificateur d'applications partielles relatif $L^\circ_Y(f)$.
• Cela fournit une nouvelle propriété universelle « droite » pour les cylindres d'application au sein du sous-univers des types complets de Sierpi´nski.

4. Résultats clés

1. Théorème 64 & Corollaire 66 : Un type est complet de Sierpi´nski si et seulement s'il est complet de Sierpi´nski petit. Par conséquent, les types complets de Sierpi´nski forment un sous-univers réfléchi accessible.
2. Corollaire 48/49/50 : Dans les modèles standards (espaces simpliciaux, espaces cubiques de Dedekind), la complétude de Segal basée est strictement plus forte que la complétude de Segal.
3. Théorème 75 & Corollaire 77 : Le sous-univers des types complets de Sierpi´nski est clos sous la formation de classificateurs d'applications partielles ouvertes relatives. Au sein de ce sous-univers, le cylindre d'application ouvert $M^\circ_Y(f)$ classe les points $y:Y$ équipés d'éléments partiels ouverts de la fibre $\text{fib}_f(y)$.
4. Exponentiabilité : Le papier analyse l'exponentiabilité des points globaux. Il montre que, bien que les inclusions de points globaux soient exponentiables au sens classique, elles ne sont pas $L_{Segal}$-exponentiables intérieurement sauf si l'intervalle est trivial. Cela met en évidence la distinction entre propriétés internes et externes en mathématiques synthétiques.

5. Importance et applications

• Sémantique dénotationnelle : En théorie des domaines synthétique, la partialité est souvent modélisée via le monade classificateur d'applications partielles $L^\circ$. Les résultats clarifient que pour définir des fonctions paresseuses (qui dépendent du fait qu'une entrée soit définie) par cas, le codomaine doit être complet de Sierpi´nski. Cela implique que tout domaine synthétique supportant de telles fonctions paresseuses doit satisfaire la condition de Segal (transitivité des chemins) et, plus fortement, la condition de Segal basée.
• Théorie des catégories supérieures synthétiques : Le travail clarifie la structure de la cocomplétion libre par un objet initial. Dans les $\infty$-catégories synthétiques, le cône de Sierpi´nski $C_\perp$ n'est pas automatiquement une $\infty$-catégorie. Cependant, au sein du sous-univers réfléchi des $\infty$-catégories complètes de Sierpi´nski, la réflexion $R(C_\perp)$ est équivalente au classificateur d'applications partielles $L^\circ(C)$. Cela fournit une description calculable de la cocomplétion libre dans ces contextes spécifiques.
• Unification des domaines : Le papier unifie avec succès des concepts issus de la topologie synthétique, de la théorie des domaines et de la théorie des catégories supérieures. Il démontre que la « coïncidence » entre le cône géométrique de Sierpi´nski et le classificateur logique d'applications partielles n'est pas une loi universelle, mais une propriété d'un sous-univers spécifique et bien comporté de types.
• Mécanisation : Les auteurs notent que leurs résultats principaux ont été mécanisés dans l'assistant de preuve Agda, assurant la correction rigoureuse des arguments de théorie des types.

En résumé, le papier résout une ambiguïté critique en mathématiques synthétiques en identifiant les conditions précises (complétude de Sierpi´nski) sous lesquelles les constructions géométriques (cônes/cylindres) s'alignent avec la classification logique (applications partielles), tout en prouvant simultanément que ces conditions sont strictement plus fortes que les exigences standard pour les $\infty$-catégories synthétiques.