I have just added a missing OP to the 'alternative definition'.
I have some problems with this article. The 'definition' is not the one given by Barr in his LNM monograph. Moreover, neither the 'alternative definition' nor the 'property' appear in either of the cited articles. I have not taken the time to verify them, and I suppose that they may be wrong. Are you sure that existence of an equivalence implies existence of a dualising object?
Perhaps one should start with the non-symmetric definition.
I think that it should be mentioned that *-autonomous categories are the categorical semantics of multiplicative-additive linear logic.
In the entry for monoidal category the unit is denoted by the letter "I" and not 1. Perhaps we should continue that convention here. Another reason is that 1 is often used for the identity morphism so it may be confusing.
In the last definition the functor (-)* should be an equivalence. I am not sure if the condition A** isomorphic to A is enough. Why I am not sure that * is a functor is enough: we need to be able to say that any object of C can be written as D* for some D. An equivalence allows us to say that and then the isomorphism gives the desired A** isomorphic to A.
To see that I* is the dualising object note that the internal hom is defined by . Then we see that since .
Relationship with compact closed categories
I have removed the claim:
- A *-autonomous category is compact closed iff for each pair (A,B) of objects:
from the article, because I believe it to be false, or at least unproven. It is true that this claim is made, parenthetically, in the Kelly-Laplaza paper on compact closed categories; it is stated without proof there, and I think the authors made a mistake. There is also a fallacious "proof" that is occasionally seen, which may be another factor contributing to the persistence of this apparent myth.
I once emailed the late Max Kelly to ask about this, towards the end of his life. Sadly he was already unwell, and directed me instead to his former student Ross Street. Street told me he did not believe it to be true, and expressed surprise that such a claim is made in Kelly and Laplaza's paper.
I don't think any similar claim should be added to this article without a reference to a proof.
The above claim is true, and if I find a proof in the literature I will give a reference. I also have a proof written down in front of me. Here is the idea. It mostly relies on the following isomorphisms which are valid in any star-autonomous category with the above property: C(A, C # SB) ~ C(A, S(B # SC)) ~ C(A # B, C)... where # is tensor and S is the star operation. Set C = I and A = SB (assuming the monoidal category is strict) and follow the isomorphisms forward to get the evaluation map SB # B ---> I and set A = I and C = B and follow the isomorphisms backwards to get the coevaluation map I ---> B # SB. To prove the triangle axioms is a diagram chase. This works in the non-symmetric case with very little change. You must be careful with the left and right star operations though. —Preceding unsigned comment added by 188.8.131.52 (talk) 05:41, 21 January 2009 (UTC)
Characterization as linearly distributive categories with negation
Perhaps it should be mentioned somewhere that the notion of *-autonomous category is the same as the notion of linearly distributive category with negation, both in the symmetric case and in the non-symmetric case. I imagine I will do it myself in due time, but I thought I should preface it here, the original documents would be a pair of papers by Robin Cockett and Robert Seely. —Preceding unsigned comment added by 184.108.40.206 (talk) 11:41, 22 January 2009 (UTC)