Homotopy invariance of path concatenation

Stub grade: A*

This page is a stub

This page is a stub, so it contains little or minimal information and is on a to-do list for being expanded.The message provided is:

Really not in the mood for this, done it anyway, check first and flesh out

Statement

TODO: This caption

Let [ilmath]p_1,p_2,p_1',p_2'\in[/ilmath][ilmath]C([0,1],X)[/ilmath] be given. Suppose [ilmath]H:\ p_1\simeq p_1'\ (\text{rel }\{0,1\})[/ilmath] and [ilmath]H:\ p_2\simeq p_2'\ (\text{rel }\{0,1\})[/ilmath] are end point preserving homotopies (where [ilmath]H_1,H_2:[0,1]\times [0,1]\rightarrow X[/ilmath] are the specific homotopies of the paths) then:

• [ilmath]H:p_1*p_2\simeq p_1'*p_2'\ (\text{rel }\{0,1\})[/ilmath] where [ilmath]H:=H_1*H_2[/ilmath] - the homotopy concatenation, explicitly:
  • [ilmath]H:[0,1]\times[0,1]\rightarrow X[/ilmath] by [ilmath]H:(s,t)\mapsto\left\{\begin{array}{lr}H_1(s,2t)&\text{for }t\in[0,\frac{1}{2}]\\ H_2(s,2t-1)&\text{for }t\in[\frac{1}{2},1]\end{array}\right.[/ilmath]
    • Note that the fact [ilmath]t=\frac{1}{2}[/ilmath] is in both parts is a nod towards the use of the pasting lemma

Proof

Grade: A*

This page requires one or more proofs to be filled in, it is on a to-do list for being expanded with them.

Please note that this does not mean the content is unreliable. Unless there are any caveats mentioned below the statement comes from a reliable source. As always, Warnings and limitations will be clearly shown and possibly highlighted if very important (see template:Caution et al).
The message provided is:

It's basically already done. All we have to show is that the homotopy concatenation, [ilmath]H[/ilmath], fits the requirements

See also

• The fundamental group

References