Catégorie *-autonome

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

En mathématiques, une catégorie *-autonome (lire « étoile-autonome » ou « star-autonome ») est une structure étudiée en théorie des catégories.

Il s'agit plus précisément d'une catégorie qui possède un objet dit « dualisant » et qui vérifie un jeu d'axiomes précis. Cette structure rend compte de plusieurs situations essentielles qui apparaissent naturellement en logique mathématique, en topologie, en informatique théorique et en physique théorique et a été introduite par le mathématicien américain Michael Barr (en) en 1979.

Le terme « *-autonome » fait écho à la notion de catégorie rigide (en), aussi dite « autonome », qui est une catégorie où la notion de dual peut être définie.

Définition[modifier | modifier le code]

Catégorie *-autonome ordinaire[modifier | modifier le code]

Définition explicite[modifier | modifier le code]

Soit \langle C, \otimes, 1\rangle une catégorie monoïdale symétrique fermée, dont le foncteur Hom interne est noté \multimap. C est une catégorie *-autonome si elle est équipée d'un objet dualisant \bot et pour tout objet A, d'un isomorphisme :

d_A : A \to \left(A \multimap \bot \right) \multimap \bot .

Cette application n'est autre que la transposée de l'application d'évaluation :

\mathrm{eval}_{A, \bot} : (A \multimap \bot) \otimes A \to \bot

Le fait qu'il s'agisse d'un isomorphisme permet de donner un sens à la double négation, et donc de rendre compte de logiques plus flexibles que la logique intuitionniste.

Définition implicite[modifier | modifier le code]

Une définition alternative, mais équivalente, est de considérer sur cette catégorie C le foncteur

(-)^{*} = (-) \multimap \bot

et de demander qu'existe une bijection naturelle

\mathrm{Hom}(X\otimes Y,Z^*)\simeq\mathrm{Hom}(X,(Y\otimes Z)^*)

Le rôle de l'objet dualisant \bot est alors joué par 1^{*}.

Catégorie *-autonome enrichie[modifier | modifier le code]

Soit V une catégorie monoïdale, il existe une notion de catégorie *-autonome V-enrichie. Elle coïncide avec la notion classique lorsque V = Set.

Un V-foncteur F : A → B est dit essentiellement surjectif sur les objets lorsque tout objet de B est isomorphe à Fa pour un objet a de A. Une *-opération à gauche est un V-foncteur

S : A \to A^{\mathrm{op}}

associé à la famille V-naturelle d'isomorphismes

\operatorname{Hom}_A (X\otimes Y, SZ) \simeq \operatorname{Hom}_A(X, S(Y \otimes Z)).

Une V-catégorie *-autonome est une V-catégorie monoïdale équipée d'une *-opération à gauche pleine et fidèle. Ces catégories sont en particulier fermées, et l'objet dualisant est SI.

Exemples[modifier | modifier le code]

  • Les espaces de cohérence (en) en logique linéaire, introduits par Jean-Yves Girard, sont des catégories *-autonomes. En effet la structure *-autonome permet de rendre compte des opérations de cette logique : si on note X^\bot = (X \multimap \bot), on observe que X est canoniquement isomorphe à X^{\bot\bot} et on peut définir l'opération « par » X ⅋ Y comme (X^\bot \otimes Y^\bot)^\bot.
  • La catégorie des k-espaces vectoriels de dimension finie, où k est un corps, est *-autonome. Le corps de base joue le rôle de l'objet dualisant, et le dual usuel (c'est-à-dire en tant qu'espace vectoriel dual) V* est exactement le dual au sens *-autonome. La catégorie de tous les k-espaces vectoriels (non nécessairement de dimension finie) n'est en revanche pas *-autonome.
  • Les espaces de Chu (en), qui généralisent les espaces topologiques, sont naturellement dotés d'une structure *-autonome, et sont en particulier utilisés pour modéliser les automates et les problèmes de concurrence.

Voir aussi[modifier | modifier le code]

Références[modifier | modifier le code]

  • (en) Michael Barr, *-autonomous categories, vol. 752, Springer-Verlag, coll. « Lecture Notes in Mathematics »,‎ 1979
  • (en) Michael Barr, « *-autonomous categories and linear logic », Mathematical Structures in Computer Science, vol. 1,‎ 1991, p. 159-178
  • (en) Michael Barr, « *-autonomous categories: once more around the track », Theory and Applications of Categories, vol. 6,‎ 1999, p. 5-24
  • (en) Michael Barr, « Non-symmetric *-autonomous categories », Theoretical Computer Science, vol. 139,‎ 1995, p. 115-130
  • (en) Jean-Yves Girard, Yves Lafont et Paul Taylor, Proofs and types, Cambridge University Press,‎ 1989
  • (en) Ross Street, « Quantum categories, star autonomy, and quantum groupoids », Galois theory, Hopf algebras, and semiabelian categories, vol. 43,‎ 2004, p. 187 (lire en ligne)