Instances of models of double-categorical theories
Carlson, Patterson
We contribute a chapter in common to categorical database theory and to the study of higher morphisms between double categories. The common thread here is the notion of instance, or right module, which we generalize from functors from a plain category into Set to the models of a (cartesian) double theory. This provides a concept of instance for such objects as a category equipped with a monad, or a (symmetric) multicategory, recovering the multifunctors into Set in the latter case. We also show that instances of models are equivalent to an appropriate concept of discrete opfibration over that model, not recoverable as the representable discrete opfibrations in the 2-category of models. Finally, we give comprehensive factorization systems with these discrete opfibrations as the right class.
academic
Istanze di modelli di teorie doppiamente categoriali
Questo articolo fornisce contributi congiunti alla ricerca sulla teoria dei database categoriali e sui morfismi di ordine superiore tra bicategorie. Il filo conduttore comune è il concetto di istanza o modulo destro, che gli autori generalizzano dai funtori da categorie ordinarie a Set ai modelli di teorie (cartesiane) doppiamente categoriali. Ciò fornisce un concetto di istanza per oggetti come categorie con monadi o (simmetriche) multicategorie, e nel caso di quest'ultime recupera i multifuntori verso Set. Gli autori dimostrano inoltre che le istanze di un modello sono equivalenti a un concetto appropriato di discreti opfibrati sul modello, che non può essere recuperato come opfibrati discreti rappresentabili nella 2-categoria dei modelli. Infine, viene fornito un sistema di fattorizzazione sintetico con questi opfibrati discreti come classe destra.
Necessità dello sviluppo della teoria delle bicategorie: La moderna teoria debole delle bicategorie ha origine dalla collaborazione tra Paré e Grandis, la cui "idea principale" è studiare in pseudobicategorie le frecce che sono troppo lasse (come profuntori, span, relazioni) o troppo rigide (come aggiunzioni) per ammettere limiti, associandole a frecce più ordinarie (orizzontali).
Esigenze della teoria dei database categoriali: Spivak e Kent hanno inaugurato la teoria dei database categoriali, considerando piccole categorie C come ontologie o schemi di database, e database concreti come C-insiemi. Questa idea è stata estesa nella teoria delle categorie applicata, includendo database algebrici e C-insiemi attributati.
Impulso dalle applicazioni software: L'applicazione CatColab sviluppata dagli autori presso il Topos Institute si basa sulla teoria dei funtori lassi di Paré verso Span, interpretando piccole bicategorie come teorie doppiamente (Lawvere) categoriali e funtori lassi che preservano la struttura come modelli della teoria.
Il concetto tradizionale di istanza (come C-insiemi corrispondenti a moduli I 7→ C) non può essere direttamente generalizzato in teorie doppiamente categoriali generali. Quando X è un modello di una teoria doppiamente categoriale che ammette profrecce non banali, il modello 1, sebbene sia terminale rispetto alle frecce compatte del modello, è sufficientemente ricco per agire non banalmente sul lato sinistro del modulo.
Definizione del concetto di istanza per modelli di teorie doppiamente categoriali: Generalizza il concetto di istanza da categorie ordinarie a teorie doppiamente categoriali generali, risolvendo difficoltà tecniche richiedendo che "I agisca banalmente sul lato sinistro".
Stabilimento della rappresentazione di tipo presheaf delle istanze: Dimostra che la categoria delle istanze di qualsiasi modello X è equivalente alla categoria dei funtori κ(X) → Set, dove κ(X) è il "collage" di X.
Stabilimento dell'equivalenza tra istanze e opfibrati discreti: Il teorema principale dimostra l'equivalenza tra istanze di un modello e opfibrati discreti su quel modello, generalizzando l'equivalenza classica tra copresheaf e opfibrati discreti su categorie.
Costruzione di un sistema di fattorizzazione sintetico: Utilizzando la rappresentabilità locale della categoria dei modelli, costruisce un sistema di fattorizzazione sintetico con opfibrati discreti come classe destra.
Generalizzazione al caso cartesiano: Estende tutti i risultati a teorie doppiamente categoriali cartesiane, coprendo esempi importanti come teorie di Lawvere e multicategorie simmetriche.
Il compito centrale di questo articolo è definire un concetto appropriato di istanza per un modello X di una teoria doppiamente categoriale D, tale che soddisfi:
Generalizzazione del concetto di copresheaf per categorie ordinarie
Sia D una teoria doppiamente categoriale ed E una bicategoria con oggetto terminale I. D ha un modello terminale I in E. Un'istanza del modello X è un modulo H: I 7→ X che soddisfa "I agisce banalmente sul lato sinistro", cioè tutti i lassatori della forma seguente sono identità:
La condizione di "azione banale sul lato sinistro" risolve elegantemente le difficoltà tecniche nella definizione di istanza in teorie doppiamente categoriali generali, evitando i problemi della generalizzazione diretta nel caso di profrecce non banali.
La costruzione κ fornisce un metodo sistematico per "appiattire" la struttura bicategoriale in una categoria ordinaria, permettendo l'utilizzo della teoria classica dei presheaf.
Estende il concetto classico di opfibrato discreto ai modelli di teorie doppiamente categoriali, richiedendo la condizione di pullback in ogni profreccia.
Per un modello X: D → Span di una teoria doppiamente categoriale semplice, la categoria delle istanze Inst(X) è equivalente alla categoria dei funtori Cat(κX, Set).
Fissato un modello B di una teoria doppiamente categoriale semplice D, esiste un'equivalenza
∇: Dopf(B) ⇄ Inst(B): ∫
tra la categoria degli opfibrati discreti su B e la categoria delle istanze di B.
Teorie Modali: L'articolo anticipa le teorie doppiamente categoriali virtuali modali come base più conveniente per codificare teorie doppiamente categoriali di Lawvere non semplici
Equipaggiamenti Virtuali: Considerare la generalizzazione della teoria al contesto degli equipaggiamenti virtuali
Strutture di Ordine Superiore: Ricerca di strutture bicategoriali di ordine superiore e della loro teoria delle istanze
L'articolo cita 51 importanti riferimenti bibliografici, coprendo:
Letteratura fondamentale sulla teoria delle bicategorie (Grandis & Paré, Verity, ecc.)
Teoria dei database categoriali (Spivak & Kent, ecc.)
Teoria delle categorie localmente rappresentabili (Adámek & Rosický, ecc.)
Teoria degli opfibrati e dei sistemi di fattorizzazione (Street & Walters, ecc.)
Questo articolo è un importante contributo teorico nel campo interdisciplinare tra teoria delle bicategorie e teoria dei database categoriali, fornendo nuove prospettive e strumenti per comprendere e applicare i modelli di teorie doppiamente categoriali. La sua profondità tecnica e completezza teorica lo rendono un riferimento importante in questo campo.