Instances de modèles de théories double-catégoriques

Informations fondamentales

• ID de l'article: 2510.08861
• Titre: Instances de modèles de théories double-catégoriques
• Auteurs: Kevin Carlson, Evan Patterson (Topos Institute)
• Classification: math.CT (Théorie des catégories)
• Date de soumission: 9 octobre 2025
• Lien de l'article: https://arxiv.org/abs/2510.08861

Résumé

Cet article apporte des contributions conjointes à la théorie des bases de données catégoriques et aux morphismes d'ordre supérieur entre double-catégories. Le fil conducteur commun est le concept d'instance ou de module droit, que les auteurs généralisent des foncteurs de catégories ordinaires vers Set aux modèles de (double-)théories (cartésiennes). Cela fournit une notion d'instance pour des objets tels que les catégories munies de monades ou les (multi-)catégories (symétriques), récupérant dans ce dernier cas les multi-foncteurs vers Set. Les auteurs démontrent également que les instances d'un modèle sont équivalentes à une notion appropriée de discrètes opfibrations au-dessus de ce modèle, ce qui ne peut pas être récupéré comme des discrètes opfibrations représentables dans la 2-catégorie des modèles. Enfin, un système de factorisation synthétique est fourni avec ces discrètes opfibrations comme classe droite.

Contexte et motivation de la recherche

Contexte du problème

1. Besoin du développement de la théorie double-catégorique: La théorie moderne des faibles double-catégories a commencé par la collaboration de Paré et Grandis, dont l'« idée maîtresse » est d'étudier dans les pseudo-double-catégories les flèches qui sont soit trop relâchées (comme les profuncteurs, les spans, les relations) soit trop strictes (comme les adjoints) pour admettre des limites, en les associant à des flèches plus ordinaires (horizontales).
2. Besoins de la théorie des bases de données catégoriques: Spivak et Kent ont inauguré la théorie des bases de données catégoriques, considérant une petite catégorie C comme une ontologie ou un schéma de base de données, et les bases de données concrètes comme des C-ensembles. Cette idée a été étendue dans la théorie des catégories appliquée, incluant les bases de données algébriques et les C-ensembles attribués.
3. Impulsion des applications logicielles: Les auteurs, au Topos Institute, ont développé l'application CatColab basée sur la théorie des foncteurs relâchés de Paré vers Span, interprétant les petites double-catégories comme des (double-)théories de Lawvere et les foncteurs relâchés préservant la structure comme des modèles de théories.

Problème central

La notion classique d'instance (comme les C-ensembles correspondant aux modules I 7→ C) ne peut pas être directement généralisée aux double-théories générales. Lorsque X est un modèle d'une double-théorie admettant des proarrows non triviaux, bien que le modèle 1 soit terminal par rapport aux morphismes compacts du modèle, il est suffisamment riche pour agir non trivialement sur le côté gauche du module.

Motivation de la recherche

Il est nécessaire de trouver la notion correcte d'instance pour les modèles de double-théories, permettant de:

1. Généraliser le concept de copresheaf des catégories ordinaires
2. S'appliquer à des structures complexes comme les catégories munies de monades, les multi-catégories, etc.
3. Récupérer les multi-foncteurs vers Set dans le cas des multi-catégories
4. Fournir une équivalence avec les discrètes opfibrations

Contributions principales

1. Définition de la notion d'instance pour les modèles de double-théories: Généralisation du concept d'instance des catégories ordinaires aux double-théories générales, résolvant les difficultés techniques en exigeant que « I agisse trivialement sur le côté gauche ».
2. Établissement d'une représentation de type presheaf des instances: Démonstration que la catégorie des instances de tout modèle X est équivalente à la catégorie des foncteurs κ(X) → Set, où κ(X) est le « collage » de X.
3. Établissement de l'équivalence entre instances et discrètes opfibrations: Le théorème principal démontre l'équivalence entre les instances d'un modèle et les discrètes opfibrations au-dessus de ce modèle, généralisant l'équivalence classique entre copresheaves et discrètes opfibrations sur les catégories.
4. Construction d'un système de factorisation synthétique: Utilisant la représentabilité locale de la catégorie des modèles, construction d'un système de factorisation synthétique avec les discrètes opfibrations comme classe droite.
5. Généralisation au cas cartésien: Extension de tous les résultats aux double-théories cartésiennes, couvrant les théories de Lawvere et les multi-catégories symétriques comme exemples importants.

Détails méthodologiques

Définition de la tâche

La tâche centrale de cet article est de définir une notion appropriée d'instance pour un modèle X d'une double-théorie D, satisfaisant:

• Généralisation du concept de copresheaf des catégories ordinaires
• Équivalence avec la notion de discrète opfibration
• Formation d'une catégorie de type presheaf

Définition des instances

Définition préliminaire (Definition 2.1)

Soit D une double-théorie et E une double-catégorie avec objet terminal I. D admet un modèle terminal I dans E. Une instance du modèle X est un module H: I 7→ X satisfaisant « I agit trivialement sur le côté gauche », c'est-à-dire que tous les laxateurs de la forme suivante sont des identités:

I    I    X(z)
 \   |   /
  \  |  /
   \ | /
I ---+--- X(z)

Définition simplifiée (Definition 2.3)

Après simplification structurelle, une instance H est composée des données suivantes:

• Pour chaque objet d∈D, un proarrow Hd: I 7→ Xd
• Pour chaque morphisme compact f: d→d', une cellule Hf
• Pour chaque proarrow m: d 7→ d', une cellule d'action Hm

satisfaisant les axiomes de fonctorialité, naturalité, associativité et unitarité.

Construction du collage (Construction 2.7)

Pour un modèle à valeurs dans Span X: D → Span, on définit son collage κ(X) comme la catégorie:

• Objets: pour chaque d∈D et x∈X(d), on obtient un objet x
• Morphismes: générés par les morphismes compacts et les proarrows
• Relations: préservant la composition, la naturalité, etc.

Discrètes opfibrations

Définition (Definition 3.2)

Un morphisme de modèle p: E → B est une discrète opfibration si pour chaque proarrow m: x 7→ y, le carré

⊤(Em) → Ex
  ↓      ↓
⊤(Bm) → Bx

est un pullback.

Théorème d'équivalence principal

Théorème 3.7

Il existe une équivalence ∇: Dopf(B) ⇄ Inst(B): ∫, où:

• Dopf(B) est la catégorie des discrètes opfibrations au-dessus de B
• Inst(B) est la catégorie des instances de B
• ∫H est appelé le modèle des éléments de l'instance H

Points d'innovation technique

1. Généralisation de la notion d'instance

La condition « d'action triviale sur le côté gauche » résout ingénieusement les difficultés techniques de la définition d'instance dans les double-théories générales, évitant les problèmes de généralisation directe dans le cas de proarrows non triviaux.

2. Innovation de la construction du collage

La construction κ fournit une méthode systématique pour « aplatir » la structure double-catégorique en une catégorie ordinaire, permettant d'exploiter la théorie classique des presheaves.

3. Généralisation du concept de discrète opfibration

Généralisation du concept classique de discrète opfibration aux modèles de double-théories, exigeant la satisfaction d'une condition de pullback à chaque proarrow.

4. Système de factorisation synthétique

Le système de factorisation construit en utilisant la représentabilité locale fournit un outil puissant pour l'étude des morphismes de modèles.

Configuration expérimentale

Vérification théorique

Cet article est principalement un travail théorique en mathématiques pures, dont la correction est vérifiée par:

Vérification par exemples clés

1. Instances de catégories: Vérification que dans le cas de la double-théorie terminale, on récupère les C-ensembles classiques
2. Instances de monades: Démonstration que les instances d'une catégorie munie d'une monade T: X → X sont les X-ensembles H avec transformation naturelle Hη: H → H∘T
3. Instances de multi-catégories: Récupération des multi-foncteurs vers Set dans le cas cartésien

Vérification de construction

Démonstration par traçage détaillé de diagrammes et vérification d'axiomes de:

• La fonctorialité de la construction κ
• L'inversibilité mutuelle des équivalences ∇ et ∫
• L'orthogonalité du système de factorisation

Résultats expérimentaux

Résultats principaux

Proposition 2.8

Pour un modèle X: D → Span d'une double-théorie simple, la catégorie des instances Inst(X) est équivalente à la catégorie des foncteurs Cat(κX, Set).

Théorème 3.7 (Théorème principal)

Fixant un modèle B d'une double-théorie simple D, il existe une équivalence ∇: Dopf(B) ⇄ Inst(B): ∫ entre la catégorie des discrètes opfibrations au-dessus de B et la catégorie des instances de B.

Proposition A.2

La catégorie des modèles Lax(D, Span) d'une double-théorie simple D est localement représentable.

Résultats de généralisation

Théorème 4.5

Pour les double-théories cartésiennes, l'équivalence se restreint à une équivalence entre instances cartésiennes et discrètes opfibrations cartésiennes.

Corollaire 4.6

La catégorie des modèles cartésiens admet un système de factorisation orthogonale avec les discrètes opfibrations comme classe droite.

Résultats d'application

Vérification par des exemples concrets de l'applicabilité de la théorie:

• Les instances de multi-catégories récupèrent les multi-foncteurs M → Set
• Les profuncteurs algébriques comme instances de théories modales
• Traitement unifié des multi-catégories symétriques et cocartésiennes

Travaux connexes

Fondements de la théorie double-catégorique

• Théorie des faibles double-catégories de Paré et Grandis
• Théorie de Yoneda double-catégorique et concept de module de Paré
• Équipements virtuels généralisés de Cruttwell et Shulman

Théorie des bases de données catégoriques

• Travaux fondateurs de Spivak et Kent
• C-ensembles attribués de Patterson et al.
• Bases de données algébriques de Schultz et al.

Théorie des opfibrations

• Systèmes de factorisation synthétiques de Street et Walters
• Foncteurs initiaux dans les ∞-cosmoi de Riehl et Verity
• Théorie générale des discrètes opfibrations représentables en 2-catégories

Conclusion et discussion

Conclusions principales

1. Généralisation réussie de la notion d'instance aux modèles de double-théories générales
2. Établissement de l'équivalence fondamentale entre instances et discrètes opfibrations
3. Fourniture d'un cadre synthétique pour l'étude des morphismes de modèles de double-théories
4. Fondation théorique pour les logiciels d'application tels que CatColab

Limitations

1. La construction κ n'est ni surjective ni fidèle ni conservative, limitant son utilité pour l'étude des propriétés de Lax(D, Span)
2. La catégorie des instances ne dépend pas de presque toutes les données du modèle
3. Actuellement, l'accent est mis principalement sur les modèles à valeurs dans Span; d'autres cas nécessitent des recherches supplémentaires

Directions futures

1. Théories modales: L'article annonce les double-théories virtuelles modales comme base plus pratique pour encoder les double-théories de Lawvere non simples
2. Équipements virtuels: Considération de l'extension de la théorie au cadre des équipements virtuels
3. Structures d'ordre supérieur: Étude des structures double-catégoriques d'ordre supérieur et de leur théorie d'instances

Évaluation approfondie

Avantages

1. Innovation théorique forte: Résolution réussie des difficultés techniques dans la définition d'instance pour les modèles de double-théories
2. Structure complète: Formation d'un système théorique complet allant de la définition au théorème d'équivalence principal aux exemples d'application
3. Profondeur technique: Implication de multiples techniques profondes telles que la théorie double-catégorique, la théorie des opfibrations, et la représentabilité locale
4. Valeur applicative: Fourniture d'une base théorique solide pour la théorie des bases de données catégoriques et les logiciels de modélisation formelle

Insuffisances

1. Seuil technique élevé: Nécessité d'une formation approfondie en théorie des catégories, limitant le public de lecteurs
2. Limitations de la construction κ: Reconnaissance des limitations que κ n'est ni surjective ni fidèle, pouvant affecter certaines applications
3. Exemples relativement peu nombreux: Bien que des exemples clés soient fournis, davantage de scénarios d'application concrète pourraient être souhaités

Impact

1. Contribution théorique: Ouverture de nouvelles directions pour la recherche interdisciplinaire entre la théorie double-catégorique et la théorie des bases de données catégoriques
2. Valeur pratique: Support direct du développement de logiciels de modélisation scientifique tels que CatColab
3. Reproductibilité: Preuves mathématiques détaillées, résultats théoriques vérifiables

Scénarios d'application

1. Développement de logiciels de modélisation scientifique formelle
2. Recherche en théorie des bases de données catégoriques
3. Développement ultérieur de la théorie double-catégorique
4. Applications de la théorie des multi-catégories généralisées et des opérades

Références

Cet article cite 51 références importantes, couvrant:

• Littérature fondamentale en théorie double-catégorique (Grandis & Paré, Verity, etc.)
• Théorie des bases de données catégoriques (Spivak & Kent, etc.)
• Théorie des catégories localement représentables (Adámek & Rosický, etc.)
• Théorie des opfibrations et systèmes de factorisation (Street & Walters, etc.)

Cet article est une contribution théorique importante dans le domaine interdisciplinaire de la théorie double-catégorique et de la théorie des bases de données catégoriques, fournissant de nouvelles perspectives et outils pour comprendre et appliquer les modèles de double-théories. Sa profondeur technique et son intégrité théorique en font une référence importante dans ce domaine.