Catégorie *-autonome

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 Modèle:Lien en 1979.

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

Définition

Catégorie *-autonome ordinaire

Définition explicite

Soit $⟨C,\otimes ,1⟩$ une catégorie monoïdale symétrique fermée, dont le foncteur Hom interne est noté $⊸$. C est une catégorie *-autonome si elle est équipée d'un objet dualisant $\mathrm{\perp }$ et pour tout objet A, d'un isomorphisme :

$d_A:A\to (A⊸\mathrm{\perp })⊸\mathrm{\perp }$.

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

${\mathrm{e}\mathrm{v}\mathrm{a}\mathrm{l}}_{A,\mathrm{\perp }}:(A⊸\mathrm{\perp })\otimes A\to \mathrm{\perp }$

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

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

$(-{)}^{*}=(-)⊸\mathrm{\perp }$

et de demander qu'existe une bijection naturelle

$\mathrm{H}\mathrm{o}\mathrm{m}(X\otimes Y,Z^{*})\simeq \mathrm{H}\mathrm{o}\mathrm{m}(X,(Y\otimes Z{)}^{*})$

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

Catégorie *-autonome enrichie

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{o}\mathrm{p}}$

associé à la famille V-naturelle d'isomorphismes

${\mathrm{Hom}}_A(X\otimes Y,SZ)\simeq {\mathrm{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

• Les Modèle:Lien 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^{\mathrm{\perp }}=(X⊸\mathrm{\perp })$, on observe que $X$ est canoniquement isomorphe à $X^{\mathrm{\perp }\mathrm{\perp }}$ et on peut définir l'opération « par » X ⅋ Y comme $(X^{\mathrm{\perp }}\otimes Y^{\mathrm{\perp }}{)}^{\mathrm{\perp }}$.
• 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 Modèle:Lien, 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

• Modèle:Lien
• Modèle:Lien
• Logique linéaire

Références

• Modèle:Ouvrage
• Modèle:Article
• Modèle:Article
• Modèle:Article
• Modèle:Ouvrage
• Modèle:Article