The Synthetic Sierpinski Cone

1. Enunciato del Problema

Il documento affronta una tensione fondamentale nella matematica sintetica (in particolare all'interno della Teoria dei Tipi di Omotopia, o HoTT) riguardante la relazione tra costruzioni geometriche e classificazione logica delle mappe parziali.

• La Coincidenza Classica: Nella teoria delle categorie classica e nella teoria dei domini, il cono di Sierpi´nski ($X_\perp$), costruito incollando un punto chiuso universale al di sotto di uno spazio $X$, è equivalente al classificatore delle mappe parziali ($L^\circ(X)$). Quest'ultimo classifica le mappe parziali definite su sottospazi aperti. Questa equivalenza è una pietra angolare della dualità tra logica e geometria in questi campi.
• L'Ostacolo Sintetico: In contesti sintetici basati su HoTT con un intervallo generico $I$, affermare che $X_\perp \simeq L^\circ(X)$ per tutti i tipi $X$ porta a una degenerazione della teoria. Nello specifico, se questa equivalenza vale universalmente, forza l'intervallo $I$ a essere "codiscreto" (banale), collassando la distinzione tra sottospazi aperti e chiusi e rendendo banali tutti gli spazi sintetici.
• La Domanda Centrale: È possibile identificare un sottouniverso non banale di tipi in cui il cono di Sierpi´nski classifica effettivamente le mappe parziali, e come ciò si relazioni alle nozioni esistenti di completezza nella teoria delle categorie superiori sintetiche (in particolare la completezza di Segal)?

2. Metodologia

Gli autori lavorano all'interno delle Fondazioni Univalenti (HoTT) senza assumere assiomi forti sull'intervallo $I$ (come ad esempio che sia un ordine lineare stretto) o utilizzando modali globalmente, eccetto dove necessario per argomenti specifici. Essi utilizzano:

• Reticoli Distributivi: Parametrizzano la loro teoria su un reticolo distributivo limitato $\Sigma$ (rappresentante l'"intervallo" $I$) piuttosto che fissare un modello specifico.
• Teoria della Localizzazione: Impiegano la teoria delle localizzazioni riflessive accessibili (seguendo Rijke et al.) per definire sottouniversi di tipi "completi".
• Ortogonalità: Definiscono la completezza tramite ortogonalità rispetto a classi specifiche di mappe (inclusioni di corna, coni, ecc.).
• Cilindri di Mappatura: Generalizzano il cono di Sierpi´nski a cilindri di mappatura aperti (o cilindri di visualizzazione aperti) per gestire famiglie dipendenti di tipi.
• Modali (Limitati): Utilizzano brevemente una modalità di "punti globali" ($\flat$) per analizzare l'esponenziabilità dei punti globali senza collassare la logica interna.

3. Contributi Chiave e Definizioni

A. Gerarchia di Completezza

Il documento stabilisce una gerarchia rigorosa di condizioni di completezza per i tipi, affinando il lavoro di Pugh e Sterling:

1. Completo di Segal: Ortogonale all'inclusione della corno interno $\Lambda^2_1 \hookrightarrow \Delta^2$. Questa è la condizione standard per le $\infty$-categorie sintetiche.
2. Completo di Segal Basato: Ortogonale alla famiglia di inclusioni $\{(i=1)_\perp \hookrightarrow I/i \mid i:I\}$. Questa è una condizione più forte.
3. Completo di Sierpi´nski Piccolo: Ortogonale alle mappe di confronto "piccole" $\sigma_{(i=1)}: (i=1)_\perp \to L^\circ(i=1)$.
4. Completo di Sierpi´nski: Ortogonale all'intera famiglia di mappe di confronto $\sigma_X: X_\perp \to L^\circ(X)$ per ogni $X$.

B. La Principale Equivalenza

Gli autori dimostrano che la Completezza di Sierpi´nski Piccolo è equivalente alla Completezza di Sierpi´nski.

• Significato: Pugh e Sterling avevano precedentemente mostrato questa equivalenza solo per tipi 0-truncati (insiemi). Questo documento la estende a tipi non truncati (gruppi superiori/$\infty$-categorie), dimostrando che verificare l'ortogonalità rispetto alle piccole mappe "piccole" è sufficiente a garantire l'ortogonalità rispetto a tutte le mappe.

C. Separazione della Completezza di Segal e di Segal Basato

Il documento risolve una congettura di Ulrik Buchholtz, dimostrando che la completezza di Segal non implica la completezza di Segal Basato in contesti non banali.

• Essi mostrano che se ogni tipo completo di Segal fosse anche completo di Segal Basato, l'intervallo $I$ diventerebbe iniziale per quoziente (collassando in un insieme a due elementi), il che contraddice le proprietà di modelli standard come gli spazi simpliciali.
• Ciò stabilisce che la condizione "di Segal Basato" è strettamente più forte e necessaria affinché il cono di Sierpi´nski funzioni come classificatore di mappe parziali.

D. Cilindri di Mappatura e Classificatori di Mappe Parziali

Gli autori estendono i risultati del cono di Sierpi´nski ai cilindri di mappatura aperti ($M^\circ_Y(f)$).

• Dimostrano che per i tipi completi di Sierpi´nski, il cilindro di mappatura aperto di una funzione $f: X \to Y$ è equivalente al classificatore relativo di mappe parziali $L^\circ_Y(f)$.
• Ciò fornisce una nuova proprietà universale "destra" per i cilindri di mappatura all'interno del sottouniverso dei tipi completi di Sierpi´nski.

4. Risultati Chiave

1. Teorema 64 e Corollario 66: Un tipo è completo di Sierpi´nski se e solo se è completo di Sierpi´nski piccolo. Di conseguenza, i tipi completi di Sierpi´nski formano un sottouniverso riflessivo accessibile.
2. Corollari 48/49/50: Nei modelli standard (spazi simpliciali, spazi cubici di Dedekind), la completezza di Segal Basato è strettamente più forte della completezza di Segal.
3. Teorema 75 e Corollario 77: Il sottouniverso dei tipi completi di Sierpi´nski è chiuso rispetto alla formazione di classificatori relativi di mappe parziali aperte. All'interno di questo sottouniverso, il cilindro di mappatura aperto $M^\circ_Y(f)$ classifica i punti $y:Y$ equipaggiati con elementi parziali aperti della fibra $\text{fib}_f(y)$.
4. Esponenziabilità: Il documento analizza l'esponenziabilità dei punti globali. Mostra che, mentre le inclusioni di punti globali sono esponenziabili nel senso classico, non sono $L_{Segal}$-esponenziabili internamente a meno che l'intervallo non sia banale. Ciò evidenzia la distinzione tra proprietà interne ed esterne nella matematica sintetica.

5. Significato e Applicazioni

• Semantica Denotazionale: Nella teoria dei domini sintetica, la parzialità è spesso modellata tramite il monade classificatore di mappe parziali $L^\circ$. I risultati chiariscono che per definire funzioni pigre (che dipendono dal fatto che un input sia definito) per casi, il codominio deve essere completo di Sierpi´nski. Ciò implica che qualsiasi dominio sintetico che supporta tali funzioni pigre deve soddisfare la condizione di Segal (transitività dei cammini) e, più fortemente, la condizione di Segal Basato.
• Teoria delle Categorie Superiori Sintetiche: Il lavoro chiarisce la struttura della cocompletazione libera tramite un oggetto iniziale. Nelle $\infty$-categorie sintetiche, il cono di Sierpi´nski $C_\perp$ non è automaticamente un'$\infty$-categoria. Tuttavia, all'interno del sottouniverso riflessivo delle $\infty$-categorie complete di Sierpi´nski, la riflessione $R(C_\perp)$ è equivalente al classificatore di mappe parziali $L^\circ(C)$. Ciò fornisce una descrizione computazionalmente trattabile della cocompletazione libera in questi contesti specifici.
• Unificazione dei Campi: Il documento unisce con successo concetti di topologia sintetica, teoria dei domini e teoria delle categorie superiori. Dimostra che la "coincidenza" tra il cono geometrico di Sierpi´nski e il classificatore logico di mappe parziali non è una legge universale, ma una proprietà di un sottouniverso specifico e ben comportato di tipi.
• Meccanizzazione: Gli autori notano che i loro risultati principali sono stati meccanizzati nell'assistente alla dimostrazione Agda, garantendo la correttezza rigorosa degli argomenti basati sulla teoria dei tipi.

In sintesi, il documento risolve un'ambiguità critica nella matematica sintetica identificando le condizioni precise (completezza di Sierpi´nski) in cui le costruzioni geometriche (coni/cilindri) si allineano con la classificazione logica (mappe parziali), dimostrando simultaneamente che queste condizioni sono strettamente più forti dei requisiti standard per le $\infty$-categorie sintetiche.