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?