View source for Unique lifting property

__TOC__
==Statement==
Let {{Top.|X|J}} be a [[topological space]], suppose that {{Top.|E|H}} is a {{link|covering space|topology}} (with {{link|covering map|topology}} {{M|p:E\rightarrow X}}). Suppose {{Top.|Y|K}} is a [[connected topological space]] and {{M|f:Y\rightarrow X}} is a [[continuous map]], then{{rITTGG}}<sup>Partial:</sup>{{rITTMJML}}<sup> - </sup><ref group="Note">Lee defines covering maps and spaces a little differently. He requires that for {{link|evenly covered|topology}} that {{M|U}} be homeomorphic to each sheet, and each sheet is ''connected'' and disjoint from the others. Thus {{M|U}} is connected. It may not matter
* {{XXX|Does it?}}
But Gamelin and Green do not do this, so we can have coverings of not-connected neighbourhoods. It's worth investigating but it isn't critical to the theory.</ref>
* given two [[lift of a continuous map through a covering map|lifts of {{M|f}} through {{M|p}}]], say {{M|g,h:Y\rightarrow E}} we have:
** {{M|\big(\exists y\in Y[g(y)\eq h(y)\big)\implies \big(\ \underbrace{\forall y\in Y[g(y)\eq h(y)]}_{\text{i.e. that }g\eq h}\ \big)}}
*** In words: if there exists a point on which {{M|g}} and {{M|h}} agree then {{M|g}} and {{M|h}} are [[equal as functions]]
===Bonus corollary===
Recall that a [[logical implication]] is [[logically equivalent]] to the [[contrapositive]], that is
* {{M|(A\implies B)\iff(\neg B\implies\neg A)}}
So, should the above claim be true, we also get:
* {{M|\big(\exists y\in Y[g(y)\neq h(y)]\big)\implies\big(\forall y\in Y[g(y)\neq h(y)]\big)}}
** In words: if there exists a {{M|y_0\in Y}} such that {{M|g}} and {{M|h}} disagree at {{M|y_0}} then they disagree everywhere. 
*** {{Caveat|This does not mean {{M|g(Y)\cap h(Y)\eq\emptyset}} necessarily!}}
==Proof==
{{Requires work|grade=C|msg={{Warning|What follows is VERY messy.}} I was distracted when writing it and kept switching between it and something else. However the written proof was BARELY legible so this is better than nothing. Hopefully}}
{{XXX|It'd be good to put some reasoning here. Like given a {{M|z\in Y}} to show {{M|g}} and {{M|h}} agree there we really need to work in terms of [[open neighbourhoods]] to {{M|z}}, which we can get from somewhere they're known to agree on. However this only works if it's connected, as if {{M|z}} is in another connected components "stuff just doesn't work" <--make this more formal}}


Let us make the following definitions:
* {{M|S:\eq\{y\in Y\ \vert\ h(y)\eq g(y)\} }} (when we introduce the hypothesis, by that hypothesis this will be [[non-empty]])
* {{M|T:\eq\{y\in Y\ \vert\ h(y)\neq g(y)\} }}

'''Lemma 1: ''' {{M|S}} and {{M|T}} are [[disjoint]].
* Suppose {{M|S\cap T\neq\emptyset}}, clearly this {{M|iff\exists z\in S\cap T}}
** Suppose there is such a {{M|z\in S\cap T}}, by definition of [[intersection]] that means {{M|\exists z\in Y[z\in S\wedge z\in T]}}
*** {{M|z\in S\iff g(z)\eq h(z)}} and {{M|z\in T\iff g(z)\neq h(z)}}
**** We see {{M|g(z)\eq h(z)\neq g(z)}} so {{M|g(z)\neq g(z)}} - a contradiction!
* We see there cannot be any elements in {{M|S\cap T}} for if there was we have a contradiction. As shown
* So {{M|S\cap T\eq\emptyset}} - {{ie}} {{M|S}} and {{M|T}} are [[disjoint]]


'''Lemma 2: ''' {{M|S\cup T\eq Y}} AND {{M|S\eq Y-T}} (and {{M|T\eq Y-S}}) in some form. We need {{M|S\eq Y-T}} and {{M|T\eq Y-S}} at least!
{{XXX|Todo}}


As {{M|Y}} is a [[connected topological space]] we see that the ''only'' sets that are both [[open sets|open]] and [[closed set|closed]] are {{M|Y}} itself and {{M|\emptyset}}, if the result holds (which we very much hope it does) then {{M|S\eq Y}} and {{M|T\eq\emptyset}}, so if we show {{M|S}} is open. As {{M|T\eq Y-S}} we would see {{M|T}} is closed as a result.

If we show {{M|T}} is open too, then {{M|S}} would be closed, thus showing they're both open and closed!

So we must have {{M|S\eq Y}} (as {{M|S}} is non-empty by hypothesis) and {{M|T\eq\emptyset}}, but if {{M|S\eq Y}} then they agree everywhere!

: {{XXX|[[Notes:Covering spaces]] shows it better}}

===Proof that {{M|S}} is open===
* Let {{M|s\in S}} be given. There is at least one to give by hypothesis. We must find a [[neighbourhood]] of {{M|s}} that is fully contained in {{M|S}}, recall that ''[[a set is open if and only if it is a neighbourhood to all of its points]]'', this is what we hope to show. 
** Define {{M|r:\eq h(s)\eq g(s)}} and notice {{M|r\in E}}
*** Define {{M|z:\eq p(r)}} and notice {{M|p(r)\in X}}
**** As {{M|z\in X}} and {{M|p}} is a {{link|covering map|topology}} there exists an [[open neighbourhood]], {{M|U\in\mathcal{J} }} of {{M|z}} such that {{M|U}} is {{link|evenly covered|topology}} by {{M|p}}
**** Choose {{M|U}} to be such an [[open neighbourhood]]
***** By choice of {{M|U}} we see {{M|\exists(V_\alpha)_{\alpha\in I}\subseteq\mathcal{H} }} 
****** such that:
******# {{M|p^{-1}(U)\eq\bigcup_{\alpha\in I}V_\alpha}}
******# The {{M|(V_\alpha)_\alpha}} are open (given by being in {{M|\mathcal{H} }})
******# The {{M|(V_\alpha)_\alpha}} are [[pairwise disjoint]]
******# For each {{M|V_\beta\in(V_\alpha)_\alpha}} we have {{M|V_\beta\cong_{p\vert^\text{Im}_{V_\beta} } U}}, that is the covering map [[restricted to its image]] on {{M|V_\beta}} is a [[homeomorphism]] onto {{M|U}}
***** Choose {{M|(V_\alpha)_{\alpha\in I}\subseteq\mathcal{H} }} to be this family of {{link|sheets of the covering|topology}}
****** As {{M|z\in U}} we see {{M|p^{-1}(z)\subseteq p^{-1}(U)}}
****** As {{M|z:\eq p(r)}} we see that {{M|r\in p^{-1}(z) }} so {{M|r\in p^{-1}(U)}}
****** As {{M|p^{-1}(U)\eq\bigcup_{\alpha\in I}V_\alpha}} we see {{M|r\in \bigcup_{\alpha\in I}V_\alpha}}, by definition of [[union]]:
******* {{M|\big(r\in \bigcup_{\alpha\in I}V_\alpha\big)\iff\big(\exists\beta\in I[r\in V_\beta\big)}}
****** So {{M|\exists\beta\in I[r\in V_\beta]}}
******* Define {{M|V:\eq V_\beta}} where {{M|V_\beta}} is the element of {{M|(V_\alpha)_{\alpha\in I} }} with {{M|r\in V_\beta}} as discussed above
******** As {{M|r:\eq h(s)}} and {{M|h(s)\eq g(s)}} we see that:
********* {{M|r\in V\iff[h(s)\in V\wedge g(s)\in V]}}
******** So {{M|s\in h^{-1}(V)}} and {{M|s\in g^{-1}(V)}}
********* Notice, by [[continuity]] and {{M|V}} being [[open set|open]] in {{Top.|E|H}} that {{M|h^{-1}(V)}} and {{M|g^{-1}(V)}} are both [[open set|open]] in {{Top.|Y|K}}.
******** Thus {{M|s\in h^{-1}(V)\cap g^{-1}(V)}} (as by definition of [[intersection]] {{M|(s\in A\cap B)\iff(s\in A\wedge s\in B)}} - we have the RHS, so we have the left.
********* Define {{M|W:\eq h^{-1}(V)\cap g^{-1}(V)}}, so {{M|W\subseteq Y}}
********** notice:
**********# that {{M|W}} is [[open set|open]] in {{Top.|Y|K}} as by definition of a [[topology]] the intersection of open sets is open.
**********# {{M|W\neq\emptyset}} ({{M|W}} is non-empty) as - at least - {{M|s\in W}}
********** Define {{M|q:\eq p\vert_V^\text{Im}:V\rightarrow U}} be the [[homeomorphism]] of the restriction of {{M|p}} to {{M|V}} which is onto {{M|U}}. 
*********** This means that {{M|q}} is [[injective]], {{ie}}:
************ {{M|\forall v,w\in V[q(v)\eq q(w)\implies v\eq w]}} 
*********** Notice also that {{M|h(W)\subseteq V}} and {{M|g(W)\subseteq V}}
*********** Let {{M|w\in W}} be given
************ By definition of being lifts: {{M|f(w)\eq p(h(w))\eq p(g(w))}}
************ As {{M|h(w)\in V}} and {{M|g(w)\in V}} we see that {{M|p(h(w))\eq q(w)}} and {{M|p(g(w))\eq q(g(w))}}
************* So {{M|f(w)\eq q(h(w))\eq q(g(w))}}
************** But {{M|q}} is injective, so {{M|q(h(w))\eq q(g(w))\implies g(w)\eq h(w)}}
************ so we have {{M|g(w)\eq h(w)}}
************* so {{M|w\in S}} (by definition of {{M|S}})
*********** Since {{M|w\in W}} was arbitrary we have shown {{M|\forall w\in W[w\in S]}}
********* Thus {{M|W\subseteq Y}}, that is {{M|Y}} contains a [[neighbourhood]] of {{M|s}}
* Since {{M|s\in S}} was arbitrary, we have shown {{M|\forall s\in S\exists W\in\mathcal{K}[x\in W\wedge W\subseteq Y]}}
** In words: that for all points in {{M|S}} there is a neighbourhood to that point contained entirely in {{M|S}}
Thus {{M|S}} is [[open set|open]], as required.

{{Requires proof|We still need to show {{M|T}} is open|grade=A}}
==Notes==
<references group="Note"/>
==References==
<references/>
{{Theorem Of|Algebraic Topology|Topology|Homotopy Theory}}