Not signed in (Sign In)

Start a new discussion

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-categories 2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry beauty bundles calculus categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology combinatorics complex-geometry computable-mathematics computer-science connection constructive constructive-mathematics cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry differential-topology digraphs duality education elliptic-cohomology enriched fibration finite foundations functional-analysis functor galois-theory gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck 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 infinity integration integration-theory k-theory lie lie-theory limits linear linear-algebra locale localization logic manifolds mathematics measure-theory modal-logic model model-category-theory monad monoidal monoidal-category-theory morphism motives motivic-cohomology multicategories noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory 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-theory subobject superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory 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
    • CommentTimeOct 20th 2017

    I added to star-autonomous category a mention of “*\ast-autonomous functors”.

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeOct 20th 2017

    I have a question about the definitions of star-autonomous category. The proof given there shows that the two definitions are equivalent as properties of a symmetric monoidal category. (Actually, it doesn’t quite finish the proof by showing that d Ad_A is an isomorphism for I *\bot\coloneqq I^* in the second definition, but I can believe that that works.) However, are they equivalent as structure? Or, technically, I suppose, as stuff?

    The first definition equips a symmetric monoidal category with the stuff of an object \bot, the (property-like) structure of being closed, and the property of the double-dualization map d Ad_A being an isomorphism. The second definition equips it with the stuff of a functor () *(-)^*, the structure of a natural isomorphism 𝒞(AB,C *)𝒞(A,(BC) *)\mathcal{C}(A\otimes B,C^*) \cong \mathcal{C}(A,(B\otimes C)^*), and… no properties. This immediately makes me suspicious: nearly always non-property-like structure has to be equipped with coherence properties to be “correct”. And I can easily imagine coherence properties that the second definition could satisfy, like the equality of two isomorphisms 𝒞(A(BC),D *)𝒞(A,(B(CD)) *)\mathcal{C}(A\otimes (B\otimes C),D^*) \cong \mathcal{C}(A,(B\otimes (C\otimes D))^*) — and it seems likely that when the data is constructed from the first definition then it would satisfy these properties. Are these properties automatically always satisfied by the second definition? Or (as seems more likely to me) does passing back and forth from the second definition to the first and back again “coherentify” the isomorphism 𝒞(AB,C *)𝒞(A,(BC) *)\mathcal{C}(A\otimes B,C^*) \cong \mathcal{C}(A,(B\otimes C)^*) into a possibly-different one that does satisfy the coherence axiom, analogous to replacing an equivalence by an adjoint equivalence?

    • CommentRowNumber3.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 21st 2017
    • (edited Oct 21st 2017)

    Mike, I suspect I was the one who introduced the second definition (I haven’t gone back through the history to check). I’m not sure that I have much time to investigate this, but if the me of yesteryear wanted to argue back, I might have said this: are you sure this is non-property-like structure?

    You probably recognize that the second definition is trying to define closed structure (where to make that clearer it should probably be written instead as 𝒞(AB,C)𝒞(A,(BC *) *)\mathcal{C}(A \otimes B, C) \cong \mathcal{C}(A, (B \otimes C^\ast)^\ast)), and closed structure is property-like, right? So at the moment I’m a little puzzled where the problem might lie.

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeOct 21st 2017

    It’s property-like to assert the existence of some new object together with a universal property for it. But it’s not generally property-like to assert that some object that’s already present in the doctrine has some new universal property. Put differently, that isomorphism could equivalently be phrased as saying (1) 𝒞\mathcal{C} is closed, with internal-homs [B,C][B,C], and (2) we have a specified natural isomorphism [B,C](BC *) *[B,C] \cong (B\otimes C^*)^*. Part (1) is property-like, but part (2) is not.

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeOct 21st 2017

    On the other hand, if the isomorphism 𝒞(AB,C)𝒞(A,(BC *) *)\mathcal{C}(A \otimes B, C) \cong \mathcal{C}(A, (B \otimes C^\ast)^\ast) were asserting a universal property for the operation () *(-)^*, then together the two of them would be property-like. But it isn’t quite doing that; it’s saying that something constructed in a more complicated way using () *(-)^* and \otimes has a universal property.

    • CommentRowNumber6.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 21st 2017

    Okay, thanks. At this point I don’t know how to amend definition 2 in a way that doesn’t make it tautologously the same as definition 1. Rats. We can scrap it if you don’t see a fix-up either.

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeOct 22nd 2017

    Here’s a specific example to consider: the category FDVectFDVect of finite-dimensional vector spaces over a field kk, which is compact closed and hence star-autonomous. Then I believe the “obvious” definition-2 structure τ:𝒞(AB,C *)𝒞(A,(BC) *)\tau : \mathcal{C}(A \otimes B, C^\ast) \cong \mathcal{C}(A, (B \otimes C)^\ast) can be “twisted” by multiplying by any nonzero element tkt\in k to obtain another such structure τ^\hat{\tau}. An isomorphism between this structure and the original one would consist of natural isomorphisms ρ A:A *A *\rho_A : A^\ast \cong A^\ast, which I think would have to be multiplication by some nonzero rkr\in k, such that the square

    𝒞(AB,C *) τ 𝒞(A,(BC) *) ρ C ρ BC 𝒞(AB,C *) τ^ 𝒞(A,(BC) *) \array{ \mathcal{C}(A \otimes B, C^\ast) & \xrightarrow{\tau} & \mathcal{C}(A, (B \otimes C)^\ast)\\ ^{\rho_{C}}\downarrow && \downarrow^{\rho_{B\otimes C}} \\ \mathcal{C}(A \otimes B, C^\ast) & \xrightarrow{\hat{\tau}} & \mathcal{C}(A, (B \otimes C)^\ast) }

    commutes. But this says tr=rt r = r, hence t=1t=1. So the twisted version is not equivalent to the untwisted one. But it seems clear that even the twisted one will give rise to the standard form of definition-1, since the only non-property-like data there is the dualizing object kk, and that when we come backwards to definition 2 we will get only the untwisted version.

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeOct 22nd 2017

    My proposal would be to add to definition 2 the coherence condition that the composites

    𝒞(A(BC),D *)𝒞(A,((BC)D) *)𝒞(A,(B(CD)) *) \mathcal{C}(A\otimes (B\otimes C), D^\ast) \cong \mathcal{C}(A, ((B\otimes C) \otimes D)^\ast) \cong \mathcal{C}(A, (B\otimes (C \otimes D))^\ast)

    and

    𝒞(A(BC),D *)𝒞((AB)C,D *)𝒞(AB,(CD) *)𝒞(A,(B(CD)) *) \mathcal{C}(A\otimes (B\otimes C), D^\ast) \cong \mathcal{C}((A\otimes B) \otimes C, D^\ast) \cong \mathcal{C} (A\otimes B, (C\otimes D)^\ast) \cong \mathcal{C}(A, (B\otimes (C \otimes D))^\ast)

    are equal. In the twisted example this would entail t 2=t 3t^2 = t^3, hence t=1t=1. In general it would require some work to show that this is sufficient, but I think it’s likely to be true.

    At first I thought Definition 2 doesn’t appear in the literature (although I don’t have a copy of Barr’s original monograph yet), but I just noticed that it is the definition given in section 5 of Day-Street. There they say

    For the reader interested in checking that our *\ast-autonomous monoidal categories agree with Michael Barr’s *\ast-autonomous categories, we recommend Definition 2.3 of [Ba2] as the appropriate one for comparison.

    Reference [Ba2] is Barr’s non-symmetric star-autonomous categories, and his definition 2.3 (“Definition C”) is similar to our Definition 2 but includes only the special case of the isomorphism where AA is the unit object. Is that enough to eliminate the ambiguity? (Although Barr’s “Definition D” therein also makes me worried about coherence, since it also consists of an isomorphism satisfying no conditions.)

    Also, sections 8 and 10 of Mellies add to the abstract Day-Street definition an associativity pentagon that I think reduces in the concrete case of profunctors to my proposed coherence axiom above. This is some additional justification for it, although it still remains to be proven that it’s strongly equivalent to Definition 1.

    • CommentRowNumber9.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 22nd 2017

    Right, so the message of #7 is that the possible structures in that case are in bijection with automorphisms of the unit object II, and I think that holds generally. By setting B=IB = I in 𝒞(AB,C)𝒞(A,(BC *) *)\mathcal{C}(A \otimes B, C) \cong \mathcal{C}(A, (B \otimes C^\ast)^\ast), we have by Yoneda an assigned isomorphism CC **C \cong C^{\ast\ast}. Then, putting C=I *C = I^\ast, we get the universal property of () *(-)^\ast via 𝒞(AB,I *)𝒞(A,B *)\mathcal{C}(A \otimes B, I^\ast) \cong \mathcal{C}(A, B^\ast), whereupon your comment #5 kicks in. So it all comes down to which natural isomorphism CC **C \cong C^{\ast\ast} we are dealing with. The set of such isomorphisms is a torsor over the group of automorphisms of the identity functor CCC \mapsto C; by an enriched Yoneda argument this boils down to the group of automorphisms of II.

    Your suggestion for the coherence condition in #8 nails down which automorphism of II we are dealing with to the identity map, similar to the way in which the pentagon condition for monoidal categories forces the associator for the tensor product on vector spaces to be the standard one. In fact, your condition is a pentagon! And based on your description I’m pretty sure Barr’s specialization in his definition C would nail it down as well, even though I haven’t looked at it yet. There may be other simple ways of writing down an appropriate coherence condition.

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeOct 22nd 2017
    • (edited Oct 22nd 2017)

    Another condition one could ask for is a “unit” condition that 𝒞(AB,C *)𝒞(A,(BC) *)\mathcal{C}(A \otimes B, C^\ast) \cong \mathcal{C}(A, (B \otimes C)^\ast) becomes the identity when B=IB=I. (I actually prefer 𝒞(AB,C *)𝒞(A,(BC) *)\mathcal{C}(A \otimes B, C^\ast) \cong \mathcal{C}(A, (B \otimes C)^\ast) to 𝒞(AB,C)𝒞(A,(BC *) *)\mathcal{C}(A \otimes B, C) \cong \mathcal{C}(A, (B \otimes C^\ast)^\ast) because the former applies verbatim in the non-symmetric case, whereas the latter has to be modified to 𝒞(AB,C)𝒞(A,(B *C) *)\mathcal{C}(A \otimes B, C) \cong \mathcal{C}(A, (B \otimes {}^\ast C)^\ast), where *(){}^\ast(-) is the inverse of () *(-)^\ast.)

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeOct 22nd 2017

    By “automorphisms of the identity functor” do you mean 𝒞\mathcal{C}-enriched automorphisms? Otherwise I don’t see how the unit object enters. Is it obvious that () **(-)^{\ast\ast} is 𝒞\mathcal{C}-enriched and that only enriched automorphisms work?

    • CommentRowNumber12.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 22nd 2017

    Re #11: yes, I mean enriched. Admittedly I didn’t check carefully yet that () *(-)^\ast is enriched, but let’s see: a contravariant strength would take the form (BA) *BA *(B \otimes A)^\ast \otimes B \to A^\ast which we can derive from the identity (BA) *(BA) *(B \otimes A)^\ast \to (B \otimes A)^\ast, so I think it would work out.

    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeOct 22nd 2017

    Oh, silly me: of course () **(-)^{\ast\ast} is 𝒞\mathcal{C}-enriched, since it’s isomorphic to the identity.

    But I still don’t quite understand #9: I see that the isomorphism 𝒞(AB,C)𝒞(A,(BC *) *)\mathcal{C}(A \otimes B, C) \cong \mathcal{C}(A, (B \otimes C^\ast)^\ast) determines an isomorphism from () **(-)^{\ast\ast} to the identity, and also a universal property of () *(-)^\ast, as special cases, but how do these special cases in turn determine it?

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeOct 25th 2017

    Ok, finally got my copy of Barr’s original monograph “*\ast-autonomous categories” from ILL.

    Firstly I was not quite right in #8 that our Definition 2 is that of Day-Street, since the former requires a priori only that () *(-)^\ast is fully faithful, whereas Day and Street require it to be an equivalence (as does Definition C of Barr’s non-symmetric paper). But that doesn’t affect its coherence or lack thereof.

    Our Definition 2 actually does appear in Barr’s monograph in paragraph (4.3). It’s not his definition of *\ast-autonomous category, but he proves that this data “suffices to determine” a *\ast-autonomous category, which isn’t quite the same as claiming that it’s an equivalent definition; so that could be compatible with what we’re seeing.

    However, his actual definition doesn’t seem quite right to me either. He defines a *\ast-autonomous category to be a closed symmetric monoidal category 𝒞\mathcal{C} together with a 𝒞\mathcal{C}-enriched functor (which he calls a “closed functor” for some reason) () *:𝒞 op𝒞(-)^\ast : \mathcal{C}^{op}\to \mathcal{C} and a 𝒞\mathcal{C}-enriched natural isomorphism AA **A \cong A^{\ast\ast}. It seems like this would have the same problem of being a torsor over the center of 𝒞\mathcal{C}.

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeApr 17th 2018

    Added Hyland-Schalk reference

    diff, v45, current

    • CommentRowNumber16.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 29th 2018

    Thought I’d add Mike’s explanation of “autonomous”.

    diff, v47, current

    • CommentRowNumber17.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 8th 2019

    The links aren’t appearing for me at star-autonomous category in this sentence

    Regarding the use of “autonomous”, this was once used as a bare adjective to describe a closed monoidal category, or sometimes a compact closed monoidal category,…

    Anyone else?

    • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeJan 8th 2019

    Same here. Perhaps related to the square brackets around that sentence?

    • CommentRowNumber19.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 8th 2019

    That must be it. Have shifted to round ones.

    • CommentRowNumber20.
    • CommentAuthorMike Shulman
    • CommentTimeJan 8th 2019

    Still a bug, though, even if we can work around it easily. (-:

Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)