Injectivity for partially applied composition 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

*

*f is injective → Hom(S, f) is injective AND

*f is not injective → Hom(S, f) is not injective

Or we can prove

*

*Hom(S, f) is injective → f is injective AND

*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?

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$.
