Cartesian isomorphisms are symmetric monoidal: A justification of linear logic

1999 ◽  
Vol 64 (1) ◽  
pp. 227-242 ◽  
Author(s):  
Kosta Došen ◽  
Zoran Petrić
Keyword(s):  
Monoidal Category ◽  
Linear Logic ◽  
Symmetric Monoidal Category

AbstractIt is proved that all the isomorphisms in the cartesian category freely generated by a set of objects (i.e., a graph without arrows) can be written in terms of arrows from the symmetric monoidal category freely generated by the same set of objects. This proof yields an algorithm for deciding whether an arrow in this free cartesian category is an isomorphism.

scholarly journals An explicit formula for the free exponential modality of linear logic

2017 ◽  
Vol 28 (7) ◽  
pp. 1253-1286 ◽  
Author(s):  
PAUL-ANDRÉ MELLIÈS ◽  
NICOLAS TABAREAU ◽  
CHRISTINE TASSON
Keyword(s):  
Tensor Product ◽  
Explicit Formula ◽  
Monoidal Category ◽  
Linear Logic ◽  
Double Negation ◽  
Symmetric Monoidal Category ◽  
Algebraic Description ◽  
Classical Duality ◽  
First Time ◽  
Coherence Spaces

The exponential modality of linear logic associates to every formula A a commutative comonoid !A which can be duplicated in the course of reasoning. Here, we explain how to compute the free commutative comonoid !A as a sequential limit of equalizers in any symmetric monoidal category where this sequential limit exists and commutes with the tensor product. We apply this general recipe to a series of models of linear logic, typically based on coherence spaces, Conway games and finiteness spaces. This algebraic description unifies for the first time a number of apparently different constructions of the exponential modality in spaces and games. It also sheds light on the duplication policy of linear logic, and its interaction with classical duality and double negation completion.

scholarly journals Twin TQFTs and Frobenius Algebras

2013 ◽  
Vol 2013 ◽  
pp. 1-25
Author(s):  
Carmen Caprau
Keyword(s):  
Monoidal Category ◽  
Topological Quantum Field Theory ◽  
Algebra Homomorphism ◽  
Frobenius Algebra ◽  
Quantum Field ◽  
Generators And Relations ◽  
Symmetric Monoidal Category ◽  
Frobenius Algebras ◽  
Topological Quantum ◽  
Algebraic Description

We introduce the category of singular 2-dimensional cobordisms and show that it admits a completely algebraic description as the free symmetric monoidal category on atwin Frobenius algebra, by providing a description of this category in terms of generators and relations. A twin Frobenius algebra(C,W,z,z∗)consists of a commutative Frobenius algebraC, a symmetric Frobenius algebraW, and an algebra homomorphismz:C→Wwith dualz∗:W→C, satisfying some extra conditions. We also introduce a generalized 2-dimensional Topological Quantum Field Theory defined on singular 2-dimensional cobordisms and show that it is equivalent to a twin Frobenius algebra in a symmetric monoidal category.

Monad compositions II: Kleisli strength

2008 ◽  
Vol 18 (3) ◽  
pp. 613-643 ◽  
Author(s):  
ERNIE MANES ◽  
PHILIP MULRY
Keyword(s):  
Monoidal Category ◽  
Linear Equations ◽  
Large Collection ◽  
Data Types ◽  
Cartesian Closed Category ◽  
Closed Category ◽  
Symmetric Monoidal Category ◽  
Cartesian Closed

In this paper we introduce the concept of Kleisli strength for monads in an arbitrary symmetric monoidal category. This generalises the notion of commutative monad and gives us new examples, even in the cartesian-closed category of sets. We exploit the presence of Kleisli strength to derive methods for generating distributive laws. We also introduce linear equations to extend the results to certain quotient monads. Mechanisms are described for finding strengths that produce a large collection of new distributive laws, and consequently monad compositions, including the composition of monadic data types such as lists, trees, exceptions and state.

scholarly journals Abstract bivariant Cuntz semigroups II

2020 ◽  
Vol 32 (1) ◽  
pp. 45-62 ◽  
Author(s):  
Ramon Antoine ◽  
Francesc Perera ◽  
Hannes Thiel
Keyword(s):  
Tensor Product ◽  
Monoidal Category ◽  
Additional Structure ◽  
Mild Conditions ◽  
Symmetric Monoidal Category

AbstractWe previously showed that abstract Cuntz semigroups form a closed symmetric monoidal category. This automatically provides additional structure in the category, such as a composition and an external tensor product, for which we give concrete constructions in order to be used in applications. We further analyze the structure of not necessarily commutative {\mathrm{Cu}}-semirings, and we obtain, under mild conditions, a new characterization of solid {\mathrm{Cu}}-semirings R by the condition that {R\cong\llbracket R,R\rrbracket}.

scholarly journals Tannakization in derived algebraic geometry

2014 ◽  
Vol 14 (3) ◽  
pp. 642-700 ◽  
Author(s):  
Isamu Iwanari
Keyword(s):  
Algebraic Geometry ◽  
Galois Group ◽  
Monoidal Category ◽  
Group Scheme ◽  
Affine Group ◽  
Stable Category ◽  
Group Schemes ◽  
Symmetric Monoidal Category ◽  
Derived Algebraic Geometry ◽  
Mixed Motives

AbstractIn this paper we begin studying tannakian constructions in ∞-categories and combine them with the theory of motivic categories developed by Hanamura, Levine, and Voevodsky. This paper is the first in a series of papers. For the purposes above, we first construct a derived affine group scheme and its representation category from a symmetric monoidal ∞-category, which we shall call the tannakization of a symmetric monoidal ∞-category. It can be viewed as an ∞-categorical generalization of work of Joyal-Street and Nori. Next we apply it to the stable ∞-category of mixed motives equipped with the realization functor of a mixed Weil cohomology. We construct a derived motivic Galois group which represents the automorphism group of the realization functor, and whose representation category satisfies an appropriate universal property. As a consequence, we construct an underived motivic Galois group of mixed motives, which is a pro-algebraic group and has nice properties. Also, we present basic properties of derived affine group schemes in the Appendix.

Hopf Quasimodules and Yetter-Drinfeld Modules over Hopf Quasigroups

2021 ◽  
Vol 28 (02) ◽  
pp. 213-242
Author(s):  
Tao Zhang ◽  
Yue Gu ◽  
Shuanhong Wang
Keyword(s):  
Monoidal Category ◽  
Drinfeld Modules ◽  
Braided Monoidal Category ◽  
Symmetric Monoidal Category ◽  
Category Equivalence ◽  
Hopf Modules ◽  
Hopf Quasigroup

We introduce the notions of a four-angle Hopf quasimodule and an adjoint quasiaction over a Hopf quasigroup [Formula: see text] in a symmetric monoidal category [Formula: see text]. If [Formula: see text] possesses an adjoint quasiaction, we show that symmetric Yetter-Drinfeld categories are trivial, and hence we obtain a braided monoidal category equivalence between the category of right Yetter-Drinfeld modules over [Formula: see text] and the category of four-angle Hopf modules over [Formula: see text] under some suitable conditions.

scholarly journals On geometry of interaction for polarized linear logic

2017 ◽  
Vol 28 (10) ◽  
pp. 1639-1694
Author(s):  
MASAHIRO HAMANO ◽  
PHILIP SCOTT
Keyword(s):  
Proof Theory ◽  
Monoidal Category ◽  
Linear Logic ◽  
Cut Elimination ◽  
List Type ◽  
Monoidal Categories ◽  
Categorical Structure ◽  
Categorical Models ◽  
Focusing Property ◽  
Special Case

We present Geometry of Interaction (GoI) models for Multiplicative Polarized Linear Logic, MLLP, which is the multiplicative fragment of Olivier Laurent's Polarized Linear Logic. This is done by uniformly adding multi-points to various categorical models of GoI. Multi-points are shown to play an essential role in semantically characterizing the dynamics of proof networks in polarized proof theory. For example, they permit us to characterize the key feature of polarization, focusing, as well as being fundamental to our construction of concrete polarized GoI models.Our approach to polarized GoI involves following two independent studies, based on different categorical perspectives of GoI: (i)Inspired by the work of Abramsky, Haghverdi and Scott, a polarized GoI situation is defined in which multi-points are added to a traced monoidal category equipped with a reflexive object U. Using this framework, categorical versions of Girard's execution formula are defined, as well as the GoI interpretation of MLLP proofs. Running the execution formula is shown to characterize the focusing property (and thus polarities) as well as the dynamics of cut elimination.(ii)The Int construction of Joyal–Street–Verity is another fundamental categorical structure for modelling GoI. Here, we investigate it in a multi-pointed setting. Our presentation yields a compact version of Hamano–Scott's polarized categories, and thus denotational models of MLLP. These arise from a contravariant duality between monoidal categories of positive and negative objects, along with an appropriate bimodule structure (representing ‘non-focused proofs’) between them.Finally, as a special case of (ii) above, a compact model of MLLP is also presented based on Rel (the category of sets and relations) equipped with multi-points.

Sign in / Sign up

Export Citation Format

Share Document