Let $X$ be a sufficiently good topological space and $x \in X$, then it is well-known that there are equivalences of categories $$\begin{equation*} \begin{split} \left \{\text{coverings} \ p: Y \longrightarrow X \right \} & \longrightarrow \left \{ \text{local systems on} \ X \right \} & \longrightarrow \pi_1(X,x)-\text{sets} \\ Y & \longmapsto \ \ \ \ \ \ \ \ \ \ \mathcal{F}_Y & \longrightarrow p^{-1}(x) \end{split} \end{equation*}$$ where by coverings I mean local homemorphisms and local systems are locally constant sheaves.
- The notation $\mathcal{F}_Y$ denotes the sheaf of sections of $p: Y \longrightarrow X$, this induces the first equivalence
- For any local system $\mathcal{F}$ on $X$ and a loop $\gamma: [0,1] \longrightarrow X$ at $x$, i.e. $\gamma(0)=\gamma(1)=x$, the sheaf $\gamma^{-1}\mathcal{F}$ is constant so there are isomorphisms $$\mathcal{F}_x \simeq (\gamma^{-1}\mathcal{F})_0 \simeq (\gamma^{-1}\mathcal{F})_1 \simeq \mathcal{F}_x$$ and hence $\mathcal{F}_x$ is equipped with an action of $\pi_1(X,x)$. This induces the second equivalence.
The composition of these two is often denoted as $\operatorname{Fib}_x$, and it is representable by the universal covering $\widetilde{X}$ of $X$. But I'd like to prove (or reference) that this encodes the lifting property:
- We know that for any $y \in p^{-1}(x)$, then every path $\gamma:[0,1]: \longrightarrow X$ admits a lifting to $Y$, i.e. $\widetilde{\gamma}:[0,1] \longrightarrow Y$ s.t $p \circ \widetilde{\gamma} = \gamma$ and $\widetilde{\gamma}(0)=y$. The ending point $\widetilde{\gamma}(1)$ is independent up to homotopy. How to show that the action $$[\gamma] \cdot y = \widetilde{\gamma}(1)$$ is really the action that defined above.
Thank you in advance.
Since a section of $\gamma^{-1} \mathcal{F}$ is the same as a section of $\gamma^* p : Y \times_X [0, 1] \to [0,1]$ is the same as a lift of $\gamma$ to $Y$, the trivialization $\gamma^{-1} \mathcal{F} \cong [0,1] \times (\gamma^{-1}\mathcal{F})_0$ is exactly the same as path lifting for $\gamma$.
In other words, the map you get through the composition $\mathcal{F}_x \simeq (\gamma^{-1}\mathcal{F})_0 \simeq (\gamma^{-1}\mathcal{F})_1 \simeq \mathcal{F}_x$ is tautologically the same as the map you get from path lifting.