Quotient Groups

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity, let $(G,\cdot)$ be a group and $N$ a normal subgroup of $G$; let $gN$ be the left coset of $N$ determined by $g\in G$, and $G/N$ the set of left cosets of $N$.

(i) Quotient group. The quotient group of $G$ by $N$ is the pair $(G/N,\ast)$, where $\ast$ is the unique binary operation on $G/N$ with

$$(gN)\ast(hN)=(g\cdot h)N\qquad\text{for all } g,h\in G,$$

given by The Product of Cosets of a Normal Subgroup Is Well Defined and Makes the Cosets a Group (i).

(ii) Canonical projection. The canonical projection of $G$ onto $G/N$ is the function $\pi:G\to G/N$ given by $\pi(g)=gN$.