Injectivity for partially applied composition

Question

I struggle to understand the following theorem (not the proof, I can't even validate it to be true). Note: I don't have a math background.

If S is not the empty set, then (f : T → V) is injective if and only if Hom(S, f) is injective.

Hom(S, f) : Hom(S, T) → Hom(T, V)

As I understand, to prove

f is injective ↔ Hom(S, f) is injective

we can go two ways. We can either prove

1. f is injective → Hom(S, f) is injective AND
2. f is not injective → Hom(S, f) is not injective

Or we can prove

1. Hom(S, f) is injective → f is injective AND
2. Hom(S, f) is not injective → f is not injective

Both ways should give the same result, because biconditional is symmetric, right?!

Then I draw the following diagram:

where I see f as injective but HOM(S, f) as not!

Where I'm wrong? How to visualize HOM(S, f) correctly?

Answer 1

The claim is perfectly correct. Your diagram misinterprets $Hom(S,f)$. To say $Hom(S,f):Hom(S,T)\to Hom(S,V)$ is noninjective is to say there are maps $a,b:S\to T$ such that $a\neq b$ but $f\circ a=f\circ b$. Since $a\neq b$, there exists $s\in S$ with $a(s)\neq b(s)$. But since $f\circ a=f\circ b$, we have $f(a(s))=f(b(s))).$ That shows $f$ is not injective. The converse is easier: set $S$ to be a 1-point set. Then $Hom(S,f)$ is sent to $f$ under the natural isomorphism $Hom(S,T)\cong T, Hom(S,V)\cong V$, so the injectivity of the one implies that of the other.

Note that your diagram tries to interpret $Hom(S,f)$ as a map $Hom(S,T)\to Hom(T,V)$. But there is no map of that form induced by $f$.

Answer 2

I don’t understand how it defines the map $Hom(S,f)$. From the choice of your symbols (which refers to category theory because you are fixed the set category in which the objects are sets and the morfism are the function between these sets) I think that $Hom(S,f)$ is defined from $Hom(S,T)$ to $Hom(S,V)$ and it maps every $p\in Hom(S,T)$ to $f\circ p$. In this case if for every non-empty set $S$ the map $Hom(S,f)$ is infective than you have that $f$ is injective. (This result characterize the the class of monomorphism in the category sets as the class of injective map)