0
$\begingroup$

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.

$\endgroup$
4
  • 3
    $\begingroup$ What are the "unique isomorphisms" from $A$ to $B$? $\endgroup$ Sep 9, 2013 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, 2013 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$ Sep 9, 2013 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, 2013 at 23:55

1 Answer 1

11
$\begingroup$

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.

$\endgroup$
3
  • $\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$ Sep 9, 2013 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$ Sep 9, 2013 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, 2013 at 23:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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