In a cartesian closed category, the exponential object [A,B] basically internalizes the collection of morphisms from A to B.

Is there some similar notion that internalizes the isomorphisms between A and B? What about the unique isomorphisms?

It seems like you could get somewhere with subobject classifiers, but maybe there is something more elementary?

My apologies if this is well-known; I haven't been able to dig anything up via searching.

  • 3
    $\begingroup$ What are the "unique isomorphisms" from $A$ to $B$? $\endgroup$ – Mariano Suárez-Álvarez Sep 9 '13 at 3:31
  • $\begingroup$ Suppose $\phi$ is an iso from $A$ to $B$. Then $\phi$ is unique if, for every other iso $\phi'$ from $A$ to $B$, $\phi = \phi'$. $\endgroup$ – ct-novice Sep 9 '13 at 3:41
  • 3
    $\begingroup$ If there is exactly one isomorphism from $A$ to $B$ (or indeed if there is exactly one of anything, in a category with terminal object) then that isomorphism (or whatever) is classified by the terminal object. You probably have some other idea hidden behind this one of unique isomorphisms. $\endgroup$ – Colin McLarty Sep 9 '13 at 9:03
  • $\begingroup$ I'm primarily interested in categories for their connection to denotational semantics of lambda calculi. My question is motivated by wondering what the type of "type equivalences" is. We might consider types (objects of a category) equal if there is an iso between them, or we might be interested in the stronger property that there is a unique iso (I'm not sure). In the latter case, I suppose the classifying object would either be (isomorphic to) the terminal object or the initial object; but which it is depends on $A$ and $B$. $\endgroup$ – ct-novice Sep 10 '13 at 23:55

There is a map $[A, B] \times [B, A] \to [A, A] \times [B, B]$ given by composition in each of the possible directions. There is also a map $1 \to [A, A] \times [B, B]$ which picks out $(\text{id}_A, \text{id}_B)$. These fit together into a diagram $[A, B] \times [B, A] \to [A, A] \times [B, B] \leftarrow 1$ and the object of isomorphisms is the limit (so pullback) of this diagram.

  • $\begingroup$ Here is a more down-to-earth explanation of Qiaochu's answer: $\underline{\mathrm{Isom}}(A,B)$ should be a subobject of $\underline{\mathrm{Hom}}(A,B)$, namely of those morphisms which have an inverse. But since inverses are unique, we can also see it as the subobject of $\underline{\mathrm{Hom}}(A,B) \times \underline{\mathrm{Hom}}(B,A)$ of all $(f,g)$ such that $fg=1$ and $gf=1$. This is the preimage of $(1,1)$ under the map $\underline{\mathrm{Hom}}(A,B) \times \underline{\mathrm{Hom}}(B,A) \to \underline{\mathrm{Hom}}(A,A) \times \underline{\mathrm{Hom}}(B,B)$, $(f,g) \mapsto (gf,fg)$. $\endgroup$ – Martin Brandenburg Sep 9 '13 at 10:44
  • $\begingroup$ It is a good exercise to verify directly from the definition of exponentials that there is indeed an arrow $[A, B] \times [B, A] \to [A, A] \times [B, B]$ as described by Qiaochu. $\endgroup$ – Colin McLarty Sep 9 '13 at 23:23
  • $\begingroup$ Does the object so constructed have a well-known name? Would I just call it the classifying object of isomorphisms? $\endgroup$ – ct-novice Sep 10 '13 at 23:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.