Added pointer to:
added the publication data:
Added a reference to Dold and Puppe’s work which implies that a -autonomous category with a natural isomorphism is a compact closed category.
]]>I think the generalization from posets (as in Girard’s phase semantics) to more general idempotent adjunctions was original. I haven’t written it or seen it anywhere else, so yes, I guess you could cite the nLab page.
]]>Incidentally, Mike has a corresponding MathOverflow question/comment at MO:343167.
]]>Okay, so is this observation due to Mike Shulman? Should I cite this nLab entry as the original reference on “predualizing objects”?
]]>I don’t know off the top of my head. But that paragraph was added in revision 39 by Mike Shulman.
]]>One of the examples is
Suppose is a closed symmetric monoidal category equipped with a “pre-dualizing object” , in the sense that the contravariant self-adjunction is idempotent, i.e. the double-dualization map is an isomorphism whenever is of the form . (Note that idempotence is automatic if is a poset.) Then the category of fixed points of this adjunction, i.e. the full subcategory of objects of the form , is -autonomous. For it is closed under , as , and reflective with reflector , and it contains since . Hence it is closed symmetric monoidal with tensor product , and all its double-dualization maps are isomorphisms by assumption. A historically important example is Girard’s phase semantics of linear logic. Note that this category is a full subcategory of closed under duality — indeed, it is the intersection of the two embeddings of and therein — but its tensor product is not the restriction of the tensor product of .
Is there a citeable reference where this example is presented? Who should be credited for this observation?
]]>Added definition of the internal hom from .
]]>Suggest a new notion of weak -autonomous category: « We can weaken the requirement that the canonical morphism is an isomorphism to the one that it is a monomorphism. »
is a weak -autonomous category. It allows to speak about duality in more general situations.
I would be glad to have returns on this.
]]>Added an example of a subcategory of which is a *-autononomous category and the reference by Michael Barr which develops the idea.
]]>Change the link from Vect to FinVect category in examples
Oleg Nizhnik
]]>Added a list of relations to other structures, including the fact that a traced -autonomous category must be compact closed (Hajgató and Hasegawa).
]]>Still a bug, though, even if we can work around it easily. (-:
]]>That must be it. Have shifted to round ones.
]]>Same here. Perhaps related to the square brackets around that sentence?
]]>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?
]]>Thought I’d add Mike’s explanation of “autonomous”.
]]>Added Hyland-Schalk reference
]]>Ok, finally got my copy of Barr’s original monograph “-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 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 -autonomous category, but he proves that this data “suffices to determine” a -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 -autonomous category to be a closed symmetric monoidal category together with a -enriched functor (which he calls a “closed functor” for some reason) and a -enriched natural isomorphism . It seems like this would have the same problem of being a torsor over the center of .
]]>Oh, silly me: of course is -enriched, since it’s isomorphic to the identity.
But I still don’t quite understand #9: I see that the isomorphism determines an isomorphism from to the identity, and also a universal property of , as special cases, but how do these special cases in turn determine it?
]]>Re #11: yes, I mean enriched. Admittedly I didn’t check carefully yet that is enriched, but let’s see: a contravariant strength would take the form which we can derive from the identity , so I think it would work out.
]]>By “automorphisms of the identity functor” do you mean -enriched automorphisms? Otherwise I don’t see how the unit object enters. Is it obvious that is -enriched and that only enriched automorphisms work?
]]>Another condition one could ask for is a “unit” condition that becomes the identity when . (I actually prefer to because the former applies verbatim in the non-symmetric case, whereas the latter has to be modified to , where is the inverse of .)
]]>