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>-->
==Applications==
Topology:
* [[Factoring a continuous map through the projection of an equivalence relation induced by that map yields an injective continuous map|If {{M|f:X\rightarrow Y}} is a continuous map then factoring it through the projection of the equivalence relation it induces yields a continuous injection]] - topological version of this theorem almost exactly. We can extend this slightly in the case {{M|f:X\rightarrow Y}} is [[surjective]]:
** [[If a surjective continuous map is factored through the canonical projection of the equivalence relation induced by that map then the yielded map is a continuous bijection|If {{M|f:X\rightarrow Y}} is continuous ''and'' surjective then factoring it through the canonical projection of the equivalence relation it induces yields a continuous bijection]] - this is an extension of the previous statement, recall that when we take a surjection and apply {{link|passing-to-the-quotient|function}} we get surjection, we know from above it's injective. So now it's [[bijective]]
==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.-->Outline of proof method
# We must check the set up satisfies the requirements of the {{link|passing-to-the-quotient|function}} theorem (to yield {{M|\tilde{f}:\frac{X}{\sim}\rightarrow Y}}).
# We apply the theorem to get {{M|\tilde{f}:\frac{X}{\sim}\rightarrow Y}}.
# Next we must show {{M|\tilde{f}:\frac{X}{\sim}\rightarrow Y}} is [[injective]]
===Proof body===
{{Requires proof|grade=D|msg=Part 3 was the only non-trivial part. It is obvious that we can factor {{M|f}} through {{M|\pi}}, in fact:
* To do so requires that "{{M|f}} be constant on the {{plural|fibre|s}} of {{M|\pi}}", ie:
** {{M|1=\forall x,y\in X[\pi(x)=\pi(y)\implies f(x)=f(y)]}} (see [[Equivalent conditions to being constant on the fibres of a map]])
*** But if {{M|1=\pi(x)=\pi(y)}} then {{M|x\sim y}} and by definition {{M|1=x\sim y\iff f(x)=f(y)}}! Trivial!
Oh just FYI there's a commented out note and a requires-proof template at the top of the {{C|1===proof==}} heading, remove that later!}}
====Step 3====
We wish to show that {{M|\tilde{f}:\frac{X}{\sim}\rightarrow Y}} is [[injective]], ie: {{M|1=\forall a,b\in\frac{X}{\sim}[\tilde{f}(a)=\tilde{f}(b)\implies a=b]}}
* Let {{M|a,b\in\frac{X}{\sim} }} be given. 
** Suppose {{M|1=\tilde{f}(a)\ne\tilde{f}(b)}} then by the nature of [[logical implication]] we do not care whether or not {{M|1=a=b}}, either way it is true, we're done in this case.
** Suppose {{M|1=\tilde{f}(a)=\tilde{f}(b)}}, by the nature of logical implication we now require this leads to {{M|1=a=b}}
*** By the [[surjectivity]] of {{M|\pi:X\rightarrow\frac{X}{\sim} }} we see:
**** {{M|1=\exists x\in X[\pi(x)=a]}} and {{M|1=\exists y\in X[\pi(y)=b]}} 
***** Note that {{M|1=\tilde{f}(a)=\tilde{f}(\pi(x))}} and {{M|1=\tilde{f}(b)=\tilde{f}(\pi(y))}}, also by assumption we have {{M|1=\tilde{f}(a)=\tilde{f}(\pi(x))= \tilde{f}(\pi(y))=\tilde{f}(b)}}
***** Notice also that {{M|1=f(x)=\tilde{f}(\pi(x))}} and {{M|1=f(y)=\tilde{f}(\pi(y))}} (this is the whole point of {{M|\tilde{f} }}) 
****** So we see {{M|1=f(x)=\tilde{f}(a)=\tilde{f}(\pi(x))= \tilde{f}(\pi(y))=\tilde{f}(b)=f(y)}}, or importantly:
******* {{M|1=f(x)=f(y)}}
****** Recall that {{M|1=x\sim y\iff f(x)=f(y)}}, so now we know {{M|x\sim y}}
***** An elementary property of {{M|\pi:X\rightarrow\frac{X}{\sim} }} is that if {{M|x\sim y}} then {{M|1=\pi(x)=\pi(y)}}<ref group="Note">{{Todo|Link to statement, this ought to be mentioned somewhere explicit on this site!}}</ref><ref group="Note">{{Todo|This can be strengthened to {{M|\iff}} surely!}}</ref>
****** Explicitly, notice we have: {{M|1=\pi(x)=\pi(y)}}
***** Recall that {{M|1=a=\pi(x)}} and {{M|1=b=\pi(y)}} by definition of {{M|x}} and {{M|y}}, so:
****** {{M|1=a=\pi(x)=\pi(y)=b}} or more simply: {{M|1=a=b}}
*** We have shown that supposing {{M|1=f(a)=f(b)}} is given then {{M|1=a=b}}
** Both cases have been evaluated and the implication holds for both
* Since {{M|a,b\in\frac{X}{\sim} }} were arbitrary we have shown this for all {{M|a,b\in\frac{X}{\sim} }}

==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]]
* [[Factoring a continuous map through the projection of an equivalence relation induced by that map yields an injective continuous map]]
** [[If a surjective continuous map is factored through the canonical projection of the equivalence relation induced by that map then the yielded map is a continuous bijection]]
==Notes==
<references group="Note"/>
==References==
<references/>
{{Theorem Of|Elementary Set Theory|Abstract Algebra|Set Theory}}