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

Discussion Tag Cloud

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).

nLab > Latest Changes: closed category

Bottom of Page

1 to 55 of 55

  1.  
    • CommentRowNumber1.
    • CommentAuthorTobias Fritz
    • CommentTimeDec 27th 2012

    A query box has been added:

    I suspect there is a variant of the definition involving a transformation R XY Z:[X,Y]→[[Y,Z],[X,Z]]R^Z_{X Y} \colon [X,Y] \to [[Y,Z],[X,Z]] rather than LL. Is this correct? If so, how do these two definitions relate? Can one of them be expressed in terms of the other? Or is there a refined definition which comprises both LL and RR?

    • CommentRowNumber2.
    • CommentAuthoradeelkh
    • CommentTimeDec 27th 2012
    • CommentRowNumber3.
    • CommentAuthorTodd_Trimble
    • CommentTimeDec 28th 2012

    Tobias, you’re right that there’s a variant of this type, just as there is a variant of closed monoidal category where it is the functors b⊗−b \otimes - that have right adjoints, not −⊗b- \otimes b. (In fact, the underlying closed categories of such closed monoidal categories give instances of the phenomenon you’re asking about). As remarked at closed monoidal category, sometimes people use the terminology “left closed”, “right closed” to tell these things apart.

    And just as we can manufacture a right closed monoidal structure from a left closed monoidal structure (by defining a new monoidal product obtained by switching the order of tensor factors), so we can manufacture right closed structures from left closed structures. One way of doing this might be to use the fact that any (left) closed functor can be embedded fully and “closedly” into a (left) closed monoidal category, switch the tensor factors, and then take the underlying (right) closed category of the right closed monoidal category that results. Off the top of my head, I couldn’t think of a way to do this more directly, but there may be a way.

    Of course, a left closed symmetric monoidal category is also right closed. But there are also examples of left closed (monoidal) categories that aren’t right closed. An example that comes to my mind is the category of Schur functors with the plethystic monoidal product.

    • CommentRowNumber4.
    • CommentAuthorTobias Fritz
    • CommentTimeDec 29th 2012
    Thanks, Todd, much appreciated!

  5. I expanded a bit in the section on “Embedding into closed monoidal categories”, with what I understand about the way LaPlaza’s embedding works, as well as an alternative embedding originally defined by Day.

  6. While the definition of closed categories with L YZ XL^X_{YZ} matches the definition of monoidal (left) closed categories, the one with R XY ZR^Z_{XY} does not seem to.

    Let’s denote the right adjoints of X⊗−X\otimes - and −⊗X-\otimes X by −⇐X-\Leftarrow X and X⇒−X\Rightarrow -, respectively. On the one hand, the transformation L YZ X:Z⇐Y→(Z⇐X)⇐(Y⇐X)L^X_{YZ}\colon Z\Leftarrow Y\to(Z\Leftarrow X)\Leftarrow(Y\Leftarrow X) corresponds to X⊗((Y⇐X)⊗(Z⇐Y))≅(X⊗(Y⇐X))⊗(Z⇐Y)→Y⊗(Z⇐Y)→ZX\otimes((Y\Leftarrow X)\otimes(Z\Leftarrow Y)) \cong (X\otimes(Y\Leftarrow X))\otimes(Z\Leftarrow Y) \to Y\otimes(Z\Leftarrow Y) \to Z. Similarly we have R′ YZ X:Y⇒Z→(X⇒Y)⇒(X⇒Z)R'^X_{YZ}\colon Y\Rightarrow Z\to(X\Rightarrow Y)\Rightarrow(X\Rightarrow Z). On the other hand, we only have R XY Z:X⇒Y→(X⇒Z)⇐(Y⇒Z)R^Z_{XY}\colon X\Rightarrow Y\to(X\Rightarrow Z)\Leftarrow(Y\Rightarrow Z). Note that in R XY ZR^Z_{XY} two closed structures ⇐,⇒\Leftarrow, \Rightarrow are mixed. In a symmetric monoidal closed category, I suppose R XY ZR^Z_{XY} works fine.

    • CommentRowNumber7.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 24th 2016

    That’s a fair point, Toshiki; thanks! There’s no explicit mention of the right-hand structure in the article; maybe you could add it? (Or I can, sometime later.) The query box could then be removed.

    • CommentRowNumber8.
    • CommentAuthorYemon Choi
    • CommentTimeDec 19th 2017

    Have just fixed the link that Tobias created so it now points to this thread.

    If anyone is still reading: can they clarify where R XY ZR^Z_{XY} “works” as a way to define closed categories? I ask because I was playing around with the category of dual Banach spaces (the morphisms are adjoints-in-the-TVS-sense of maps between the preduals, so maybe my category is isomorphic to BSp opBSp^{op}) and trying to get a closed structure. At the time I couldn’t remember whether L XY ZL^Z_{XY} or R XY ZR^Z_{XY} was the method used in the nLab page, so I tried both, but it seems that my method fails to give suitable R XY ZR^Z_{XY} while it might give a suitable L XY ZL^Z_{XY}…

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeDec 19th 2017

    Suppose we have a biclosed monoidal category

    C(X⊗Y,Z)≅C(Y,X⊳Z)≅C(X,Z⊲Y). C(X\otimes Y,Z) \cong C(Y,X\rhd Z) \cong C(X,Z\lhd Y).

    Then adjoint transposes give us evaluation maps

    (X⊳Y)→(X⊳Y)X⊗(X⊳Y)→Y(Y⊲X)→(Y⊲X)(Y⊲X)⊗X→Y \frac{(X\rhd Y) \to (X\rhd Y)}{X\otimes (X\rhd Y) \to Y}\qquad \frac{(Y\lhd X) \to (Y\lhd X)}{(Y\lhd X) \otimes X \to Y}

    which we can put together to get double composition maps

    X⊗(X⊳Y)⊗(Y⊳Z)→Y⊗(Y⊳Z)→Z X\otimes (X\rhd Y) \otimes (Y\rhd Z) \to Y \otimes (Y\rhd Z) \to Z (Z⊲Y)⊗(Y⊲X)⊗X→(Z⊲Y)⊗Y→Z. (Z\lhd Y) \otimes (Y\lhd X) \otimes X \to (Z\lhd Y) \otimes Y \to Z.

    Now applying adjoint transposes again to the first one, we get

    X⊗(X⊳Y)⊗(Y⊳Z)→Z (X⊳Y)⊗(Y⊳Z)→(X⊳Z) (Y⊳Z)→((X⊳Y)⊳(X⊳Z)) \array{\arrayopts{\rowlines{solid}} X\otimes (X\rhd Y) \otimes (Y\rhd Z) \to Z\\ (X\rhd Y) \otimes (Y\rhd Z) \to (X\rhd Z)\\ (Y\rhd Z)\to ((X\rhd Y) \rhd (X\rhd Z)) }

    and to the second one we get

    (Z⊲Y)⊗(Y⊲X)⊗X→Z (Z⊲Y)⊗(Y⊲X)→(Z⊲X) (Z⊲Y)→((Z⊲X)⊲(Y⊲X)) \array{\arrayopts{\rowlines{solid}} (Z\lhd Y) \otimes (Y\lhd X) \otimes X\to Z\\ (Z\lhd Y) \otimes (Y\lhd X) \to (Z\lhd X)\\ (Z\lhd Y) \to ((Z\lhd X) \lhd (Y\lhd X)) }

    If we write X⊳YX\rhd Y as [X,Y][X,Y], then the first one gives L YZ XL^X_{Y Z}. But if we instead write Y⊲XY\lhd X as [X,Y][X,Y], then the second one gives… also L YZ XL^X_{Y Z}! In other words, if you forget the presence of a monoidal structure, there is no difference between left closed and right closed.

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeMar 26th 2018

    I added to closed category a statement of the result about how a closed category becomes a monoidal category, including a warning about how it requires a stronger hypothesis than the monoidal-to-closed case.

    (This came up recently in a discussion of how to prove in HoTT that the smash product is a 1-coherent monoidal structure.)

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeMay 28th 2018

    Expanded the equivalence of this definition with Eilenberg-Kelly’s a bit, and mention Street’s bicategorical version.

    diff, v47, current

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeMay 29th 2018

    Some thoughts about a non-unital notion of closed category.

    diff, v49, current

    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeMay 29th 2018

    Mention the symmetric and cartesian cases briefly

    diff, v49, current

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeMay 29th 2018

    Clarified the promonoidal version of the embedding theorem

    diff, v51, current

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeMay 29th 2018

    add citations for the symmetric case

    diff, v51, current

  16. Hi Mike,

    Thanks for all the additions and clarifications!

    Re #12: yes, that is a good question about finding a notion of “non-unital closed category” equivalent to closed multicategories without unit, and the idea of asking for “left evaluation” operations seems natural. (By the way, it looks like there is a typo in the type of ev: that should be a “\to” rather than “\cdot”, right?) But I want to mention that there is also a natural notion of “non-unital closed category” where you simply drop the ii’s and jj’s: Bourke calls these “semi-closed” categories in this paper, and they are closely related to “skew semi-monoidal” categories (= categories equipped with a ⊗\otimes which is only associative up to natural transformation, and which satisfies the pentagon axiom). Semi-closed categories are equivalent to closed “non-unitary”/“constantless” multicategories, i.e., closed multicategories with no multimaps of arity 0. To construct such a multicategory from a semi-closed category CC, you define the multimaps of positive arity by C(X 0,X 1,…X n;Z)=C(X 0,[X 1,…,[X n,Z]])C(X_0,X_1,\dots X_n; Z) = C(X_0, [X_1,\dots,[X_n,Z]]), without need for a unit.

  17. fixed definition of multimaps from maps in a closed category, which relies on the unit.

    diff, v53, current

    • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeMay 30th 2018

    Thanks for the comments Noam; I’ll have a look at Bourke’s paper. Since you’re interested, let me say a bit more about what’s going on in my head, in case you have anything to contribute to it.

    My current suspicion is that my proposed kind of non-unital closed categories (which I am tempted to claim should really be the ones called simply “closed categories”; I don’t know why having a unit should be the default) can be defined as biased-lax monoids in ProfProf whose binary multiplication profunctor is corepresentable in the first variable and satisfying one or two “normality” conditions. The “underlying-set” functor is then the unit profunctor 1⇸A1 ⇸ A, and the left evaluation is one of the biased-lax unit transformations (the other one, which I think must be required to be an isomorphism as one of the normality conditions, is the isomorphism U([X,Y])≅C(X,Y)U([X,Y]) \cong C(X,Y)). Since multicategories can be defined as normal unbiased-lax monoids in ProfProf, if this were true, then a positive answer to that MO question would almost automatically provide an abstract proof that non-unital closed categories are equivalent to closed multicategories. And by identifying monoidal categories (pseudo-monoids in CatCat) with representable pseudo-monoids in ProfProf, it would also give an abstract viewpoint on the closed category / monoidal category correspondence.

    Your comment about the semi-monoidal/constantless case also fits into this picture quite naturally: if we omit the underlying-set functor (and hence also the left evaluation), we would naturally get a “biased-lax semi-monoid” in ProfProf, which would of course be closely related to biased-lax semi-monoids in CatCat (skew semi-monoidal categories) and to unbiased-lax semi-monoids (constantless multicategories).

    • CommentRowNumber19.
    • CommentAuthorNoam_Zeilberger
    • CommentTimeMay 30th 2018
    • (edited May 30th 2018)

    First, have you seen Street’s recent-ish paper on skew-closed categories? A skew-closed category is almost a closed category, but where i:[I,X]→Xi : [I,X] \to X goes in the opposite direction and does not have to be invertible, and where the map γ:C(X,Y)→C(I,[X,Y])\gamma : C(X,Y) \to C(I,[X,Y]) also does not have to be invertible (these two invertibility conditions are called “right normality” and “left normality”, so a closed category is a skew-closed category which is both left and right normal). In any case, Street gives a similar description of skew-closed/skew-monoidal categories as “skew-promonoidal” categories + representability conditions: see Proposition 22 on p.22.

    Second, for your MO question, although they deal with skew units (I⊗A→A→A⊗II \otimes A \to A \to A \otimes I) rather than lax ones, you might be interested in Bourke and Lack’s recent paper on skew monoidal categories and skew multicategories. A skew multicategory is a certain kind of generalized multicategory, with two classes of multimaps called “loose maps” and “tight maps”, and with the latter embedding into the former. Bourke and Lack exhibit a correspondence between skew monoidal categories and left representable skew multicategories, where “left” representability basically means that the universal property of the multimaps A 1,…,A n→A 1⊗…⊗A nA_1,\dots,A_n \to A_1 \otimes \dots\otimes A_n only holds with respect to partial composition on the left. (I actually think this is a really natural idea, and wrote a paper recently that started to explore some closely related ideas from the perspective of proof theory.)

    • CommentRowNumber20.
    • CommentAuthorMike Shulman
    • CommentTimeMay 30th 2018

    Thanks very much for those references! I will certainly take a look.

  21. Indeed, I think that what you are proposing is very close to Street’s profunctorial definition of skew closed category - unit representability + left normality. The idea of retaining the unit profunctor while dropping its representability makes a lot of sense to me from the point-of-view of lambda calculus (where U:C→SetU : C \to Set is the presheaf of closed terms of a given type), which I imagine is also part of your motivation.

    In case you’re interested, I’ve also been trying to better understand aspects of the connection between linear lambda calculus and BCI combinatory logic, and wrote a bit about it in some musings that perhaps will make sense to you, see in particular Section 4 and the “topological completeness” result (Theorem 4.5) which is a variation of the BCI completeness theorem. The formulation given in the paper is pretty idiosyncratic, but the idea I originally had in mind is that the “imploid moves” on p.14 can be interpreted as natural transformations (going in the opposite direction) between profunctors constructed using the structure of a (symmetric, left normal skew) closed category. Now that you’ve mentioned non-unital closed categories, I think it makes even more sense to formulate things in that way, because in fact one doesn’t need (the moves corresponding to) representability of the unit to prove the theorem.

    • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeMay 31st 2018

    Thanks, I’ll have a look at your note too. What I have in mind, once a non-unital closed category is settled, is to reformulate it without assuming from the outset that we have a category at all. That is, since C(X,Y)=U([X,Y])C(X,Y) = U([X,Y]), the homsets of CC are redundant data: all we need are the objects of CC, the binary operation [−,−][-,-] on them, the operation UU from objects to sets, and additional structure and axioms. I made a start on this here using unital closed categories, but it got kind of messy and I realized I actually wanted the non-unital version. My expectations, once this is worked out and fully simplified, are that:

    1. One of these things where UU is valued in subsingletons will be precisely a (“semantic”) Hilbert system for the appropriate logic.

    2. Given one of these things, the set ∐ XU(X)\coprod_X U(X) inherits an “application” partial binary operation. What properties of such an operation on a set are necessary in order to reconstruct a closed category in a “universal” way? I expect there is a way to make this precise in such a way that the answer is precisely a PCA of the appropriate sort (BCI, BCK, SKI, etc.), with the resulting closed category being its category of PERs. This would provide a nice “explanation” of realizability from a purely categorical point of view, even for a category theorist who starts out not caring at all about computability.

    I did seem to be hitting a snag in the non-symmetric case. Do you know if there is a workable notion of Hilbert system or combinatory logic structure for ordered logic? Does it require the “biclosed” situation where there are two hom-objects? (If so, I could perhaps not bother about the skew case — apart from the aesthetic desire to see everything fit together well — since as noted in the Day-Laplaza paper, in the biclosed case (hence also the symmetric case) we do get an honest promonoidal category rather than a lax one.)

  23. What I have in mind, once a non-unital closed category is settled, is to reformulate it without assuming from the outset that we have a category at all.

    That sounds good!

    I did seem to be hitting a snag in the non-symmetric case. Do you know if there is a workable notion of Hilbert system or combinatory logic structure for ordered logic?

    The naive answer is to just drop the C combinator (thus “BI logic”, no pun intended), but are you referring to the fact that the functoriality rule for [−,−][-,-] is not of the kind usually admitted in Hilbert systems/combinatory logic (since it is actually an infinite collection of axioms), and it is not clear how to otherwise derive it in the non-symmetric case? That is indeed an issue, and a year ago I ran into an old paper by Zielonka where he proved that there is no finite axiomatization of “unidirectional product-free lambek calculus with the empty string” (= free non-symmetric closed multicategories) where the only rule of inference is the cut rule.

    However, I believe that this issue is resolved if you consider your combinator basis as generating terms also under η\eta-expansion, and not just under β\beta-reduction. (In the profunctor interpretation, β\beta-reduction and η\eta-expansion correspond to the unit/counit of the adjunction induced by representability of [−,−][-,-].) Though it is not expressed exactly as a Hilbert system/combinatory logic, the version of the completeness theorem proved in my paper does restrict to the planar/non-symmetric case, and relies on η\eta-expansion.

    • CommentRowNumber24.
    • CommentAuthorNoam_Zeilberger
    • CommentTimeMay 31st 2018
    • (edited May 31st 2018)

    However, I believe that this issue is resolved if you consider your combinator basis as generating terms also under η\eta-expansion, and not just under β\beta-reduction.

    But I am not sure whether this statement really makes sense in terms of combinatory logic. The more straightforward answer is that you do have to admit the functoriality principle as an additional rule in your Hilbert system. At some point Jason Reed showed me such a combinatory logic for (the even more restricted case of) ordered, constantless lambda calculus (corresponding to semi-closed categories, and “unidirectional product-free lambek calculus without the empty string”). In this system “combinators” are terms x.Mx.M with a single free variable, and there is a primitive rule taking a pair of combinators x:A 2⊢M:A 1x : A_2 \vdash M : A_1 and y:B 1⊢N:B 2y : B_1 \vdash N : B_2 and returning a new combinator y:A 1→B 1⊢λx.N[yM/y]:A 2→B 2y : A_1 \to B_1 \vdash \lambda x.N[y M/y] : A_2 \to B_2.

    • CommentRowNumber25.
    • CommentAuthorMike Shulman
    • CommentTimeMay 31st 2018

    are you referring to the fact that

    I think so, but maybe you could make me more confident by explicitly stating the rule schema you’re talking about?

    • CommentRowNumber26.
    • CommentAuthorNoam_Zeilberger
    • CommentTimeMay 31st 2018
    • (edited May 31st 2018)

    I think so, but maybe you could make me more confident by explicitly stating the rule schema you’re talking about?

    A 2≤A 1B 1≤B 2A 1→B 1≤A 2→B 2\frac{A_2 \le A_1 \quad B_1 \le B_2}{A_1 \to B_1 \le A_2 \to B_2}

    (Corresponding to the third bullet point after “Add the following structure” in your notes.)

    • CommentRowNumber27.
    • CommentAuthorMike Shulman
    • CommentTimeMay 31st 2018

    What does ≤\le mean in a Hilbert system? Or is that your point in #24 that it doesn’t mean anything?

    • CommentRowNumber28.
    • CommentAuthorMike Shulman
    • CommentTimeMay 31st 2018

    I think of a Hilbert system as a deductive system whose judgments are simply PtrueP\;true (usually written just “PP”) for some proposition PP, with no hypotheticals, and in which most properties of the system are expressed by axioms and often the rule that has premises is modus ponens A→BAB\frac{A \to B \quad A}{B}. But some Hilbert systems have other rules, and it seems like this one could be formulated as A 2→A 1B 1→B 2(A 1→B 1)→(A 2→B 2)\frac{A_2\to A_1 \quad B_1 \to B_2}{(A_1\to B_1)\to (A_2\to B_2)}. Is that right?

  29. What does ≤\le mean in a Hilbert system? Or is that your point in #24 that it doesn’t mean anything?

    Well, I guess my point is more that assuming one admits such binary judgments then functoriality is naturally formulated this way, but it is still a rule schema that would be required in addition to modus ponens.

    I think of a Hilbert system as a deductive system whose judgments are simply PtrueP\;true (usually written just “PP”) for some proposition PP, with no hypotheticals, and in which most properties of the system are expressed by axioms and often the rule that has premises is modus ponens A→BAB\frac{A \to B \quad A}{B}.

    Yeah, I’m okay with that terminology.

    But some Hilbert systems have other rules, and it seems like this one could be formulated as A 2→A 1B 1→B 2(A 1→B 1)→(A 2→B 2)\frac{A_2\to A_1 \quad B_1 \to B_2}{(A_1\to B_1)\to (A_2\to B_2)}. Is that right?

    Right. What I understood from Zielonka’s paper is that he proves that having such a rule schema is in a sense unavoidable. But let me look again at his paper and try to be a bit more careful. Looks. Right…

    First of all, he is talking about the (non-)existence of a “finite axiomatization where the only rule of inference is the cut rule”. This is not exactly a “Hilbert system” in your sense, but pretty close, what we would probably understand as a freely generated multicategory. He starts by setting up an infinite hierarchy of axioms, including all sequents of the form

    x/y,y→xx/y, y \to x

    as axioms of rank 0 (so he is interpreting x/yx/y as right division), then all sequents

    →x/x\to x/x →((x/z)/(y/z))/(x/y))\to ((x/z)/(y/z))/(x/y))

    as axioms of rank 1, and finally a sequent of the form

    →x/(x/y)\to x/(x/y)

    of rank n+1n+1 whenever →y\to y is an axiom of rank nn. Call CC the system with all such axioms (closed under the cut rule), and C nC_n the system with axioms restricted to rank ≤n\le n. What Zielonka shows is that CC is logically equivalent to (the //-fragment of) Lambek’s sequent calculus LL, but there are sequents which are derivable in C n+1C_{n+1} which are not derivable in C nC_n. Therefore LL is not finitely axiomatizable.

    Okay, so that is starting to ring some bells, and I see that it’s more interesting than I suggested above. Rather than a direct transcription of functoriality, the engine of his axiom hierarchy can be written as the following rule (shifting notation a bit)

    ⊢A⊢(A→B)→B \frac{\vdash A} {\vdash (A \to B) \to B}

    which is actually quite similar to your “evaluation” operation! (In my paper there is also an idea which I think is related of a “dni-closed” deductively closed subset [of an “imploid” = thin skew closed category], which serves as an analogue of a normal subgroup. The idea is that closure under double-negation introduction can be seen as a commutation condition necessary for the construction of quotients, and which is satisfied in particular for the subset of elements above the unit.)

    • CommentRowNumber30.
    • CommentAuthorMike Shulman
    • CommentTimeMay 31st 2018

    Following the link from Bourke-Lack to their companion paper, I see that my MO question is answered there in the case of skew-monoidal categories. The biased-lax case where both unit morphisms go in the same direction ought to be basically the same but simpler.

    • CommentRowNumber31.
    • CommentAuthorMike Shulman
    • CommentTimeMay 31st 2018

    Re: #29, are you saying that with only the “evaluation” operation he is able to get the functoriality rule somehow? (I don’t quite follow the notation.)

    • CommentRowNumber32.
    • CommentAuthorNoam_Zeilberger
    • CommentTimeMay 31st 2018
    • (edited May 31st 2018)

    Re: #29, are you saying that with only the “evaluation” operation he is able to get the functoriality rule somehow?

    Yes. (And I proved something similar as Prop. 2.23 in the above link.) The key is to prove the following rule as a lemma (in the notation of #28):

    A→B(B→C)→(A→C) \frac{A \to B}{(B \to C) \to (A \to C)}

    Proof: Assume A→BA \to B. By the “evaluation”/”dni” rule, we have ((A→B)→(A→C))→(A→C)((A \to B) \to (A \to C)) \to (A \to C) (taking A→CA \to C as the “answer type” of double-negation introduction). Composing this with the “B” axiom (B→C)→((A→B)→(A→C))(B\to C) \to ((A \to B) \to (A \to C)), we obtain (B→C)→(A→C)(B \to C) \to (A \to C). (Here I am using the auxiliary lemma that it is possible to compose a deduction f:X→Yf : X \to Y with a deduction g:Y→Zg : Y \to Z to obtain a deduction h:X→Zh : X \to Z: first we apply modus ponens on the axiom (Y→Z)→((X→Y)→(X→Z))(Y \to Z) \to ((X \to Y) \to (X \to Z)) together with gg to obtain a deduction g′:((X→Y)→(X→Z))g' : ((X \to Y) \to (X \to Z)), then we apply modus ponens on g′g' with ff to obtain h:X→Zh : X \to Z.)

    Now we can derive the functoriality rule

    A 2→A 1B 1→B 2(A 1→B 1)→(A 2→B 2) \frac{A_2 \to A_1 \quad B_1 \to B_2}{(A_1 \to B_1) \to (A_2 \to B_2)}

    as follows. Suppose given f:A 2→A 1f : A_2 \to A_1 and g:B 1→B 2g : B_1 \to B_2. First we apply modus ponens on the B axiom and gg to obtain g′:(A 2→B 1)→(A 2→B 2)g' : (A_2 \to B_1) \to (A_2 \to B_2). Then we apply the lemma to ff to obtain f′:(A 1→B 1)→(A 2→B 1)f' : (A_1 \to B_1) \to (A_2 \to B_1). Finally we compose f′f' and g′g' to obtain the desired h:(A 1→B 1)→(A 2→B 2)h : (A_1 \to B_1) \to (A_2 \to B_2).

    • CommentRowNumber33.
    • CommentAuthorMike Shulman
    • CommentTimeMay 31st 2018

    Ah, nice! I thought there might be some argument like that, but I didn’t see it.

    • CommentRowNumber34.
    • CommentAuthorNoam_Zeilberger
    • CommentTimeJun 1st 2018
    • (edited Jun 1st 2018)

    Pondering a bit more what you are saying and trying to connect it to things that I know, I think that the definition of “non-unital closed category” you are aiming for should begin with a skew monoid in ProfProf (like I was suggesting in #21) rather than a biased lax monoid. Keeping track of the directions can be tricky (nice table at lax monoidal category, by the way!), so let me spell out my calculations.

    Start with a right-skew monoid (A,M:A⊗A⇸A,U:1⇸A,α,λ,ρ)(A, M : A \otimes A ⇸ A, U : 1 ⇸ A, \alpha, \lambda, \rho) in ProfProf, where we write A=C opA = C^{op} for the opposite of some (non-unital closed) category CC, so that MM and UU correspond to functors M:C×C×C op→SetM : C \times C \times C^{op} \to Set and U:C→SetU : C \to Set. Now we ask that MM is representable by a functor [−,−]:C op×C→C[-,-] : C^{op} \times C \to C in the sense that

    M(c,a;b)=C(c,[a,b]) M(c,a;b) = C(c,[a,b])

    By profunctor composition the two halves of associativity L=M(M(−,−),−)L = M(M(-,-),-) and R=M(−,M(−,−))R = M(-,M(-,-)) are calculated as follows

    L(d,e,a;c)=∫ bC(d,[e,b])×C(b,[a,c])≅C(d,[e,[a,c]])R(d,e,a;c)=∫ bC(d,[b,c])×C(e,[a,b]) L(d,e,a;c) = \int^b C(d, [e,b]) \times C(b, [a,c]) \cong C(d,[e,[a,c]]) \qquad R(d,e,a;c) = \int^b C(d,[b,c]) \times C(e,[a,b])

    so that the right-to-left associator α:R⇒L\alpha : R \Rightarrow L yields the family of “compositor” maps

    L b,c a:[b,c]→[[a,b],[a,c]] L_{b,c}^a : [b,c] \to [[a,b],[a,c]]

    in CC. Now, consider the profunctors U L=M(U,−)U_L = M(U,-) and U R=M(−,U)U_R = M(-,U). I calculate them as follows:

    U L(a;b)=∫ cU(c)×C(c,[a,b])≅U([a,b])U R(c;b)=∫ aC(c,[a,b])×U(a) U_L(a;b) = \int^c U(c) \times C(c,[a,b]) \cong U([a,b]) \qquad U_R(c;b) = \int^a C(c,[a,b]) \times U(a)

    Therefore the left unitor λ:A⇒U L\lambda : A \Rightarrow U_L corresponds to a transformation

    C(a,b)→U([a,b]) C(a,b) \to U([a,b])

    while the right unitor ρ:U R⇒A\rho : U_R \Rightarrow A corresponds to a transformation

    U(a)→C([a,b],b) U(a) \to C([a,b],b)

    So this is what one could call a “non-unital skew closed category”. If you additionally impose that λ\lambda is an isomorphism (= left normality) then I think what comes out is what you are calling a “non-unital closed category”.

    • CommentRowNumber35.
    • CommentAuthorMike Shulman
    • CommentTimeJun 1st 2018

    Those are the same as my calculations: it’s just that since λ\lambda is an isomorphism, it could just as well point the other way. The reason I think it should point the other way is because the criterion of correctness for the definition should be that it coincides with closed multicategories, and we know that multicategories can be identified with normal unbiased lax monoids in ProfProf.

    • CommentRowNumber36.
    • CommentAuthorMike Shulman
    • CommentTimeJun 1st 2018

    By the way, I think you meant M:C op×C op×C→SetM : C^{op}\times C^{op}\times C\to Set.

    I think I see the point now that viewing them as left-normal skew monoids, whose corresponding LBC-algebras are also left-normal and hence equivalently left-normal lax monoids, would make the identification of non-unital closed categories with closed multicategories literally a consequence of Bourke-Lack rather than requiring the argument to be redone in the biased-lax case. Morally I still think the latter ought to be done, though… but I might be too lazy to do it.

  37. Those are the same as my calculations: it’s just that since λ\lambda is an isomorphism, it could just as well point the other way. The reason I think it should point the other way is because the criterion of correctness for the definition should be that it coincides with closed multicategories, and we know that multicategories can be identified with normal unbiased lax monoids in ProfProf.

    Hmm. It’s subtle, but I have a different intuition. Or I guess it’s rather that I don’t want to start from an assumption of left normality. I think the notion of “skew” multicategory discussed by Bourke and Lack is quite natural, and there, what corresponds to the left unitor is the mapping from “tight” morphisms A 0;A 1,…,A n→BA_0;A_1,\dots,A_n \to B to “loose” morphisms A 0,A 1,…,A n→BA_0,A_1,\dots,A_n \to B. My intuition coming from programming languages is that this corresponds to an inclusion of (“pure”) values into (“effectful”) computations, and so I think it will be interesting to consider closed skew multicategories which are not left normal (corresponding to extensions of the lambda calculus with effects). That is quite informal intuition, though.

    In any case, I wanted to elaborate a bit more formally what I was alluding to at the end of #29, because I think it might be related to your ideas in #22, and possibly to this question of left normality. Given a (unital or non-unital, not necessarily left normal) skew closed category CC, we can consider its category of covariant presheaves [C,Set][C,Set] as a right-skew monoidal category (or alternatively [C,Set] op[C,Set]^{op} as a left-skew monoidal category of course). Then it is interesting to consider _monoids_in [C,Set][C,Set], which correspond to “deductively closed presheaves” R:C→SetR : C \to Set, in the sense that the multiplication map gives an extranatural transformation

    m:R(a→b)×R(a)→R(b) m : R(a \to b) \times R(a) \to R(b)

    corresponding to “modus ponens”, while the unit gives a natural transformation

    u:U(a)→R(a) u : U(a) \to R(a)

    corresponding to the inclusion of all “tautologies” into RR.

    Let me restrict now to the unital, 2-enriched case, because that’s what I considered in the aforementioned paper (but I think it can be extended to the non-unital, Set-enriched case). In this case, a monoid RR in [C,2][C,2] (where CC is a unital skew closed preorder) corresponds to an upwards closed subset of CC such that the following pair of conditions hold:

    a→b∈Ra∈Rb∈RI∈R \frac{a \to b \in R \quad a \in R}{b \in R} \qquad \frac{}{I \in R}

    Given such a monoid, we can construct a new preordered category C/R=(C,≤ R)C/R = (C,\le_R) with the same objects as CC but where a≤ Rba \le_R b iff a→b∈Ra\to b \in R. The fact that this relation is transitive relies on both the multiplication mm of RR and the original associator α\alpha/compositor LL of CC, while the fact that it is reflexive relies on the unit uu of RR together with the left unitor λ\lambda of CC. There is also an evident embedding i:C→C/Ri : C \to C/R (again relying on the left unitor λ\lambda), in the sense that the preorder ≤ R\le_R is an extension of ≤\le.

    But now we might wonder whether C/RC/R is (skew) closed, and whether we can legitimately see it as a quotient. And here is where things get more interesting: although we can show that the original operation a→ba\to b is monotone in bb relative to the coarser order ≤ R\le_R, it need not be antitone in aa. So this is where we need to impose an additional condition of closure under “double-negation introduction”:

    a∈R(a→b)→b∈R \frac{a \in R}{(a \to b) \to b \in R}

    Note that this dni-condition is equivalent (at least in the 2-enriched case) to the existence of a natural transformation −⊗R⇒R⊗−-\otimes R \Rightarrow R\otimes-, where ⊗\otimes is the multiplication operation in [C,2][C,2]. Given this additional closure condition, we can prove that a→ba \to b is antitone in aa relative to ≤ R\le_R and thus defines a functor (C/R) op×C/R→C/R(C/R)^{op} \times C/R \to C/R, which together with the original unit II turns C/RC/R into a left normal skew-closed category. Moreover we can show that (C/R,i:C→C/R)(C/R, i : C \to C/R) has the appropriate universal property of the quotient.

    I did not try to work this out, but my intuition was that in the SetSet-enriched case, RR could be thought of as (generated by) a family of typed combinators, which is then used to construct a closed category C RC_R with additional structure. Perhaps that aligns with some of your ideas?

  38. By the way, I think you meant M:C op×C op×C→SetM : C^{op}\times C^{op}\times C\to Set.

    Oops…I mean, that was just to prove my point that keeping track of all the directions/signs can be tricky! :-)

    • CommentRowNumber39.
    • CommentAuthorMike Shulman
    • CommentTimeJun 1st 2018

    I don’t really understand all this skew business, and I’m not really motivated to put in the effort right now, since I don’t know or care about any of the relevant examples yet, and from a pure category-theoretic point of view it seems bizarre to me to have the unit morphisms pointing in different directions. (Even more bizarre than a noninvertible biased associator.) I accept that they do arise naturally in some contexts and are useful for some purposes, but the correspondence between non-unital closed categories and closed multicategories seems to me something much more basic, that should be simple to motivate, explain, and prove, without having to descend into this more exotic skew business.

    • CommentRowNumber40.
    • CommentAuthorMike Shulman
    • CommentTimeJun 7th 2018

    List some examples of closed monoidal categories whose closed structure is more natural than their monoidal structure.

    diff, v54, current

    • CommentRowNumber41.
    • CommentAuthorMike Shulman
    • CommentTimeJun 7th 2018

    I suppose a better name for “non-unital closed categories” would be “semi-closed categories”, by analogy to other uses of “semi-” for non-unitality (e.g. semigroup, semisimplicial set, semicategory…)

    diff, v54, current

    • CommentRowNumber42.
    • CommentAuthorNoam_Zeilberger
    • CommentTimeJun 9th 2018
    • (edited Jun 9th 2018)

    Re #41, I wouldn’t call these “semi-closed categories” since that name has already been used by Bourke (#16) for the weaker structure consisting of just a bifunctor [−,−]:C op×C→C[-,-] : C^{op} \times C \to C equipped with the compositor transformations [Y,Z]→[[X,Y],[X,Z]][Y,Z] \to [[X,Y],[X,Z]] satisfying a pentagon axiom. And as you know (#17), that terminology is natural because such semi-closed categories indeed correspond to (biased-lax/skew) semigroups in ProfProf with a representability requirement.

    What’s tricky here is that a “non-unital” closed category is actually equipped with a unit (in ProfProf), it is just not representable. I’m not sure if there is a succinct way of conveying that…perhaps something like a “semi-closed category with a presheaf of global elements”?

    • CommentRowNumber43.
    • CommentAuthorMike Shulman
    • CommentTimeJun 10th 2018

    Hrm, I suppose you’re right. There’s no name for a multicategory that has binary tensor products but not a unit, either.

    • CommentRowNumber44.
    • CommentAuthorMike Shulman
    • CommentTimeJun 10th 2018

    “prounital”?

  45. “prounital”?

    Sounds good to me!

    There’s no name for a multicategory that has binary tensor products but not a unit, either.

    You mean a multicategory where there are universal binary maps A,B→A⊗BA,B \to A\otimes B but not a universal nullary map ⋅→I\cdot \to I? I don’t know a name for that, but I think the multicategory equivalent of a semigroup category is a multicategory with no nullary operations that is representable in the standard sense, so “representable constantless multicategory” (adopting the terminology you suggested before), or “representable non-unitary multicategory” (using Fresse’s terminology for the corresponding operads, which I don’t find particularly evocative).

    • CommentRowNumber46.
    • CommentAuthorMike Shulman
    • CommentTimeJun 11th 2018

    You mean a multicategory where there are universal binary maps A,B→A⊗BA,B \to A\otimes B but not a universal nullary map ⋅→I\cdot \to I?

    Yes, that’s what I meant. Since that’s the monoidal analogue of prounital closed categories, which (conjecturally) correspond to multicategories that have nullary maps, but have a “binary internal-hom” but not a “nullary one”.

    • CommentRowNumber47.
    • CommentAuthorMike Shulman
    • CommentTimeJun 11th 2018

    Change “semi-closed category” to “prounital closed category”

    diff, v56, current

    • CommentRowNumber48.
    • CommentAuthorKeith Harbaugh
    • CommentTimeApr 9th 2019

    Added link to published version of Oleksandr Manzyuk, _Closed categories vs. closed multicategories (TAC Vol. 26, 2012). Hope I got your formatting schemes not too messed up!

    diff, v58, current

    • CommentRowNumber49.
    • CommentAuthorMike Shulman
    • CommentTimeJan 8th 2020

    Added one axiom to prounital closed categories.

    diff, v60, current

    • CommentRowNumber50.
    • CommentAuthorMike Shulman
    • CommentTimeJun 3rd 2020

    Added remark that a symmetric closed category is automatically associative as a promonoidal category, hence a weaker representability condition suffices to make it monoidal.

    diff, v62, current

    • CommentRowNumber51.
    • CommentAuthorgintaras
    • CommentTimeSep 29th 2021
    The opposite ordered space remains ordered space. So we can ask which of two categories is closed with mappings
    $L^x_{y,z}$. Other categories doesn't allow opposite category. For example the category of Sets or Additive groups.
    We can add two functions $+g$ if we have addition in target space, but not in source space.
    So the category can be closed wih mappings $L^x_{y,z} $ without having defined mappings $R^x_{y,z}$.
    Interesting closed category is provided by uniform mappings of uniform spaces.
    • CommentRowNumber52.
    • CommentAuthorvarkor
    • CommentTimeSep 27th 2022

    Mention right-closed categories.

    diff, v63, current

    • CommentRowNumber53.
    • CommentAuthorUrs
    • CommentTimeApr 25th 2023

    added DOI-link for:

    diff, v65, current

    • CommentRowNumber54.
    • CommentAuthorvarkor
    • CommentTimeJul 27th 2023

    I noticed that it would be more natural to define closed categories without assuming a category from the outset, and then I realised Mike had already suggested this back in #22 :) It reminds me somewhat of the fact that a relative monad can be defined in terms only of an object-function, and functoriality derived from the extension operator.

    Did anything ever come of this? It would be nice for it to be written out in the literature.

    • CommentRowNumber55.
    • CommentAuthorvarkor
    • CommentTimeAug 27th 2023
    • (edited Aug 27th 2023)

    Added a reference to a paper of Pavelka.

    diff, v68, current

1 to 55 of 55

  1.