Catégorie *-autonome

Summarize Timeline Fact Check

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

${\displaystyle 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 :

${\displaystyle \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.

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

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

et de demander qu'existe une bijection naturelle

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

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

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

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

associé à la famille V-naturelle d'isomorphismes

${\displaystyle \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.