Is the Axiom of Choice implicitly used when defining a binary operation on a quotient object?

Let's say you have a group $(G,\cdot)$ and you have a normal subgroup $N$ (note we are considering this only as a set). And now we want to define a binary operation $\star$ on $G/N$ such that $(G/N, \star)$ is a group. Every element of $G/N$ looks like $aN$ for some $a\in G$. Thus it seems perfectly natural to want to exploit the group-theoretic structure of the elements of the cosets and define $aN\star bN:= a\cdot bN$.

Most textbooks do this and then they quickly turn around and prove this operation is well-defined. I understand all of this and why they do it, but doesn't this construct pre-suppose a choice function on $G/N$?

It seems to me that the definition of the binary operation $\star$ is a quick abbreviation of all of this: let $f$ be a choice function for $G/N$. Then for all $A$ and $B$ in $G/N$ define $A\star B:= (f(A)\cdot f(B))N$. And the usual well-defined check follows up to show that this operation does not depend on the choice-function $f$, shows that this operation is associative, and has an identity.

But the independence of the choice-function does not excuse the need for the existence of a choice function. And we are not always guaranteed a choice function (in AC's absence). It bothers that we appear to need an extremely strong principle for something so fundamental but trivial in Group Theory. (Of course, there is a similar problem with rings and ideals in Ring Theory)

I have a couple questions. Is my supposition correct? That is, in the usual construction of the quotient operation, is there an assumption of a choice-function? If that is the case, could we---at the cost of being long-winded and perhaps tedious---define a quotient operation that does not presuppose a choice function?

Solution 1:

You can avoid the choice function altogether by defining $A\cdot B=\{\,ab\mid a\in A, b\in B\,\}$ where $A,B$ are subsets of $G$ that happen to be of the form $aN=\{\,an\mid n\in N\,\}$ for some $a\in G$, but we really just use Replacement here, no choice.

To see all the settheoretic details for defining $G/N$ and verify that Choice is not invoked, use Powerset and Comprehension (and lesser sins) to define $$G/N:=\{\,A\in\mathcal P(G)\mid A\ne\emptyset, \forall a,b\in A\colon a^{-1}b\in N\,\}$$ and Replacement as above or Comprehension as in $$ A\cdot B:=\{\,g\in G\mid \exists a\in A, b\in B\colon g=ab\,\}$$ for multiplication.

Solution 2:

If you wanted to make a single once-for-all selection of coset representatives, then, in general, you would need to use the axiom of choice to create a choice function. However, when defining the product in $G/N$, you just need to pick representatives for two cosets at a time. You can forget about the representatives once you've computed the product of the cosets. That is, suppose we pick two cosets $A$ and $B$. We then define $C$ to be the unique coset in $G/N$ such that whenever $A = aN$ and $B = bN$, then $C = (ab)N$. We can prove the existence and uniqueness of such a $C$ without appealing to the axiom of choice. Finally, we define the product on $G/N$ by declaring, for any cosets $A$ and $B$, that $AB$ is the coset $C$ determined as above.