Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Non-existence of a particular left adjoint

Jacques Carette (Dec 20 2023 at 16:35):

Consider the category where objects are pairs $\left(X, x\right)$ of a set $X$ and a point $x : X$, but where the morphisms are simply functions $f : X \rightarrow Y$, i.e. where there is no guarantee that the point is preserved. It is reasonable to call this the category of inhabited sets, $\mathsf{Inh}$.

There is an obvious forgetful functor $U : \mathsf{Inh} \rightarrow \mathsf{Set}$.

Conjecture: $U$ has no left adjoint. Alas, I have no proof. Various people have given "fly by" suggestions (left adjoints preserve colimits, so that ought to do it, and similar ideas that are too sparse on details) but I have been unable to turn these into actual proofs [where by actual proof, I'm eventually going to want to convince a proof assistant, so the bar is high!]

Can anyone help me with this conjecture? Preferably with enough detail that I can convince my favourite proof assistant that this is indeed a proof.

Nathanael Arkor (Dec 20 2023 at 16:42):

$\mathsf{Inh}$ has no initial object. However, since left adjoints preserve colimits, given a purported left adjoint $F : \mathsf{Set} \to \mathsf{Inh}$, we could construct an initial object $F(\varnothing)$, which is a contradiction.

Jacques Carette (Dec 20 2023 at 16:45):

That does seem like enough detail for me to convince Agda. I will indeed try. (I wonder if I'll now get stuck on 'has no initial object'. That would be funny.)

Nathanael Arkor (Dec 20 2023 at 16:48):

To clarify that point, for any inhabited set $X$, one can pick any set $Y$ with more than one element, and explicitly construct (at least) two different functions $X \to Y$, demonstrating that $X$ cannot be initial.