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...
 A: 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.
