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.

Improve this question
$\endgroup$
4
  • 3
    $\begingroup$ What are the "unique isomorphisms" from $A$ to $B$? $\endgroup$
    – Mariano Suárez-Álvarez
    Commented 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
    Commented 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$
    – Colin McLarty
    Commented 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
    Commented Sep 10, 2013 at 23:55

1 Answer 1

Reset to default
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.

Improve this answer
$\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$
    – Martin Brandenburg
    Commented 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$
    – Colin McLarty
    Commented 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
    Commented Sep 10, 2013 at 23:56

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .