Table of Contents
Fetching ...

Constructing linear bicategories

Richard Blute, Rose Kudzman-Blais, Susan Niefield

TL;DR

The paper develops the theory of linear bicategories by introducing LD-quantales and linear quantaloids as the algebraic backbone for two interacting compositions $⊗$ and $⊕$ linked by a linear distribution. It shows that the quantaloid $Q$-Rel forms a linear bicategory precisely when $Q$ is an LD-quantale, with Girard cases delivering a full dualizing structure. A broad array of examples is constructed, including both locally posetal and non-posetal settings such as $ ext{Loc}$, $ ext{Quant}$, and $ ext{Qtld}$, and enriched versions $Q$-Mod and related matrices and monads are developed to yield new linear bicategorical structures. The work connects linear logic semantics, monoidal topology, and enriched bicategory theory, providing a versatile framework for linear-distributive semantics across quantales and quantaloids and their enriched categories. This yields cyclic $*$-autonomous bicategories and closed/auto structures useful for modeling linear logic fragments and generalized metric-like spaces.

Abstract

Linearly distributive categories were introduced to model the tensor/par fragment of linear logic, without resorting to the use of negation. Linear bicategories are the bicategorical version of linearly distributive categories. Essentially, a linear bicategory has two forms of composition, each determining the structure of a bicategory, and the two compositions are related by a linear distribution. The main goal of this paper is to demonstrate that there are many examples of linear bicategories, which are obtained by considering quantales and quantaloids. It is standard in the field of monoidal topology that the category of quantale-valued relations is a bicategory. Here we begin by showing that a quantale is Girard if and only if the corresponding bicategory is a Girard quantaloid, which is an example of linear bicategory. The tropical and arctic semiring structures fit together into a Girard quantale, so this construction is likely to have multiple applications. More generally, we define LD-quantales, which are sup-lattices with two quantale structures related by a linear distribution, and their bicategorical analogue, linear quantaloids. We show that Q-Rel is a linear quantaloid if and only if Q is an LD-quantale. We then consider several standard constructions from enriched bicategory theory, and show that these lift to the linear quantaloid setting and produce new examples of linear bicategories. In particular, we consider linear Q-categories, matrices in Q and linear monads in Q, where Q is a linear quantaloid. We develop non-locally posetal examples as well, Quant, the bicategory of quantales, modules and module homomorphisms, and Qtld, the bicategory of quantaloids, modules and module homomorphisms. These turn out to be cyclic *-autonomous bicategories, which are in essence a closed version of linear bicategories.

Constructing linear bicategories

TL;DR

The paper develops the theory of linear bicategories by introducing LD-quantales and linear quantaloids as the algebraic backbone for two interacting compositions and linked by a linear distribution. It shows that the quantaloid -Rel forms a linear bicategory precisely when is an LD-quantale, with Girard cases delivering a full dualizing structure. A broad array of examples is constructed, including both locally posetal and non-posetal settings such as , , and , and enriched versions -Mod and related matrices and monads are developed to yield new linear bicategorical structures. The work connects linear logic semantics, monoidal topology, and enriched bicategory theory, providing a versatile framework for linear-distributive semantics across quantales and quantaloids and their enriched categories. This yields cyclic -autonomous bicategories and closed/auto structures useful for modeling linear logic fragments and generalized metric-like spaces.

Abstract

Linearly distributive categories were introduced to model the tensor/par fragment of linear logic, without resorting to the use of negation. Linear bicategories are the bicategorical version of linearly distributive categories. Essentially, a linear bicategory has two forms of composition, each determining the structure of a bicategory, and the two compositions are related by a linear distribution. The main goal of this paper is to demonstrate that there are many examples of linear bicategories, which are obtained by considering quantales and quantaloids. It is standard in the field of monoidal topology that the category of quantale-valued relations is a bicategory. Here we begin by showing that a quantale is Girard if and only if the corresponding bicategory is a Girard quantaloid, which is an example of linear bicategory. The tropical and arctic semiring structures fit together into a Girard quantale, so this construction is likely to have multiple applications. More generally, we define LD-quantales, which are sup-lattices with two quantale structures related by a linear distribution, and their bicategorical analogue, linear quantaloids. We show that Q-Rel is a linear quantaloid if and only if Q is an LD-quantale. We then consider several standard constructions from enriched bicategory theory, and show that these lift to the linear quantaloid setting and produce new examples of linear bicategories. In particular, we consider linear Q-categories, matrices in Q and linear monads in Q, where Q is a linear quantaloid. We develop non-locally posetal examples as well, Quant, the bicategory of quantales, modules and module homomorphisms, and Qtld, the bicategory of quantaloids, modules and module homomorphisms. These turn out to be cyclic *-autonomous bicategories, which are in essence a closed version of linear bicategories.
Paper Structure (19 sections, 35 theorems, 97 equations)

This paper contains 19 sections, 35 theorems, 97 equations.

Key Result

Lemma 2.9

Hofmann_Seal_Tholen_2014 If $Q$ is a unital quantale, then $Q$-${\sf Rel}$ is a quantaloid under point-wise ordering, so in particular it is a locally posetal bicategory.

Theorems & Definitions (102)

  • Remark 1.1
  • Definition 2.1
  • Example 2.3
  • Definition 2.4
  • Remark 2.5
  • Example 2.6
  • Definition 2.7
  • Definition 2.8
  • Lemma 2.9
  • Example 2.10
  • ...and 92 more