# What's the category-theoretical existence proof, and name, for this morphism?

First, suppose that $i:K \hookrightarrow M$ is an insertion in some concrete category $\mathcal{C}$, and that we have some morphism $f:T \to M$ such that $f(T) \subseteq K \subseteq M$. It seems to me evident (from the standard definitions of function, subset, insertion, etc.) that there is a morphism $g:T \to K$ such that $i \circ g = f$, the only difference between $f$ and $g$ being that $\mathrm{cod}(f) = M$ while $\mathrm{cod}(g) = K$. But how does one prove the existence of $g$ categorically? (I imagine that the key to this lies in casting the definitions of insertion and $f(T) \subseteq K$ in categorical language.) How would the statement of the theorem have to be changed so that it holds for an arbitrary category? (E.g. I imagine that $i:K \to M$ would be described merely as a monomorphism, rather than an insertion.)

Second, what does one call a function like $g$, which differs from another function $f$ in codomain only? Is there a general category-theoretical name for the relationship between morphisms $g$ and $f$ in this example?

(This reminds me of how one gets a function $h|_Y$ by restricting the function $h$ to some subset $Y$ of $\mathrm{dom}(h)$. Here, instead, I want to "restrict" the codomain.)

Thanks!

PS: I have been studying a bit of CT in my spare time for some weeks: IOW, I'm a rank noob! I know what (co)products are, and have a very fuzzy understanding of pullbacks/pushouts and (co)limits...

-
Would you mind defining insertion and $\mathrm{cod}$? – Rasmus Aug 20 '11 at 10:07
Given a set $X$ and a subset $Y$ of $X$, the insertion (aka inclusion, aka immersion) of $Y$ is the restriction $I_X|_Y:Y \to X$ of the identity map of $X$ to $Y$. $\mathrm{cod}(f)$ means "codomain of $f$". – kjo Aug 20 '11 at 10:25
This follows from the faithfulness of the forgetfull functor of your concrete category. – Rasmus Aug 20 '11 at 10:33
@Rasmus: how could this categorical proof work in the case where $\mathcal{C}$ is $\mathbf{Set}$ (so the forgetful functor doesn't enter into the picture)? BTW, I have a vague idea of what functors are, and what the forgetful functor is, thanks to Wikipedia, though I have not really reached functors yet in my independent study... – kjo Aug 20 '11 at 10:38
Well, if $\mathcal C$ is the category of sets, then $g$ is just $f$, but regarded as a function to $K$ instead of $M$, which is possible since $f(T)\subseteq K$. – Rasmus Aug 20 '11 at 10:40

The concept you need is the image of an arrow $f : T \to M$. It is defined by the obvious universal property: a monomorphism $\operatorname{im} f : H \rightarrowtail M$ is the image of $f$ just if there is an arrow $c : T \to H$ such that $f = (\operatorname{im} f) \circ c$ and for every morphism $g : T \to K$ and every monomorphism $h : K \to M$ such that $f = h \circ g$, there is a (necessarily unique) arrow $k : H \to K$ such that $g = k \circ c$ and $\operatorname{im} f = h \circ k$.

Exercise. Show that $\operatorname{im} f$ is unique up to unique isomorphism.

The trouble is that $\operatorname{im} f$ as defined above is not guaranteed to exist unless the category is nice enough. This happens, for example, when the category is a topos or an abelian category.

Once we have $\operatorname{im} f$, it's clear how we may obtain $g : T \to K$ given $i : K \rightarrowtail M$ and the fact that we have a monomorphism $m: H \rightarrowtail K$ (i.e. the witness of the inclusion $H \subseteq K$) — we just take the composite $m \circ c$.

A related concept is that of the regular coimage. This makes sense in any category with finite limits and colimits. First, we take the pullback of $f$ along $f$ to obtain the kernel pair $p_1, p_2 : S \to T$. (For example, in the category of sets, $S = \{ (t_1, t_2) \in T \times T : f(t_1) = f(t_2) \}$.) The regular coimage of $f$ is the coequaliser $e : T \to H$ of $p_1$ and $p_2$. Notice that since $f \circ p_1 = f \circ p_2$, there must be an arrow $m : H \to M$ such that $f = m \circ e$. In any regular category (e.g. a topos or an abelian category) this $m$ will also be the image in the sense defined above.

I don't know of a name for the phenomenon where two arrows differ ‘only in the codomain’. But it's easy enough to formulate this categorically: this happens when the (regular) coimage of the two arrows are isomorphic.

-
Thanks! I'm still working through the details of your answer. What is the exact definition witness (as in "the witness of the inclusion $H \subseteq K$) in CT? I've consulted the indices of several books, but none mention this term. – kjo Aug 20 '11 at 12:38
It's a term from logic, which I am using informally. A ‘witness’ is a specific instance of a thing which is asserted to exist. For example, when we say $H \subseteq K$ in the ETCS, we are asserting that there is a monomorphism $H \rightarrowtail K$; so a witness is a specific such monomorphism. (Actually, this is an abuse of notation, because we're only supposed to write $m \subseteq K$ where $m$ is a monomorphism into $K$!) Or a more elementary example: $2$ is a witness to the assertion that $6$ is composite, because $2$ is a factor of $6$. – Zhen Lin Aug 20 '11 at 12:59