Right-inverse characterization of the axiom of choice (source code)

= Right-inverse characterization of the axiom of choice

The statement that every <surjective function> has a <right inverse> is equivalent to the <axiom of choice>.

Given a <surjective function> $f:X\to Y$, each <fiber of a function> $f^{-1}(\{y\})$ is nonempty. The <axiom of choice> selects $g(y)$ from that fiber for every $y\in Y$, so $f(g(y))=y$ and $g$ is a <right inverse>. When $Y$ is the <empty set>, the unique <empty function> supplies $g$ without a choice.

Conversely, take an indexed family $(X_i)_{i\in I}$ of nonempty <sets>. The <projection map> from the disjoint <union> $D=\{(i,x):i\in I,\ x\in X_i\}$ to $I$ is <surjective>. A <right inverse> assigns $i\mapsto(i,x_i)$, selecting one $x_i\in X_i$ for every index. This is a <choice function>, so the asserted splitting of all <surjections> gives the <axiom of choice>.