Injectivity not required for unification algorithms?
Here $f$ is not a mathematical function.  Rather, it is a function symbol.  Don't think of $f(a,b)$ as the result of evaluating the function at parameters $a,b$.  Rather, think of it as a term in a symbolic expression -- it is a syntactic object that is not intended to be interpreted in the way you are interpreting it.

If you like, you can think of it as though every function symbol in a symbolic expression is an injective function; but that's not really accurate, that's just a crude way to think about symbolic expressions.

You can't define $f(x)=x+y$.  $f$ is an uninterpreted function symbol.  You're not allowed to define a particular function.  Rather, $f$ is a stand-in for a function that is not yet defined. One way to think about it is that any conclusions that you draw from unification, are conclusions that should hold for all functions $f$ (not just a single one).