View source for Homotopy invariance of loop concatenation

{{Stub page|grade=A*|msg=Stub page, chore to write, probably needs redoing}}
: '''Note: ''' the homotopy in the title means [[homotopy]] {{M|\text{rel }\{0,1\} 
Marked as A* because I wrote it in such a bored mood, it needs to be checked ASAP}}
__TOC__
==Statement==
Here {{M|1=I:=[0,1]:=\{x\in\mathbb{R}\ \vert\ 0\le x\le 1\}\subset\mathbb{R} }} will denote the [[closed unit interval]]. Let {{M|Top.|X|J}} and {{Top.|Y|K}} be [[topological spaces]], let {{M|b\in X}} be given and let {{nowrap|1={{M|\ell_1,\ell_2,\ell_1',\ell_2'\in}}[[Omega(X,b)|{{M|\Omega(X,b)}}]]<ref group="Note">Recall that [[Omega(X,b)|{{M|\Omega(X,b)}} is a [[subset of|subset]] of {{C(I,X)}}, and {{M|C(I,X)}} is the set of all {{link|path|topology|s}} in {{M|X}}. {{M|\Omega(X,b)}} is the set of all ''{{link|loop|s}}'' in {{M|X}} ''based at'' {{M|b\in X}}. That means if {{M|\ell\in\Omega(X,b)}} that {{M|\ell:I\rightarrow X}} is a path and {{M|1=\ell(0)=\ell(1)=b}}.<br/><br/>Furthermore, {{M|\Omega(X,b)}} is not just a [[set]], it does have a [[group]] structure we can imbue on it, called [[the fundamental group]]. This page is actually an important step in the process.</ref>}}, then<sup>[[Corollary]] to 7.10:</sup>{{rITTMJML}} we have:<!--
--------------------------------------
Statement first paragraph ends HERE
-------------------------------------
-->
* If {{M|H_1:\ \ell_1\simeq\ell_1'\ (\text{rel }\{0,1\})}} and {{M|H_2:\ \ell_2\simeq\ell_2'\ (\text{rel }\{0,1\})}}<ref group="Note">Recall that means {{M|H_1}} is a [[homotopy]] between {{M|\ell_1}} and {{M|\ell_2}} that is relative to {{M|\{0,1\} }} or stationary on {{M|\{0,1\} }}. We may say {{M|\ell_1}} is ''[[homotopic]]'' to {{M|\ell_2}} (rel {{M|\{0,1\} }})
* In this case we have [[loop homotopy/homotopic|loop homotopies]], an instance of [[end point preserving homotopy/homotopic]] maps</ref>
Then
* {{M|1=H:\ \ell_1*\ell_2\simeq\ell_1'*\ell_2'\ (\text{rel }\{0,1\})}} - {{M|*}} is the operation of [[loop concatenation]], an instance of [[path concatenation (topology)|path concatenation]]
This can perhaps be better written symbolically using {{M|[\ell]}} to denote the [[equivalence class]] of {{M|\ell}} under (equivalence) [[relation]] of [[end point preseriving homotopy]]:
* {{M|1=\forall\ell_1,\ell_2,\ell_1',\ell_2'\in\Omega(X,b)[([\ell_1]=[\ell_1']\wedge[\ell_2]=[\ell_2'])\implies[\ell_1*\ell_2]=[\ell_1'*\ell_2']]}}
==Proof==
The [[homotopy concatenation]], {{M|1=H:=H_1*H_2}}, is easily shown to be the required homotopy. This is actually an instance of [[Homotopy invariance of path concatenation]]
{{Requires proof|grade=A|msg=Check this page and demote. It was such a chore to write, I just want it done!}}
==Notes==
<references group="Note"/>
==References==
<references/>
{{Theorem Of|Algebraic Topology|Homotopy Theory|Topology}}