Square lemma (of homotopic paths)

Statement

Let [ilmath]F:[0,1]\times[0,1]\rightarrow X[/ilmath] be a continuous map (note this is sufficient to make it a homotopy, specifically a path homotopy - but it need not be end point preserving and supposed we define the following paths:

• [ilmath]f:[0,1]\rightarrow X[/ilmath] by [ilmath]f(t):\eq F(t,0)[/ilmath]
• [ilmath]g:[0,1]\rightarrow X[/ilmath] by [ilmath]g(t):\eq F(1,t)[/ilmath]
• [ilmath]h:[0,1]\rightarrow X[/ilmath] by [ilmath]h(t):\eq F(0,t)[/ilmath] and
• [ilmath]k:[0,1]\rightarrow X[/ilmath] by [ilmath]k(t):\eq F(t,1)[/ilmath]

Then we claim^Ex::

• [ilmath](f*g)\simeq(h*k)\ (\text{rel }\{0,1\})[/ilmath]
  • In words: the path concatenations of ([ilmath]f[/ilmath] then [ilmath]g[/ilmath]) and ([ilmath]h[/ilmath] then [ilmath]k[/ilmath]) are end point preserving homotopic

Proof

Grade: C

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:

Gist is here, could use writeup - not a priority Alec (talk) 14:51, 25 April 2017 (UTC)

Notes:

• Define [ilmath]H':[0,1]\times[0,1]\rightarrow [0,1]\times[0,1][/ilmath] as follows:
  • [ilmath]H':(t,s)\mapsto\left\{\begin{array}{lr} (0,2t)+s\big((2t,0)-(0,2t)\big) & \text{if }t\in[0,\frac{1}{2}] \\ (2t-1,1)+s\big((1,2t-1)-(2t-1,1)\big)& \text{if }t\in[\frac{1}{2},1]\end{array}\right.[/ilmath] -
    TODO: I may (have) have deviated from convention, [ilmath]s[/ilmath] and [ilmath]t[/ilmath] should be swapped, as [ilmath]t[/ilmath] should represent stages of the homotopy and [ilmath]s[/ilmath] (more typically: [ilmath]x[/ilmath]) the point in the domain space of the homotopy - proceeding anyway as it doesn't matter Alec (talk) 14:51, 25 April 2017 (UTC)
    • This is just the straight-line homotopy in [ilmath][0,1]\times[0,1][/ilmath] - which is fine as [ilmath][0,1]^2[/ilmath] is convex. Notice if [ilmath]s\eq 0[/ilmath] we go along [ilmath]h[/ilmath] for [ilmath]t\in[0,\frac{1}{2}][/ilmath] then along [ilmath]k[/ilmath].
    • It is a homotopy as it is a continuous map on something [ilmath]\times[0,1][/ilmath] to some space - any map like this is a homotopy.
      • We need it to be relative to [ilmath]\{0,1\} [/ilmath], that is:
        • [ilmath]\forall t,r\in [0,1]\forall p\in\{0,1\}[H'(p,s)\eq H'(p,r)][/ilmath]
          • We have this as [ilmath]H'(0,r)\eq (0,0)+r(0,0)\eq (0,0)[/ilmath] and [ilmath]H'(1,r)\eq(1,1)+r(0,0)[/ilmath]
            • As expected as the entire idea was [ilmath]H'(0,r)[/ilmath] is the start (in the domain) of the [ilmath]f*g[/ilmath] path - which is the same as the start in the domain of the [ilmath]h*k[/ilmath] path, "" for the end points.