I've been struggling to understand how the surjection of a function $f : X \rightarrow Y$ implies that it has a right inverse. My questions basically reside on the application of the axiom of choice to the proof.
First question: The axiom of choice states that, for any set $Y$, if $\varnothing \not\in Y$, then there exists a function $g : Y \rightarrow \bigcup_{y\in Y} X_y$. such that $\forall y \in Y g(y)\in X_y$. Why, if $f : X \rightarrow Y$ is surjective, $\varnothing \not\in Y$? I can't find my way on this one.
Second question: As far as I understand, $\bigcup_{y\in Y} X_y$ represents the union of a family of the sets $X_y$ indexed by the elements $y\in Y$. Hence, $\bigcup_{y\in Y} X_y$ is equal to $\{x : \exists y \in Y (x\in X_y)\}$. If $X_y$ is defined as $\{x\in X : y=f(x)\}$, then $\{x : \exists y\in Y (x\in X_y)\}$ is equal to $\{x : \exists y[y\in Y \land x\in X \land y=f(x)]\}$, which is the same as $\{x \in X : f(x) \in Y\}$. The set $\{x \in X : f(x) \in Y\}$ is equal to the inverse image $g[Y]$, which is equal to $X$, since $f : X \rightarrow Y$. Hence, $\bigcup_{y\in Y} X_y$ is equal to $X$ and $g : Y \rightarrow \bigcup_{y\in Y} X_y$ is equivalent to $g : Y \rightarrow X$. Is this correct?
Third question: If we define $X_y$ as being equal to $\{x\in X : y=f(x)\}$, then $\forall y\in Y g(y)\in X_y$ is equivalent to $\forall y \in Y g(y)\in X \land y=f(g(y))$. Is this also correct?
If my (incomlete) proof attempt is correct, the axiom of choice $g : Y \rightarrow \bigcup_{y\in Y} X_y$. such that $\forall y \in Y g(y)\in X_y$, considering $X_y$ equal to $\{x\in X : y=f(x)\}$, could be rewritten as $g : Y \rightarrow X$, such that $\forall y \in Y \hspace{0.5em} g(y)\in X \land y=f(g(y))$, which concludes our proof.
I apologize for the basic questions, but this all seems very confusing for me.
Your statement of the Axiom of Choice is unclear, because you never explain what $ X _ y $ is. There are two ways to fix this (and if you're going through a course or a textbook, then you should probably find out which version of AC they're using):
I'll call these two versions AC1 and AC2.
First question: There is no reason why $ \varnothing \notin Y $. If you use AC1, then the $ Y $ in your hypothesis is not the same as the $ Y $ in AC. Instead of $ Y $, you have to use $ \{ A \subseteq X \; | \; \exists \, y \in Y , \; A = f ^ * [ \{ y \} ] \} $, the set of all preimages under $ f $ of elements of $ Y $. These preimages are all nonempty, because $ f $ is surjective. On the other hand, if you use AC2, then they are the same $ Y $, but you don't need $ \varnothing \notin Y $ but rather $ X _ y \ne \varnothing $, and this is the case if $ X _ y : = f ^ * [ \{ y \} ] $, which is nonempty because $ f $ is surjective.
For the other two questions, your development seems correct, but notice that you're using AC2. So you'll need to rewrite this a bit if you want to use AC1.