Fundamental Group Axiom Verification

Let $X$ be a topological space and $x \in X$. The fundamental group $\pi_1(X,x)$ is defined as the set of homotopy classes (relative to endpoints) of loops based at $x$, i.e. $$ \pi_1(X,x) = \{ [\gamma] \mid \gamma : [0,1] \to X, \ \gamma(0)=\gamma(1)=x \}. $$ We define a binary operation on $\pi_1(X,x)$ by concatenation: for loops $\gamma_1, \gamma_2$, define $$ (\gamma_1 * \gamma_2)(t) = \begin{cases} \gamma_1(2t) & 0 \le t \le \tfrac{1}{2}, \\ \gamma_2(2t - 1) & \tfrac{1}{2} \le t \le 1. \end{cases} $$ Then define $$ [\gamma_1] \cdot [\gamma_2] := [\gamma_1 * \gamma_2]. $$ We show this makes $\pi_1(X,x)$ a group. Suppose $\gamma_1 \sim \gamma_1'$ and $\gamma_2 \sim \gamma_2'$ (homotopy relative endpoints). Then there exist homotopies $H$ and $K$ between them. One constructs a homotopy between $\gamma_1 * \gamma_2$ and $\gamma_1' * \gamma_2'$ by concatenating $H$ and $K$ in the same way: $$ F(t,s) = \begin{cases} H(2t,s) & 0 \le t \le \tfrac{1}{2}, \\ K(2t-1,s) & \tfrac{1}{2} \le t \le 1. \end{cases} $$ Thus $[\gamma_1 * \gamma_2] = [\gamma_1' * \gamma_2']$, so the operation is well-defined. Let $\gamma_1, \gamma_2, \gamma_3$ be loops at $x$. Then $$ (\gamma_1 * \gamma_2) * \gamma_3 \sim \gamma_1 * (\gamma_2 * \gamma_3), $$ since both paths traverse $\gamma_1$, $\gamma_2$, and $\gamma_3$ in order, differing only by a reparametrization of $[0,1]$. This reparametrization yields a homotopy relative endpoints. Hence $$ ([\gamma_1] \cdot [\gamma_2]) \cdot [\gamma_3] = [\gamma_1] \cdot ([\gamma_2] \cdot [\gamma_3]). $$ Let $e : [0,1] \to X$ be the constant loop at $x$, defined by $e(t)=x$. Then for any loop $\gamma$, $$ e * \gamma \sim \gamma, \quad \gamma * e \sim \gamma, $$ by a simple reparametrization homotopy. Hence $[e]$ is the identity element. Let $\gamma$ be a loop at $x$. Define the reverse path $$ \gamma^{-1}(t) = \gamma(1 - t). $$ Then $$ \gamma * \gamma^{-1} \sim e, \quad \gamma^{-1} * \gamma \sim e, $$ since the path goes out along $\gamma$ and returns along the same path, which can be contracted to the constant loop. Thus $[\gamma^{-1}]$ is the inverse of $[\gamma]$. Therefore, the fundamental group is indeed a group.