View source for Passing to the quotient (function)

==Definition==
Given a function, {{M|f:X\rightarrow Y}} and another function, {{M|w:X\rightarrow W}} (I have chosen {{M|W}} to mean "whatever") we can say:
: '''{{M|f}} may be factored through {{M|w}}'''
if {{M|f}} and {{M|w}} are such that:
* <math>\forall x,y\in X[w(x)=w(y)\implies f(x)=f(y)]</math> 
*: (this is the same as: <math>\forall x,y\in X[f(x)\ne f(y)\implies w(x)\ne w(y)]</math>)
Then {{M|f}} ''induces'' a function, {{M|\tilde{f} }} such that <math>f=\tilde{f}\circ w</math>, or more simply that the following [[Commutative diagram|diagram commutes]]:
{| class="wikitable" border="1"
|-
| style="font-size:1.5em;" | <math>
\begin{xy}
\xymatrix{
X \ar[r]^w \ar[dr]_f & W \ar@{.>}[d]^{\tilde{f}}\\
 & Y
}
\end{xy}
</math>
|-
! Diagram
|}
Note:
# {{M|\tilde{f} }} may be explicitly written as {{M|\tilde{f}:W\rightarrow Y}} by {{M|\tilde{f}:v\mapsto f(w^{-1}(v))}}
#* Or indeed {{M|1=\tilde{f}:=f\circ w^{-1} }}
#* This is actually an abuse of notation as {{M|w^{-1}(x\in W)}} is a subset of {{M|X}}, however it is safe to use it because (as is proved below) {{M|f}} of any element of {{M|w^{-1}(x\in W)}} for a given {{M|x}} is the same. 
# The function {{M|\tilde{f} }} is unique if {{M|w}} is [[Surjection|surjective]]
===Points to remember===
* Remembering the requirements:
*: We want to induce a function {{M|\tilde{f}:W\rightarrow Y}} - if {{M|1=w(x)=w(y)}} then {{M|1=\tilde{f}(w(x))=\tilde{f}(w(y))}} just by composition. 
*: If {{M|1=f(x)\ne f(y)}} we're screwed in this case. So it is easy to see that we must have {{M|1=[w(x)=w(y)]\implies[f(x)=f(y)]}} otherwise we cannot proceed.
==Proof of claims==
{{Begin Theorem}}
Claim: the induced function, {{M|\tilde{f} }} exists and is given unambiguously by {{M|\tilde{f}:v\mapsto f(w^{-1}(v))}}
{{Begin Proof}}
'''Existence'''
: Let {{M|\tilde{f}:W\rightarrow Y}} be given by: {{M|f:v\mapsto f(w^{-1}(v))}} - I need to prove this is a [[Function]]
:: This means I must check it is well defined, a function must associate each point in its domain with exactly 1 element of its codomain
::: Let {{M|v\in W}} be given
:::: Let {{M|a\in w^{-1}(v)}} be given
::::: Let {{M|b\in w^{-1}(v)}} be given
:::::: We know <math>\forall a\in w^{-1}(v)</math> that <math>w(a)=v</math> by definition of <math>w^{-1}</math>
:::::: This means <math>w(a)=w(b)</math>
::::::: But by hypothesis <math>w(a)=w(b)\implies f(a)=f(b)</math>
:::::: So <math>f(a)=f(b)</math>
::::: Thus given an {{M|a\in w^{-1}(v)}}, <math>\forall b\in w^{-1}[f(a)=f(b)]</math>
:::: We now know (formally) that: (given a {{M|v}}) <math>\exists y\in Y\forall a\in w^{-1}(v)[f(a)=y]</math> - notice the <math>\exists y</math> comes first. We can uniquely define <math>f(w^{-1}(v))</math>
::: Since {{M|v\in W}} was arbitrary we know <math>\forall v\in W\exists y\in Y\forall a\in w^{-1}(v)[f(a)=y]</math>
:: We have now shown that <math>\tilde{f}</math> can be well defined (as the function that maps a {{M|v\in W}} to a {{M|y\in Y}}.
:: To calculate <math>\tilde{f}(v)</math> we may choose any <math>a\in w^{-1}(v)</math> and define <math>\tilde{f}(v)=f(a)</math> - we know <math>f(a)</math> is the same for whichever <math>a\in w^{-1}(v)</math> we choose.
: So we know the function <math>\tilde{f}:W\rightarrow Y</math> given by <math>\tilde{f}:x\mapsto f(w^{-1}(x))</math> exists


This completes the proof<ref name="Alec">This is my (Alec's) own work</ref>
{{End Proof}}{{End Theorem}}
{{Begin Theorem}}
Claim: if {{M|w}} is surjective then the induced {{M|\tilde{f} }} is unique
{{Begin Proof}}
'''Uniqueness'''
: Suppose another function exists, <math>\tilde{f}':W\rightarrow Y</math> that isn't the same as <math>\tilde{f}:W\rightarrow Y</math>
:: That means <math>\exists u\in W:[\tilde{f}(u)\ne\tilde{f}'(u)]</math>
::* Note, as {{M|w:X\rightarrow W}} is [[surjective]], that {{M|1=\exists x'\in X[w(x')=u]}}
:: However for both {{M|\tilde{f} }} and {{M|\tilde{f}'}} we have the property of <math>f=\tilde{f}\circ w=\tilde{f}'\circ w</math> so:
::: By hypothesis we have: {{M|1=\forall x\in X[f(x)=\tilde{f}(w(x))=\tilde{f}'(w(x))]}} however we know:
:::* {{M|1=\exists x'\in X[w(x')=u]}} and {{M|1=\tilde{f}(u)\ne \tilde{f}'(u)}}, this means:
:::** {{M|1=f(x')=\tilde{f}(w(x'))\ne\tilde{f}'(w(x'))}} - which contradicts the hypothesis.
:: However if {{M|w}} is not surjective, then the parts of the domain on which {{M|\tilde{f} }} and {{M|\tilde{f}'}} disagree on may never actually come up; that is to say:
::* {{M|1=\forall x\in X[\tilde{f}(w(x))=\tilde{f}'(w(x))]}} as {{m|w:X\rightarrow W}} may never take an {{M|x\in X}} to a {{M|z\in W}} where {{M|\tilde{f}(z)}} and {{M|\tilde{f}'(z)}} differ; ''but'' they could still be different functions. 


This completes the proof<ref name="Alec"/>

: '''Notes:'''
:# Notice that if {{M|w}} is not surjective, the point(s) on which {{M|\tilde{f} }} and {{M|\tilde{f}'}} disagree on may never actually come up, so it is indeed not-unique if {{M|w}} isn't surjective. 
{{End Proof}}
{{End Theorem}}
==References==
<references/>
{{Definition|Abstract Algebra}}