nLab
linearly distributive category

Context

Monoidal categories

Contents

Idea

A linearly distributive category is a category with two monoidal structures \otimes and \invamp that “distribute” in the sense that there is a map (not necessarily invertible)

δ:A(BC)(AB)C \delta \colon A \otimes (B \parr C) \longrightarrow (A \otimes B) \parr C

Linearly distributive categories are the “representable” form of polycategories, and they are also what “remains” of a star-autonomous category when the involution is forgotten but the dual tensor AB(A *B *) *A\invamp B \coloneqq (A^* \otimes B^*)^* is remembered.

Another way to say essentially the same thing is that a *\ast-autonomous category is like a compact closed category in which the unit and counit of the dual objects refer to two different tensor products: we have AA *\top \to A \parr A^* but A *AA^* \otimes A \to \bot, where (,)(\otimes,\top) and (,)(\parr,\bot) are two different monoidal structures. A linearly distributive category encodes the necessary relationship between two such monoidal structures such that this makes sense, i.e. such that the triangle identities can be stated.

Definition

A linearly distributive category (also called a weakly distributive category) is a monoidal category in two ways, with monoidal structures (,)(\otimes, \top) and (,)(\parr, \bot) equipped with extra associator natural transformations

(1)δ L:A(BC)(AB)C \delta^L:A\otimes (B\parr C) \to (A \otimes B) \parr C
(2)δ R:(AB)CA(BC) \delta^R:(A\parr B) \otimes C \to A \parr (B \otimes C)

and the obvious six pentagon equations and four triangle equations that make the monoidal structures work together nicely. (Some of these equations can be interpreted as saying that the δ\deltas are tensorial strengths for the functors (A)(A\parr -) and (C)(-\parr C) with respect to the \otimes monoidal structure.) A symmetric linearly distributive category is one in which both monoidal structures are symmetric and three squares commute relating the symmetries to the δ\deltas.

These extra associators are sometimes called “distributors”, and should not be confused with profunctors. The term is a pun on the distributivity of multiplication over addition, but “linearized” so that each variable only appears once in the result.

Warning: a distributive category cannot be made into a linearly distributive category with =×\otimes = \times and =+\parr = + unless it is a partial order (but every distributive lattice is indeed a linearly distributive category). See Cockett-Seely for a proof. This mistake is easy to make and even appears in print in one or two places.

Linear functors and transformations

A linear functor F:CDF:C\to D between linearly distributive categories consists of a pair of functors F ,F F_\otimes, F_\parr such that, F F_\otimes is a lax monoidal functor with respect to \otimes, F F_\parr is a colax monoidal functor with respect to \parr, and there are “linear strengths”

F (AB)F (A)F (B) F_\otimes (A\parr B) \to F_\parr(A) \parr F_\otimes (B)
F (AB)F (A)F (B) F_\otimes (A\parr B) \to F_\otimes(A) \parr F_\parr(B)
F (A)F (B)F (AB) F_\otimes (A) \otimes F_\parr(B) \to F_\parr(A\otimes B)
F (A)F (B)F (AB) F_\parr (A) \otimes F_\otimes(B) \to F_\parr(A\otimes B)

satisfying appropriate coherence conditions; see Cockett-Seely 1999. A linear natural transformation FGF\to G consists of a monoidal transformations F G F_\otimes \to G_\otimes and F G F_\parr \to G_\parr satisfying further coherence conditions. This defines a 2-category of linearly distributive categories, which has the property of embedding the 2-category of *\ast-autonomous categories and arbitrary lax monoidal functors (see below).

On the other hand, a linear functor in this sense is more general than a functor between underlying polycategories (see below). The latter probably coincide with linear functors having the property that F =F F_\otimes = F_\parr as functors (so that the same functor FF is \otimes-lax monoidal and \parr-colax monoidal) and the linear strengths are identities. We might call these Frobenius linear functors, since such a 1C1\to C is the same as a Frobenius algebra in CC, and when specialized to the monoidal case =\otimes=\parr they coincide with Frobenius monoidal functors.

Yet stronger is the notion of strong Frobenius linear functor, in which the lax and colax monoidal structures are strong.

Star-autonomous category

Any star-autonomous category has an underlying symmetric linearly distributive category where we define AB(A *B *) *A\parr B \coloneqq (A^* \otimes B^*)^*, or equivalently ABA *BA\parr B \coloneqq A^* \multimap B, where \multimap is the internal-hom. The left distributor, for instance, is obtained as follows:

(AB) *(AB) * A(AB) *B *B *CB *C B *(B *C)C B *(B *C)C A(AB) *(B *C)C A(B *C)(AB) *C\array{\arrayopts{\rowlines{solid}} \array{\arrayopts{\rowlines{solid}} (A\otimes B)^* \longrightarrow (A\otimes B)^* \\ A \otimes (A\otimes B)^* \longrightarrow B^*} \qquad \array{\arrayopts{\rowlines{solid}} B^* \multimap C \longrightarrow B^* \multimap C\\ B^* \otimes (B^* \multimap C) \longrightarrow C\\ B^* \longrightarrow (B^* \multimap C) \multimap C} \\ A \otimes (A\otimes B)^* \longrightarrow (B^* \multimap C) \multimap C \\ A\otimes (B^*\multimap C) \longrightarrow (A \otimes B)^* \multimap C }

Conversely, we say that a symmetric linearly distributive category with monoidal structures (,)(\otimes,\top) and (,)(\parr,\bot) has a negation if every object AA has a dual ¬A\neg A and arrows

A¬A,¬AA\top \to A \parr \neg A, \qquad \neg A \otimes A \to \bot

subject to triangular equations

1 A=(AA(A¬A)AdistA(¬AA)AA)1_A = \left( A \cong \top \otimes A \to (A \parr \neg A) \otimes A \stackrel{dist}{\to} A \parr (\neg A \otimes A) \to A \parr \bot \cong A \right)
\,
1 ¬A=(¬A¬A¬A(A¬A)dist(¬AA)¬A¬A¬A).1_{\neg A} = \left( \neg A \cong \neg A \otimes \top \to \neg A \otimes (A \parr \neg A) \stackrel{dist}{\to} (\neg A \otimes A) \parr \neg A \to \bot \parr \neg A \cong \neg A \right).

Then symmetric linearly distributive categories with negations are the same as *\ast-autonomous categories; see (Cockett-Seely 97). Moreover:

  • the forgetful functor from *\ast-autonomous categories to symmetric linearly distributive ones has a left adjoint that “freely adjoins negations”. I don’t know which kind of functors this statement refers to, but it’s probably strong Frobenius ones.

  • This functor also has a right adjoint that picks out the “nucleus” of dualizable objects (in the linear sense); see Cockett-Seely 1999. This adjunction uses lax monoidal functors between *\ast-autonomous categories and linear functors between linearly distributive categories.

  • Analogous facts hold relating non-symmetric linearly distributive categories with non-symmetric star-autonomous categories?.

Polycategories

Any linearly distributive category has an underlying polycategory where we define Hom(A 1,,A n;B 1,,B m)Hom(A_1,\dots,A_n; B_1,\dots,B_m) to be Hom(A 1A n;B 1B m)Hom(A_1\otimes \cdots \otimes A_n; B_1 \parr \cdots \parr B_m). The polycategorical compositions are obtained using the distributors. For instance, we should be able to compose f:(A,B)(C,D,E)f:(A,B) \to (C,D,E) with g:(F,D,G)Hg:(F,D,G) \to H to get gf:(F,A,B,G)(C,H,E)g\circ f : (F,A,B,G) \to (C,H,E); in a linearly distributive category this is the composite

F(AB)G 1 Ff1 GF(CDE)G δ((F(CD))E)G δ((C(FD))E)G ((CE)(FD))G δ(CE)((FD)G) 1 CEg(CE)H CHE\begin{aligned} F\otimes (A\otimes B)\otimes G &\xrightarrow{1_F\otimes f\otimes 1_G} F\otimes (C\parr D\parr E)\otimes G\\ &\xrightarrow{\delta} ((F\otimes (C\parr D)) \parr E)\otimes G\\ &\xrightarrow{\delta} ((C\parr (F\otimes D)) \parr E)\otimes G\\ &\xrightarrow{\cong} ((C\parr E) \parr (F\otimes D))\otimes G\\ &\xrightarrow{\delta} (C\parr E) \parr ((F\otimes D)\otimes G)\\ &\xrightarrow{1_{C\parr E}\parr g} (C\parr E) \parr H\\ &\xrightarrow{\cong} C\parr H\parr E \end{aligned}

Conversely, a polycategory that is suitably “representable” yields a linearly distributive category. And the forgetful functor from linearly distributive categories and strong Frobenius linear functors to polycategories has a left adjoint; see (Cockett-Seely 97).

Symmetric monoidal categories

Any symmetric monoidal category becomes a linearly distributive category in which both monoidal structures are the same; all the required structure and coherence conditions follow straight from coherence for symmetric monoidal categories. Note that such examples are almost never star-autonomous.

These examples satisfy the extra property that the distributors δ\delta are isomorphisms. However, not every linearly distributive category in which the distributors are isomorphisms are of this form; the rest are “shifted monoidal categories” in which ABA 1BA \parr B \coloneqq A \otimes \bot^{-1} \otimes B, where \bot is a chosen \otimes-invertible object.

Linear bicategories

Linear bicategories are a horizontal categorification of linearly distributive categories.

Internal structures

Some structures normally defined in a monoidal category can more generally be defined in a linearly distributive category. This includes dual objects (yielding the above “negations”) and also Frobenius algebras; see (Egger2010).

As lax Frobenius algebras

Linearly distributive categories that are both closed and co-closed can be identified with lax Frobenius algebras in the polycategory MVar? of multivariable adjunctions; see this blog post.

History

The concept was originally called a weakly distributive category and was introduced by Robin Cockett and Robert Seely in 1991 at the Durham conference on applications of categories (Cockett-Seely 97). Subsequently, in recognition of their fundamental role in the categorical semantics for the proof theory of linear logic, and the fact that they are not a “weakening” of distributive categories in any standard sense, they were renamed to linearly distributive categories.

A key feature of linearly distributive categories is the existence of morphisms of the form

δ:A(BC)(AB)C \delta \colon A \otimes (B \parr C) \longrightarrow (A \otimes B) \parr C

which exhibit linear distributivity. The importance of this map had previously been overlooked in the linear logic community due to the (continuing) tendency to write sequents in a one-sided manner. However, the importance of the map was gradually being realized: for example Valeria de Paiva and Martin Hyland had independently pointed out the significance of the map.

Linearly distributive categories were introduced to modularize the proof theory of linear logic and to allow a more systematic approach to the then still unsolved coherence problems associated with the units in linear logic. This program of work culminated in a solution which was published in (BCST 1996)

These techniques also solved a classical open problem in closed monoidal categories concerning the behaviour of the triple dual. Todd Trimble, who was completing his PhD. at the time, provided a vital insight to the group on how this problem could be solved and this unlocked the solution to the general problem.

Linearly distributive categories are to polycategories as monoidal categories are to multicategories. Namely, when one represents “the commas” of a polycategory one obtains a linearly distributive category. Crucially, the key coherence issues of (the multiplicative fragment of) linear logic concerning the units is already present at the linearly distributive level – but it is no longer cluttered by the other features of linear logic. Thus, this provided a clean substrate from which to study and isolate this coherence problem.

Contrary to the general direction of work in coherence (and, indeed, in the linear logic community) the solution to the problem (given in (BCST 1996)) involved an expansion reduction rewriting system modulo equations. At that time, the prevailing proof theoretic strategy for solving coherence problems was simply to cut-eliminate: usually this suffices to leave proofs in a normal form. However, this system was notable as this strategy clearly failed: it was necessary to leave some equations in the system. These equations, of course, involved the possible “rewiring”s of the units.

At that time this was generally thought to be a rather unsatisfactory and unnecessarily technical solution especially when compared to the normal forms to which the community was accustomed. However, subsequently, in 2014, Willem Heijltjes and Robin Houston (HH2014) showed that equality of morphism is a PSPACE? complete problem. This essentially implies that there is no practical way round this problem beyond a search of the rewiring equivalence class.

Linearly distributive categories have now been used as the substrate for a number of systems.

References

  • Willem Heijltjes, Robin Houston, No proof nets for MLL with units: proof equivalence in MLL is PSPACE-complete, CSL-LICS ‘14 Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Article No. 50. (web)
  • M.E. Szabo, Polycategories, Comm. Algebra 3 (1975) 663-689. DOI

Frobenius algebras in linearly distributive categories are discussed in

  • Jeff Egger, The Frobenius relations meet linear distributivity, TAC

Revised on November 28, 2017 19:07:10 by Mike Shulman (208.71.27.101)