Lifting criterion for maps from path-connected locally path-connected spaces

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

Let $p:E\to B$ be a covering, let $\alpha :I\to B$ be a path, and let $e_0\in E$ satisfy $p(e_0)=\alpha (0)$. There is a unique path $\tilde{\alpha }:I\to E$ with $\tilde{\alpha }(0)=e_0$ and $p\circ \tilde{\alpha }=\alpha$. (Existence and uniqueness of path lifts through a covering map).

Endpoint-fixed homotopic paths in the base have lifts with the same endpoint whenever their lifts begin at the same point. (The endpoint of a lifted path depends only on its endpoint-fixed homotopy class).

Let $Y$ be connected and let $f,g:Y\to E$ be lifts through the same covering of the same map $Y\to B$. If $f(y_0)=g(y_0)$ for some $y_0\in Y$, then $f=g$. (Two lifts from a connected space that agree at one point agree everywhere).

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).

Let $(X,\mathcal{T})$ be a topological space (def-topological-space) and let $x\in X$. Subsets carry the subspace topology (def-subspace-topology-top); connectedness is def-connected-space and path-connectedness is def-path-connected. $X$ is locally connected at $x$ when for every open $U$ with $x\in U$ there is an open connected $V$ with $x\in V\subseteq U$, and locally connected when this holds at every point; $X$ is locally path-connected at $x$ when for every open $U$ with $x\in U$ there is an open path-connected $V$ with $x\in V\subseteq U$, and locally path-connected when this holds at every point. (Locally connected and locally path-connected spaces: a neighbourhood base of open connected, respectively open path-connected, sets at every point).

Let $f:(X,x_0)\to (Y,y_0)$ be continuous with $f(x_0)=y_0$. Then $f_{\ast }([\alpha ])=[f\circ \alpha ]$ is a well-defined group homomorphism, and for pointed continuous maps ${\mathrm{id}}_{\ast }=\mathrm{id}$ and $(g\circ f{)}_{\ast }=g_{\ast }\circ f_{\ast }$ (Induced fundamental-group maps are well defined, functorial and invariant under based homotopy).