Square lemma (of homotopic paths)

Statement

Let $F:[0,1]\times[0,1]\rightarrow X$ 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:

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

Then we claim^Ex::

• $(f*g)\simeq(h*k)\ (\text{rel }\{0,1\})$
  • In words: the path concatenations of ($f$ then $g$) and ($h$ then $k$) 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 $H':[0,1]\times[0,1]\rightarrow [0,1]\times[0,1]$ as follows:
  • $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.$ -
    TODO: I may (have) have deviated from convention, $s$ and $t$ should be swapped, as $t$ should represent stages of the homotopy and $s$ (more typically: $x$) 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 $[0,1]\times[0,1]$ - which is fine as $[0,1]^2$ is convex. Notice if $s\eq 0$ we go along $h$ for $t\in[0,\frac{1}{2}]$ then along $k$.
    • It is a homotopy as it is a continuous map on something $\times[0,1]$ to some space - any map like this is a homotopy.
      • We need it to be relative to $\{0,1\}$, that is:
        • $\forall t,r\in [0,1]\forall p\in\{0,1\}[H'(p,s)\eq H'(p,r)]$
          • We have this as $H'(0,r)\eq (0,0)+r(0,0)\eq (0,0)$ and $H'(1,r)\eq(1,1)+r(0,0)$
            • As expected as the entire idea was $H'(0,r)$ is the start (in the domain) of the $f*g$ path - which is the same as the start in the domain of the $h*k$ path, "" for the end points.