1. Frobenius structures in star-autonomous categories
- Author
-
de Lacroix, Cédric, Santocanale, Luigi, Laboratoire d'Informatique et Systèmes (LIS), Aix Marseille Université (AMU)-Université de Toulon (UTLN)-Centre National de la Recherche Scientifique (CNRS), Logique, Interaction, Raisonnement et Inférence, Complexité, Algèbre (LIRICA), Aix Marseille Université (AMU)-Université de Toulon (UTLN)-Centre National de la Recherche Scientifique (CNRS)-Aix Marseille Université (AMU)-Université de Toulon (UTLN)-Centre National de la Recherche Scientifique (CNRS), Algorithmique, Combinatoire et Recherche Opérationnelle (ACRO), and ANR-21-CE48-0017,LambdaComb,une expédition cartographique entre le lambda-calcul, la logique, et la combinatoire(2021)
- Subjects
FOS: Computer and information sciences ,Computer Science - Logic in Computer Science ,adjoint ,Theory of computation → Linear logic ,Girard quantale ,Frobenius quantale ,nuclear object ,[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] ,Mathematics - Category Theory ,Mathematics - Logic ,star-autonomous category ,Logic in Computer Science (cs.LO) ,[MATH.MATH-LO]Mathematics [math]/Logic [math.LO] ,Quantale ,Theory of computation → Proof theory ,FOS: Mathematics ,Category Theory (math.CT) ,associative algebra ,Theory of computation → Constructive mathematics ,Logic (math.LO) ,[MATH.MATH-CT]Mathematics [math]/Category Theory [math.CT] - Abstract
It is known that the quantale of sup-preserving maps from a complete lattice to itself is a Frobenius quantale if and only if the lattice is completely distributive. Since completely distributive lattices are the nuclear objects in the autonomous category of complete lattices and sup-preserving maps, we study the above statement in a categorical setting. We introduce the notion of Frobenius structure in an arbitrary autonomous category, generalizing that of Frobenius quantale. We prove that the monoid of endomorphisms of a nuclear object has a Frobenius structure. If the environment category is star-autonomous and has epi-mono factorizations, a variant of this theorem allows to develop an abstract phase semantics and to generalise the previous statement. Conversely, we argue that, in a star-autonomous category where the monoidal unit is a dualizing object, if the monoid of endomorphisms of an object has a Frobenius structure and the monoidal unit embeds into this object as a retract, then the object is nuclear., LIPIcs, Vol. 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023), pages 18:1-18:20
- Published
- 2022
- Full Text
- View/download PDF