Theorem: Condition for Existence of Epimorphism from Quotient Structure to Epimorphic Image

Let $\struct {A, \odot}$ and $\struct {B, \otimes}$ be algebraic structures.
Let $\RR$ be a congruence relation on $\struct {A, \odot}$.
Let $f: \struct {A, \odot} \to \struct {B, \otimes}$ be an epimorphism.
Let $\struct {A / \RR, \odot_\RR}$ denote the quotient structure defined by $\RR$.
Let $q_\RR: A \to A / \RR$ denote the quotient mapping induced by $\RR$:
:$\forall x \in A: \map {q_\RR} x = \eqclass x \RR$
where $\eqclass x \RR$ denotes the equivalence class of $x$ under $\RR$.
Then:
:there exists an epimorphism $g$ from $\struct {A / \RR, \odot_\RR}$ to $\struct {B, \otimes}$ which satisfies $g \circ q_\RR = f$
{{iff}}:
:$\RR \subseteq \RR_f$
where $\RR_f$ denotes the equivalence relation induced by $f$.

Proof:
=== Necessary Condition ===
Let $\RR \subseteq \RR_f$.
Recall the definition of $\RR_f$:
:$\forall x, y \in A: x \mathrel {\RR_f} y \iff \map f x = \map f y$ 
Let us define $g: \struct {A / \RR, \odot_\RR} \to \struct {B, \otimes}$ as:
:$\forall \eqclass x \RR \in A / \RR: \map g {\eqclass x \RR} = \map f x$
We show that $g$ is well-defined.
Let $x \mathrel \RR y$.
Then as $\RR \subseteq \RR_f$, it follows that:
:$x \mathrel {\RR_f} y$
By definition of the equivalence class of $x$:
:$\eqclass x \RR = \eqclass y \RR$
Thus:
{{begin-eqn}}
{{eqn | l = \map g {\eqclass x \RR}
      | r = \map f x
      | c = Definition of $g$
}}
{{eqn | r = \map f y
      | c = as $x \mathrel {\RR_f} y$
}}
{{eqn | r = \map g {\eqclass y \RR}
      | c = Definition of $g$
}}
{{end-eqn}}
Thus we have that:
:$\forall x, y \in A: x \mathrel \RR y \implies \map g {\eqclass x \RR} = \map g {\eqclass y \RR}$
and so $g$ is well-defined.
Then:
{{begin-eqn}}
{{eqn | q = \forall x \in A
      | l = \map {g \circ q_R} x
      | r = \map g {\map {q_R} x}
      | c = {{Defof|Composition of Mappings}}
}}
{{eqn | r = \map g {\eqclass x \RR}
      | c = {{Defof|Quotient Mapping}}
}}
{{eqn | r = \map f x
      | c = Definition of $g$
}}
{{end-eqn}}
and so we have that:
:$g \circ q_\RR = f$
Let $x, y \in A$.
We have:
{{begin-eqn}}
{{eqn | l = \map g {\eqclass x \RR \odot_\RR \eqclass y \RR}
      | r = \map g {\eqclass {x \odot y} \RR}
      | c = Quotient Structure is Well-Defined
}}
{{eqn | r = \map f {x \odot y}
      | c = Definition of $g$
}}
{{eqn | r = \map f x \otimes \map f y
      | c = $f$ is an epimorphism
}}
{{eqn | r = \map g {\eqclass x \RR} \otimes \map g {\eqclass y \RR}
      | c = Definition of $g$: {{apriori}} $g$ is well-defined
}}
{{end-eqn}}
Thus we see that $g$ is a homomorphism.
We have {{hypothesis}} that $g \circ q_\RR = f$ is an epimorphism.
Hence {{afortiori}} $g \circ q_\RR$ is a surjection.
So from Surjection if Composite is Surjection we have that $g$ is likewise a surjection.
Thus we have that $g$ is a surjective homomorphism.
Hence by definition $g$ is an epimorphism.
We note that if it is not the case that $\RR \subseteq \RR_f$, then there exist $\tuple {x, y} \in \RR$ such that $\map f x \ne \map f y$.
In that case we would see that while $x \mathrel y$ we would have that:
:$\map g {\eqclass x \RR} \ne \map g {\eqclass y \RR}$
meaning that $g$ is not a well-defined mapping.
So, in summary, given that $\RR \subseteq \RR_f$, we have demonstrated the existence of an epimorphism $g$ which satisfies $g \circ q_\RR = f$.
{{qed|lemma}}