Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor galois-theory gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics planar pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorMike Shulman
    • CommentTimeMay 11th 2016

    I reorganized linearly distributive category by moving the long block of history down to the bottom, adding an “Idea” section and a description of how **-autonomous categories give rise to linearly distributive ones and linearly distributive ones give rise to polycategories. I also cross-linked the page better with polycategory and star-autonomous category.

    • CommentRowNumber2.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 12th 2016

    Thanks, Mike!

    It should be pointed out that at least some of those coherence conditions are essentially tensorial strength conditions (noting that each of those δ\delta’s, read as strengths, can be read either as \otimes-ing with AA is strong over \wp, or \wp-ing with AA is strong over \otimes).

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeMay 12th 2016

    Feel free to add that to the page… (-:

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeMay 12th 2016

    The notion of linearly distributive category is not very intuitive to me, particularly as regards these constructions. I mean, looking at the definition of star-autonomous category, I don’t “see” a linearly distributive category underneath — heck, the definition doesn’t even include \parr — and looking at the definition of linearly distributive category, I don’t “see” a polycategory underneath. Maybe I just need to practice to improve my vision, but if anyone can provide some extra intuition I wouldn’t mind.

    • CommentRowNumber5.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 12th 2016

    I don’t know that I can help much, Mike. But usually I revert back to *\ast-autonomous categories, knowing that every linearly distributive category (aka “weakly distributive category” back in the day) comes canonically from a *\ast-autonomous category: if CC is linearly distributive then the unit CUFCC \to U F C is an equivalence of linearly distributive categories, where FU:*AutonLinDistF \dashv U: \ast-Auton \to LinDist is the free-forgetful adjunction. (Linear logic is a conservative extension of the (,)(\otimes, \parr)-fragment.)

    From that point of view, the strengths just come from a corresponding strength for *\ast-autonomous categories, e.g., a bc(ac) ba^b \otimes c \to (a \otimes c)^b where a ba^b is alternate shorthand for bab \multimap a. (A fact that is useful: if VV is symmetric monoidal closed, then any unary functor VVV \to V definable in the language of smc categories carries a canonical strength, in fact a unique strength by the coherence for smc categories. This extends to the case where we include contravariant functors VVV \to V along with the covariant ones, although the notion of tensorial strength for contravariant functors might not be as well-known as for covariant ones.)

    As for seeing the polycategory underneath, I guess you know that linearly distributive categories were invented in the first place to explain what polycategories are from the viewpoint of categorical algebra. You yourself wrote the blurb on how you get a polycategory out of a linearly distributive category (so again I don’t know I can help much further), but again, my tendency is to think directly in terms of linear logic and *\ast-autonomous categories, where we know how to interpret two-sided sequents A 1,,A mB 1,,B nA_1, \ldots, A_m \to B_1, \ldots, B_n. Thus, if you can see an underlying polycategory in a *\ast-autonomous category (or if you know how to build a *\ast-autonomous freely out of two-sided sequents), then you can in a linearly distributive category (more directly in fact, since we cut out the linear ¬\neg middleman).

    By the way, I wouldn’t say that polycategories are a “natural categorical semantics” for linearly distributive categories [1] – if I’d say anything along these lines, I’d say that’s backwards: it’s more that linearly distributive categories provide categorical semantics for polycategories! But even that is not how I’d put it. Normally one refers to categorical semantics of various fragments of (e.g. propositional) logic, so I’d really rather say that linearly distributive categories provide a semantics for the multiplicative conjunction and disjunction fragment of (linear) logic. Polycategories are actually slightly alien from the viewpoint of category theory, since we cut at only one formula at a time, but linearly distributive categories is how a category theorist might make sense of them.

    [1] In fact I think it’s just wrong to say polycategories are a semantics for ld categories or for the (,)(\otimes, \parr)-fragment, since general polycategories don’t interpret formulas AB,ABA \otimes B, A \parr B.

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeMay 12th 2016

    Did I say that polycategories are a categorical semantics for linearly distributive categories? I agree that that makes no sense — categorical structures are categorical semantics for logic, not for each other. If that’s on one of the pages it should be fixed.

    Richard Garner’s approach to polycategories (cited on the page now) describes them with a “multi-object cut” in terms of a pseudo-distributive law. In fact I think there is a theory of “generalized polycategories” analogous to “generalized multicategories” but as far as I know no one has written it down yet.

    Regarding intuition, to be honest I still struggle with all three of these structures on their own, even before thinking about how they relate to each other. The cut rule for linear logic is still strange to me, possibly coming down to the meaning of \parr again — how can you have a “disjunction” where you don’t know which of the disjuncts is true, but nevertheless you somehow have to “use up the resources” involved in all of them? Possibly what I need to do is spend more time with concrete examples like Chu constructions.

    • CommentRowNumber7.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 12th 2016

    No, you didn’t say that. But it’s on the polycategory page (sorry not to have specified that earlier).

    Now that you mention Richard Garner, I vaguely remember that Robin Houston also had a neat way of thinking about polycategories or *\ast-autonomous categories, which I’ll try to recall when I have some time.

    There are some good examples of linearly distributive categories on the star-autonomous category page, so that might be worth a look. However, another source of intuition though is proof nets. Is that something you’ve played with? The validity criterion for proof nets relies crucially on the structure of \parr-connectives (meaning instances of \parr when looking at positive formulas, i.e., formulas of Δ\Delta on the right of a sequent ΓΔ\Gamma \to \Delta, or instances of \otimes when looking at negative formulas, i.e., formulas of Γ\Gamma).

    I should really spend some time writing some of this up at the nLab, because it’s closely connected with my PhD thesis. In the meantime, you might also benefit from reading Girard’s original article Linear Logic and especially where he gets into proof nets and his “cyclic trips” and his longtrip criterion, which is the kind of thing I’m alluding to in the previous paragraph. A more streamlined approach to proof nets was later given by Danos and Regnier.

    But in a nutshell, to decide whether a proof structure on a sequent Γ \to \Gamma is a proof net (is derivable in the theory of say *\ast-autonomous categories or linearly distributive categories), the criterion is basically that for all the 2 n2^n ways of setting switches at the nn \parr-connectives occurring in subformulas of Γ\Gamma, the result is an acyclic connected graph – a tree. (For the moment I’m considering only those Γ\Gamma in which monoidal units do not appear – how to handle units requires an extension which was a major part of my thesis.)

    Bah – I’m doing a terrible job trying to discuss this here. So much to say. I’d better spend some time in the Lab and organize my thoughts there, and when I come back up for some air, maybe we can discuss this further.

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeMay 12th 2016

    I don’t see it on the polycategory page either; what I see under “Internal logic” is “Polycategories provide a natural categorical semantics for linear logic.”

    I’ve looked at proof nets a little, a while ago, but I don’t think they really help; it seems to me just a way of reformulating the confusing thing that doesn’t make it any less confusing.

    • CommentRowNumber9.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 12th 2016

    Oops. So it does. My bad (although I still think that sentence needs to be brushed up a little).

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeMay 12th 2016

    Feel free to brush it up. (-: If what you’re worried about is that polycategories don’t have connectives, then maybe “…for the judgmental structure of classical linear logic”?

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeMay 13th 2016

    Is it true that any symmetric monoidal category is linearly distributive (but not, of course, *\ast-autonomous) if we define =\parr = \otimes?

    • CommentRowNumber12.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 13th 2016

    Yes, all the required structure and coherence conditions follow straight from coherence for symmetric monoidal categories.

    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeMay 13th 2016

    Great. I added that to the page. Two related questions:

    1. Do you know whether anyone has written down a type theory for “symmetric monoidal categories regarded as linearly distributive”? I’m imagining a sequent calculus with multiple formulas in both antecedent and consequent, and where you’re allowed to cut on multiple formulas at once.

    2. What is the free *\ast-autonomous category on a symmetric monoidal category regarded as linearly distributive? Does it have a nice description?

    • CommentRowNumber14.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 14th 2016

    I don’t know an answer to 1 off hand. But the lack of such might be related to an observation below.

    The free *\ast-autonomous category in this case would coincide with the free compact closed category. From a sequent calculus perspective, this is (I think) a weird case because IIRC there’s no good cut-elimination procedure. (Notice that string-theoretically, composition can produce loops or islands, which in the case of free compact closed categories on a category CC, must be accounted for by taking the trace of a category CC. Meanwhile loops don’t occur in a cut-free fragment, unless perhaps they are put in by hand as axioms, for each CC.)

    I am not aware of any really clean way of describing the free compact closed category on a symmetric monoidal category. The free compact closed category F(C)F(C) on a category CC has I think a halfway decent description in terms of a kind of wreath product F(1)CF(1) \wr C where edges of graphs in F(1)F(1) are labeled by morphisms in CC (and loops by elements of tr(C)tr(C)). If S(C)S(C) is the free symmetric monoidal category on CC, then I guess the relatively free compact closed category on a symmetric monoidal category CC can be formed as a suitable kind of 2-colimit (a co-isoinserter? not sure) of a diagram of type

    FSCFCF S C \rightrightarrows F C

    which could be further described by applying rewrite rules on morphisms of FCF C, but I’m not sure such rewrite rules can be organized nicely.

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeMay 14th 2016

    Interesting; that will take some thought. Can you give any intuition for why the free *\ast-autonomous category on a symmetric monoidal category qua linearly distributive category would coincide with the free compact closed category?

    • CommentRowNumber16.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 14th 2016
    • (edited May 14th 2016)

    The free *\ast-autonomous category on a linearly distributive category is formed by adjoining (in the doctrine of linearly distributive categories) objects ¬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)

    and where we have =,=\parr = \otimes, \bot = \top, this is exactly how one would form the free compact closed category generated by the symmetric monoidal category CC.

    This construction is mentioned both in the original Cockett-Seely paper (page 159 ff) and in Blute-Cockett-Seely-Trimble.

    By the way, that Cockett-Seely paper also handily spells out the definition of polycategories (which is due to Manfred Szabo); someone should just copy that over to the nLab (and that someone could be me).

    • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeMay 14th 2016

    Ah, I see! Somehow that makes *\ast-autonomous categories and linearly distributive categories make some more sense to me: a *\ast-autonomous category is one which is almost compact closed, but where the unit and counit of the “dualities” use different monoidal structures; and a linearly distributive category is one with two monoidal structures that interact in exactly the way that’s necessary for this to make sense.

    Does it ever happen nontrivially (i.e. apart from the case where the two monoidal structures coincide) that the distributors in a linearly distributive category are isomorphisms?

    • CommentRowNumber18.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 14th 2016

    Yes, exactly.

    I’m pretty sure that if those constraints are isomorphisms, then the monoidal structures coincide. I should work this out more explicitly to satisfy myself, but this should be related to Brian Day’s result that when one localizes the free symmetric monoidal closed category on a symmetric monoidal category with respect to the strength constraints (AB)CA(BC)(A \multimap B) \otimes C \to A \multimap (B \otimes C) (i.e., forcing them to be isomorphisms), then you get the free compact closed category on the symmetric monoidal category. That strength constraint corresponds to the linear distributivity.

    • CommentRowNumber19.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 15th 2016

    Ah, I take it back: Cockett-Seely, 5.3 and 5.4, specify that linearly distributive categories where the distributivities are isomorphisms are the same as “shifted” (symmetric) monoidal categories. If I’m not mistaken, supervector spaces provides an instructive example of this.

    • CommentRowNumber20.
    • CommentAuthorMike Shulman
    • CommentTimeMay 15th 2016

    Nice. I should have read that paper more carefully.

    One other reason the notion of linearly distributive category is difficult for me is that it isn’t usually “packaged” in a categorically nice way, making it seem somewhat ad hoc. For instance, the notion of duoidal category seems a little weird when written out explicitly, but it makes more sense when you say that it’s just a pseudomonoid in the 2-category of monoidal categories and lax monoidal functors. The observation about tensorial strength is partway to the sort of thing I would like to say, but it doesn’t describe the structure completely.

    Here’s a first attempt. If CC is any monoidal category, then there is a 2-category of (pseudo) CC-modules (which I guess some people call “actegories”) and lax CC-module morphisms. As noted at the page tensorial strength, we can regard CC as a CC-module, and in this case the lax CC-module maps CCC\to C are precisely the tensorially-strong endofunctors. Now in fact, at least if CC is symmetric, then the 2-category of CC-modules should be a 2-multicategory, where the multimorphisms are “lax in each variable separately”. One might then hope that a symmetric linearly distributive category is precisely a symmetric monoidal category (C,)(C,\otimes) together with the structure \parr of a symmetric pseudomonoid in this 2-multicategory on CC regarded as a CC-module. However, this doesn’t seem quite right; I can’t see how to get out of it the “distribution and distribution” axiom in Cockett-Seely. Does it follow somehow? Or can one modify this definition so as to be able to get it out?

    • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeMay 15th 2016

    I added some more remarks to linearly distributive category and star-autonomous category based on this discussion.

    • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeMay 15th 2016

    Thanks for taking the time to help me understand all this, by the way.

    • CommentRowNumber23.
    • CommentAuthorMike Shulman
    • CommentTimeMay 18th 2016

    One reason ordinary dual objects are interesting is that they allow us to define traces. With the “unit” and “counit” defined using different monoidal structures in a *\ast-autonomous category, we can’t define a trace in the usual way. But this problem is somewhat reminiscent to me of what happens with bicategorical traces, so I wonder whether it has a similar solution. If we equip a *\ast-autonomous category CC with a functor sh:CDsh:C\to D and isomorphisms sh(AB)sh(AB)sh(A\otimes B) \cong sh(A\parr B), then we could define the trace of any endomorphism f:AAf:A\to A to be the composite

    sh()sh(AA *)fsh(AA *)sh(A *A)sh(A *A)sh() sh(\top) \to sh(A\parr A^*) \xrightarrow{f} sh(A\parr A^*) \cong sh(A^* \parr A) \cong sh(A^* \otimes A) \to sh(\bot)

    I wonder whether there are any interesting examples of this?

    • CommentRowNumber24.
    • CommentAuthorMike Shulman
    • CommentTimeOct 20th 2017

    I added a sketch definition of the 2-category of linearly distributive categories, and a remark that the forgetful functor from *\ast-autonomous ones to linearly distributive ones also has a right adjoint. I also uniformized the notation on the page to (,)(\otimes,\top) and (,)(\parr,\bot) for the monoidal structures; I hope no one objects to that.

    • CommentRowNumber25.
    • CommentAuthorMike Shulman
    • CommentTimeOct 20th 2017

    Actually, I now realized that there are actually three different notions of functor between linearly distributive category that appear in the literature: the Cockett-Seely “linear functors”, the linear functors whose \otimes-part and \parr-part agree as functors (which I’m tempted to call “Frobenius linear functors”), and the ones that moreover are strong monoidal for both structures. The “*\ast-autonomous nucleus” of a linearly distributive category uses “linear functors”, whereas the free linearly distributive category on a polycategory uses strong Frobenius linear functors. Which notion of functor is the free *\ast-autonomous category on a linearly distributive category (#16 above) free with respect to? I’m guessing also the strong Frobenius ones?

    • CommentRowNumber26.
    • CommentAuthorvaleriadepaiva
    • CommentTimeJul 30th 2021

    I’ve added a small historical correction.

    diff, v20, current

  1. Added more historical notes. Added and tidied up references.

    Rongmin Lu

    diff, v21, current

    • CommentRowNumber28.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 2nd 2021

    Dating back to revision 8 (Mike Shulman): “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.”

    Not that I’m doubting this, but it’s the first time I’m learning about it. Any citations?

    • CommentRowNumber29.
    • CommentAuthorMike Shulman
    • CommentTimeAug 3rd 2021

    Looks to me like that phrase was added in revision 5 by Urs.

    • CommentRowNumber30.
    • CommentAuthorUrs
    • CommentTimeAug 3rd 2021

    I don’t remember writing this, nor do I know half of what it’s saying. If it was me who entered this into the entry, it must have been in helping somebody else get their comment into the nnLab. This must have been written by somebody with inside knowledge of the linear logic community – not me. Maybe this was a contribution to another forum or blog, and was thought to deserve to be archived on the nnLab. Feel free to edit as need be.

    • CommentRowNumber31.
    • CommentAuthorRichard Williamson
    • CommentTimeAug 3rd 2021
    • (edited Aug 3rd 2021)

    My guess is that Revision 5 was the outcome of the merger Urs made described at the following link.

    If so, I’d guess that Robin Cockett is the author.

    • CommentRowNumber32.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 4th 2021

    Okay, thanks – all that makes sense. Robin would be in a position to know I think.

    • CommentRowNumber33.
    • CommentAuthorGuest
    • CommentTimeOct 22nd 2022
    I have a (perhaps naïve) question regarding *-autonomy and linear distributivity. On the page, it says that *-autonomous categories are the same as linear distributive categories with negation, with a citation to "Weakly Distributive Categories". However, while it's clear to me how one would obtain a linear distributive structure (going much along the lines of the outlined example in the paper), I fail to see how we can obtain the right kind of negation; more specifically, why the "snake identities" (or rather, analogues for linear distributive categories, as they appear in the paper) hold.

    Assume the category C is *-autonomous. We can define ⊥ = 1* and a ⊕ b = (a* ⊗ b*)* for all a, b ∈ C. Further, by assumption there is an isomorphism

    C(a ⊗ b, c*) ≅ C(a, (b ⊗ c)*), for all a, b, c ∈ C.

    I think I got the definition of the (co)evaluation morphisms themselves. For example, for x ∈ C we can set a = x*, b = x, and c = 1 = ⊥* to obtain C(x* ⊗ x, ⊥) ≅ C(x*, x*) and so we can define the evaluation of x as the retract of the identity. However, I don't understand why this implies that the snake identities follow. The coherence relations for linearly distributive categories with negation are framed in terms of the δ^{R,L}_{R,L}'s, which say that the tensor products are strong with respect to each other. Is the idea that, starting from a *-autonomous category, we can define these morphisms in such a way so that this follows automatically? Is this perhaps written down somewhere?

    As a corollary: on the star-autonomous category page it says that they are rigid when there is a natural isomorphism from (a ⊗ b)* to a* ⊗ b*. However, if the above is true, isn't it the case that we rather require the dualising functor to be a certain kind of monoidal functor (i.e., the isomorphism from (a ⊗ b)* to a* ⊗ b* has to be a particular one)? Otherwise, on objects we would have that a ⊗ b ≅ a ⊕ b, but since the associators would be different (I guess?), the "regular" snake identities that we required for rigidity still wouldn't follow.

    Am I missing something?

    Tony Zorman (TU Dresden)