I'm reading Basic Category Theory for Computer Scientists by Benjamin C. Pierce and in exercice 1.4.6, he asks what the terminal objects are in $Set^\to$.
Let $C$ be a category.
The category $C^\to$ is defined as a category so that:
- An objet in $C^\to$ is an arrow in $C$
- An arrow in $C^\to$ from $f:A\to B$ to $f':A'\to B'$ is a pair $(a,b)$ so that the following diagram commutes $$\require{AMScd} \begin{CD} A @>{a}>> A'\\ @V{f}VV @V{f'}VV \\ B @>{b}>> B' \end{CD}$$
I think I have solved this exercice (but I'd really appreciate comments on the proofs):
Theorem 1: Terminal objects in $Set^\to$ are isomorphisms whose codomain is a terminal object in $Set$:
Lemma 2: Given a morphism $f:A\to B$ and an isomorphism $f':A'\to B'$, $\exists !(a:A\to A',b:B\to B'), f;b=a;f'$ is equivalent to $\exists !b:B\to B'$.
Proof 2: Since $f'$ is an isomorphism, $\exists !(a:A\to A',b:B\to B'), f;b=a;f'$ is equivalent to $\exists !(a:A\to A',b:B\to B'), f;b;f'^{-1}=a$. We now prove that $\exists !(a:A\to A',b:B\to B'), f;b;f'^{-1}=a$ is equivalent to $\exists !b:B\to B'$.
"$\Longrightarrow$": Suppose $\exists !(a:A\to A',b:B\to B'), f;b;f'^{-1}=a$. The existence of $b:B\to B'$ is trivial. Suppose there were two function $b_1:B\to B'$ and $b_2:B\to B'$. By setting $a_1:=f;b_1;f'^{-1}$ and $a_2:=f;b_2;f'^{-1}$, we contradict the uniqueness hypothesis. So $\exists !b:B\to B'$.
"$\Longleftarrow$": Suppose $\exists !b$. Defining $a:=f;b;f'^{-1}$, we get the existence of $(a:A\to A',b:B\to B')$. The uniqueness of $b$ is given by the hypothesis and the uniqueness of $a$ for a given $b$ is ensured by the equation so $\exists !(a:A\to A',b:B\to B'), f;b=a;f'$.
Proof 1:
"$\Longleftarrow$": Let $f':A'\to B'$ be an isomorphism so that $B'$ is terminal in $Set$. By definition, we have $\forall B \in Set, \exists !b:B\to B'$. This is equivalent to $\forall A,B\in Set, \forall f:A\to B, \exists !b:B\to B'$ which is, by Lemma 1, equivalent to $\forall A,B\in Set, \forall f:A\to B, \exists !(a:A\to A',b:B\to B'), f;b=a;f'$. So $f'$ is terminal in $Set^\to$.
"$\Longrightarrow$": Let $f':A'\to B'$ be a terminal object in $Set^\to$ (where $A'$ and $B'$ are objects of $Set$).
To prove that $f'$ is injective, suppose it is not. We can find $x,y\in A'$ so that $x\not=y$ but $f(x)=f(y)$. And then the function $$s:\left\{\begin{array}{ll} x\mapsto y\\ y\mapsto x\\ \lambda\mapsto \lambda \text{ for } \lambda\not\in\{x,y\} \end{array}\right.$$ that swaps $x$ and $y$ is a valid candidate for $a$. Since $Id_A$ is a distinct valid candidate, $a$ is not unique which is absurd so $f'$ is injective. $$\require{AMScd} \begin{CD} {A'} @>{a:=Id_A\mid a := s}>> A'\\ @V{f'}VV @V{f'}VV \\ {B'} @>{b}>> B' \end{CD}$$
To prove that $f'$ is surjective, suppose it is not. We can find $y\in B'$ so that $\forall x\in A', f(x)\not=y$.
- If $B'$ contains an element $z\in B'$ so that $z\not= y$, the function $$p:\left\{\begin{array}{ll} y\mapsto z\\ \lambda\mapsto \lambda \text{ for } \lambda\not=y \end{array}\right.$$ that sends all elements to themselves except $y$ which is sent to $z$ is a valid candidate for $b$. Since $Id_B$ is a distinct valid candidate, $b$ is not unique which is absurd.
- If $B'=\{y\}$, $\forall x\in A', f(x)\not = y$ has to be vacuously true so $A'=\emptyset$. Setting $A:=\{y\}$, $B:=\{y\}$ and $f:=Id_{\{y\}}$, we don't have the existence of $a$ which is absurd. $$\require{AMScd} \begin{CD} {A:=\{y\}} @>{a}>> A'=\emptyset\\ @V{f:=Id_{\{y\}}}VV @V{f'}VV \\ {B:=\{y\}} @>{b}>> B'=\{y\} \end{CD}$$
- Since both cases are absurd, $f'$ is surjective.
Since $f'$ is injective and surjective, it is bijective and is therefore an isomorphism in $Set$.
For any object $X$ of $Set$, we can take $A:=X$, $B:=X$ and $f:=Id_X$. $$\require{AMScd} \begin{CD} A:=X @>{a}>> A'\\ @V{f:=Id_X}VV @V{f'}VV \\ B:=X @>{b}>> B' \end{CD}$$ We have $\exists !(a:X\to A',b:X\to B'), f;b=a;f'$ which is, by Lemma 1, equivalent to $\exists !b:X\to B'$. So $B'$ is terminal in $Set$.
I tried to generalize this to all categories. Lemma 1 seems to be general and doesn't need any modification. In Theorem 1, the part that becomes hard is proving that $f'$ is an isomorphism. I assume I should prove that it's both monic and epic and then find a right-inverse (or a left-inverse) to prove it's an isomorphism but I wasn't able to do any of that.
So my question is: Is there a generalisation of Theorem 1 for all categories?
If yes, then I'd like to know the exact statement, and maybe a hint on the direction that I should take (including waiting to know more stuff if need be) but no proof (unless it's a hidden proof or a linked proof or any proof that I won't see until I want to).
If not, then I'd like to know if there is a generalisation for some categories (I assume there must be something to be done with algebra categories but I haven't looked into it yet). I'd also like to see an example where it fails (hidden or linked and with juste a hint in the question if it's an example one can find).
Thank you in advance.
If $C$ is any category with a terminal object $t$ and $I$ is a category, then it is an easy exercise ($\approx$ 2 lines) that $\Delta(t)$ (the constant functor with value $t$) is a terminal object in the functor category $C^I$. Any other terminal object of $C^I$ is isomorphic to this one. Now apply this to $I=\{0 < 1\}$.