A covering map induces an injective homomorphism on fundamental groups

Given: The objects, hypotheses, and choice principles stated above.

Let $p:E\to B$ be a covering, $H:Y\times I\to B$ a homotopy, and ${\tilde{H}}_0:Y\to E$ a lift of $H(-,0)$. There is a unique lift $\tilde{H}:Y\times I\to E$ of $H$ extending ${\tilde{H}}_0$. (Existence and uniqueness of homotopy lifts through a covering map).

Let $f:X\to Y$ be continuous and let $x_0\in X$. Composition sends a loop $\alpha$ at $x_0$ to the loop $f\circ \alpha$ at $f(x_0)$. Using the loop classes and fundamental group of def-based-loops-and-fundamental-group, the proposed induced homomorphism is $f_{\ast }:{\pi }_1(X,x_0)⟶{\pi }_1(Y,f(x_0)),f_{\ast }([\alpha ]):=[f\circ \alpha ]\mathrm{.}$ The next theorem proves that this value is independent of the representative, that it is a group homomorphism in the sense of def-group-homomorphism, and that induced maps respect identities, composition and homotopies that fix the basepoint. (The homomorphism on fundamental groups induced by a pointed continuous map).

A topological space $X$ is simply connected when it is nonempty and path-connected (def-path-connected) and, for every $x_0\in X$, the group ${\pi }_1(X,x_0)$ has exactly one element. (Simply connected topological spaces).