Coslice Colimits in Homotopy Type Theory

1. Problema e Contesto

Il lavoro si inserisce nel campo della Teoria dei Tipi Omotopica (HoTT) e studia i colimiti omotopici (in particolare i colimiti su grafi) all'interno di coslice di un universo ($A/\mathcal{U}$).

• Il Contesto: In HoTT, i tipi puntati e le categorie di gruppi superiori sono spesso modellati come coslice di un universo (ad esempio, $1/\mathcal{U}$ corrisponde alla categoria dei tipi puntati).
• La Sfida: Sebbene l'esistenza dei colimiti in un universo $\mathcal{U}$ sia garantita dai Tipi Induttivi Superiori (HITs), la costruzione esplicita e le proprietà dei colimiti nelle coslice ($A/\mathcal{U}$) sono più complesse. Non è immediato come i colimiti in $A/\mathcal{U}$ si relazionino ai colimiti ordinari in $\mathcal{U}$, specialmente per quanto riguarda la preservazione di proprietà omotopiche (come la $n$-connessione) e l'interazione con sistemi di fattorizzazione ortogonale.
• Obiettivo: Caratterizzare la connessione tra i colimiti in un universo e i colimiti nelle sue coslice, fornendo una costruzione esplicita che riveli tale relazione senza fare affidamento su HITs generici non costruttivi.

2. Metodologia

Gli autori adottano un approccio costruttivo basato sulla Teoria dei Tipi di Martin-Löf (MLTT) potenziata solo con i pushout (e non con HITs generali), per dimostrare come costruire i colimiti nelle coslice.

• Costruzione Principale (Main Connection): Invece di postulare l'esistenza dei colimiti in $A/\mathcal{U}$, gli autori costruiscono esplicitamente il colimite di un diagramma $F$ in $A/\mathcal{U}$ partendo dal colimite ordinale del suo sottostante in $\mathcal{U}$ ($\text{colim}(F_g(F))$).
  • La costruzione avviene tramite un quoziente (pushout) che "riempie" i loop distintivi (distinguished loops) presenti nel colimite ordinale, imponendo le condizioni di omotopia richieste dalla struttura di coslice.
  • Formalmente, il colimite in $A/\mathcal{U}$, denotato $\text{colim}_A(F)$, è ottenuto come pushout di $\text{colim}(F_g(F))$ lungo una mappa da $A$ che identifica i percorsi indotti dalla struttura puntata.
• Strumenti Categoriali:
  • Uso di categorie selvagge (wild categories) come quadro categorico flessibile per la teoria omotopica sintetica.
  • Analisi dei sistemi di fattorizzazione ortogonale (OFS) e della loro interazione con i funtori di colimite.
  • Dimostrazione che il funtore di dimenticanza $A/\mathcal{U} \to \mathcal{U}$ crea i colimiti su grafi che sono alberi (contractibili).
• Formalizzazione: Una parte significativa del lavoro è stata formalizzata in Agda, inclusa la costruzione del funtore colimite nelle coslice e le prove delle proprietà di preservazione.

3. Contributi Chiave

A. Costruzione e Caratterizzazione dei Colimiti in Coslice

Gli autori forniscono una costruzione esplicita del colimite in $A/\mathcal{U}$ (Sezione 5.4) che lo lega direttamente ai colimiti in $\mathcal{U}$.

• Teorema 5.4.3: Dimostrano che la loro costruzione soddisfa la proprietà universale del colimite in $A/\mathcal{U}$.
• Creazione di Colimiti: Dimostrano che il funtore di dimenticanza crea (preserva e riflette) i colimiti quando il diagramma è indicizzato da un albero (Corollario 5.4.6). Questo è un risultato fondamentale perché le categorie di coslice non sono generalmente localmente cartesiane chiuse (LCC), ma su alberi si comportano bene.

B. Conservazione della Connessione e Gruppi Superiori

Uno dei risultati più significativi riguarda l'interazione tra colimiti e sistemi di fattorizzazione ortogonale.

• Preservazione della Connessione: Dimostrano che i colimiti in $A/\mathcal{U}$ preservano la classe sinistra di un sistema di fattorizzazione ortogonale su $\mathcal{U}$ (Sezione 7).
• Applicazione ai Gruppi Superiori: Poiché la connessione $n$ è definita tramite un OFS, ne consegue che i colimiti di tipi puntati $n$-connessi sono ancora $n$-connessi.
• Chiusura delle Categorie di Gruppi: Questo implica che la categoria dei gruppi superiori (k-tuply groupal n-groupoids, definita da Buchholtz, van Doorn e Rijke) è cocomplete (ammette tutti i colimiti su grafi) per ogni livello di troncamento. Questo risolve un problema aperto sulla completezza di queste categorie in HoTT.

C. Costruzione Alternativa (Pushout di Coprodotto)

Nella Sezione 5.5, gli autori derivano una seconda costruzione dei colimiti in coslice come un pushout di coprodotto (analogamente a un lemma classico nella teoria delle categorie). Questa costruzione è utile per collegare i colimiti alle sequenze di Mayer-Vietoris.

D. Continuità Debole della Cohomologia

Nella Sezione 8, gli autori studiano l'interazione tra colimiti e teorie di coomologia (di Eilenberg-Steenrod).

• Dimostrano che, assumendo l'assioma della scelta interno, la coomologia trasforma i colimiti finiti in limiti deboli (weak limits) nella categoria degli insiemi.
• Questo risultato è collegato al teorema di rappresentabilità di Brown e alla validità della sequenza esatta di Mayer-Vietoris per i colimiti finiti in HoTT.

4. Risultati Principali

1. Costruzione Esplicita: Fornita una definizione costruttiva dei colimiti in $A/\mathcal{U}$ che non richiede HITs generali, ma solo pushout e colimiti ordinari.
2. Teorema di Creazione: Il funtore di dimenticanza $A/\mathcal{U} \to \mathcal{U}$ crea i colimiti su alberi.
3. Cocompletezza dei Gruppi Superiori: Le categorie $(n, k)\text{GType}$ sono cocomplete. I colimiti di gruppi superiori sono ancora gruppi superiori.
4. Preservazione della Connessione: I colimiti di tipi puntati $n$-connessi sono $n$-connessi.
5. Relazione con la Cohomologia: I colimiti finiti in $A/\mathcal{U}$ sono mappati in limiti deboli da teorie di coomologia additive.

5. Significato e Impatto

• Fondamenti Teorici: Il lavoro colma un divario tra la teoria delle categorie sintetica e la costruzione pratica dei colimiti in contesti puntati, fornendo un modello chiaro di come la struttura di coslice influenzi l'omotopia.
• Algebra Omotopica: La dimostrazione della cocompletezza delle categorie di gruppi superiori è un passo cruciale per lo sviluppo dell'algebra omotopica in HoTT, permettendo di costruire nuovi oggetti algebrici (come gruppi abeliani superiori) tramite colimiti.
• Verifica Formale: La formalizzazione in Agda garantisce l'assenza di errori nelle complesse dimostrazioni omotopiche (coerenza di percorsi, identità di zig-zag, ecc.), offrendo una base solida per futuri sviluppi nella teoria dei tipi.
• Generalità: L'uso di categorie selvagge e la separazione tra la struttura dell'universo e quella della coslice rendono i risultati applicabili a una vasta gamma di contesti oltre i semplici tipi puntati.

In sintesi, il paper fornisce gli strumenti tecnici e le prove formali necessarie per trattare i colimiti in contesti puntati in modo rigoroso, aprendo la strada a nuove costruzioni in algebra omotopica sintetica.