View source for Factoring a function through the projection of an equivalence relation induced by that function yields an injection

{{Stub page|grade=A*|msg=Flesh out and demote}}
__TOC__
==Statement==
{{float-right|{{/Diagram}}}}Let {{M|X}} and {{M|Y}} be [[sets]], let {{M|f:X\rightarrow Y}} be any [[function]] between them, and let {{M|\sim\subseteq X\times X}} denote the ''[[equivalence relation]]'' [[equivalence relation induced by a function|induced by the function {{M|f}}]], recall that means:
* {{M|1=\forall x,x'\in X[x\sim x'\iff f(x)=f(x')]}}
Then we claim we can {{link|factor|function}}<ref group="Note">{{AKA}}: {{link|passing to the quotient|function}}</ref> {{M|f:X\rightarrow Y}} through {{M|\pi:X\rightarrow \frac{X}{\sim} }}<ref group="Note">the [[canonical projection of the equivalence relation]], given by {{M|\pi:x\mapsto [x]}} where {{M|[x]}} denotes the [[equivalence class]] containing {{M|x}}</ref> to {{underline|yield a unique [[injective]]}} map<ref>[[File:MondTop2016ex1.pdf]]</ref>:
* {{M|\tilde{f}:\frac{X}{\sim}\rightarrow Y}}
Furthermore, if {{M|f:X\rightarrow Y}} is [[surjective]] then {{M|\tilde{f}:\frac{X}{\sim}\rightarrow Y}} is not only [[injective]] but [[surjective]] to, that is: {{M|\tilde{f}:\frac{X}{\sim}\rightarrow Y}} is a [[bijection]]<ref group="Note">See "''[[If a surjective function is factored through the canonical projection of the equivalence relation induced by that function then the yielded function is a bijection]]''" for details</ref>.
<div style="clear:both;"></div>
==Proof==
{{Requires proof|grade=A*|msg=Do this now, just saving work}}
* Note to self - uniqueness comes from that we're [[factor (function)|factoring]] through a [[surjective]] map (namely, {{M|\pi}}), we only really have to show the result is injective.
==See also==
* [[If a surjective function is factored through the canonical projection of the equivalence relation induced by that function then the yielded function is a bijection]]
==Notes==
<references group="Note"/>
==References==
<references/>
{{Theorem Of|Elementary Set Theory|Abstract Algebra|Set Theory}}