Why don't you need the Axiom of Choice when constructing the "inverse" of an injection?

Suppose $f:X\rightarrow Y$ is a surjection and you want to show that there exists $g:Y\rightarrow X$ s.t. $f\circ g=\mathrm{id}_Y$. You need the AC to show this.

However, suppose $f$ is a injection and you want show there is $g$ s.t. $g\circ f=\mathrm{id}_X$. Then, according to my textbook, you don't need the AC to show this.

This is counterintuitive to me, because it's like you need a special axiom to claim that an infinite product of big sets is nonempty, while you don't need one to claim that an infinite product of singleton sets is nonempty, which seems smaller than the former.

So why don't you need the AC to show the latter?

EDIT: $X$ should be nonempty.

EDIT 2: I realized (after asking this) that my question mostly concerns whether the AC is needed to say that an infinite product of finite sets is nonempty, and why.

Solution 1:

The need for the axiom of choice is to choose arbitrary elements. Injectivity eliminates this need.

Assume that $A$ is not empty, if $f\colon A\to B$ is injective this means that if $b\in B$ is in the range of $f$ then there is a unique $a\in A$ such that $f(a)=b$.

This means that we can define (from $f$) what is the $a$ to which we send $b$.

So if $f$ is not onto $B$ we have two options:

1. $b\in B$ in the range of $f$, then we have exactly one option to send $b$ to.
2. $b\in B$ not in the range of $f$. Since $A$ is not empty fix in advance some $a_0\in A$ and send $b$ to $a_0$.

Another way to see this is let $B=B'\cup Rng(f)$, where $B'\cap Rng(f)=\varnothing$. Fix $a_0\in A$ and define $g|_{B'}(x)=a_0$. For every $b\in Rng(f)$ we have that $f^{-1}[\{b\}]=\{a\in A\mid f(a)=b\}$ is a singleton, so there is only one function which we can define in: $$\prod_{b\in Rng(f)}f^{-1}[\{b\}]$$

Now let the unique function in the product be $g|_{Rng(f)}$ and define $g$ to be the union of these two.

Your intuition about the need for the axiom of choice is true for surjections, if $f$ was surjective then we only know that $f^{-1}[\{b\}]$ is non-empty for every $b\in B$, and we need the full power of the axiom of choice to ensure that an arbitrary surjection has an inverse function.

To the edited question:

The axiom of choice is needed because we have models in which the axiom of choice does not hold, where there exists an infinite family of pairs whose product is empty.

There are weaker forms from which follow choice principles for finite sets. However these are still not provable from ZF on its own.

As indicated by Chris Eagle in the comments, and as I remark above, in a product of singletons there is no need for the axiom of choice since there is only one way to choose from a singleton.

Further reading:

1. Finite choice without AC
2. axiom of choice: cardinality of general disjoint union