Covering-space actions and fundamental-groupoid quotients

By [F1] and [F2], $p$ is a covering and its deck transformations are exactly the transformations from $N$. The action is free and every fibre is an orbit, so these transformations act freely and transitively on each fibre. Thus the covering is regular in the stated sense and $N$ identifies with its deck group.

Projection sends a path class upstairs to its projected class and is invariant under translation. Given two composable arrow orbits, translate a representative of the second so that its source equals the target of a representative of the first. Freeness gives a unique such translate; translating both representatives together changes the composite only by a common translate. Hence this rule gives a well-defined orbit groupoid, and projection defines a functor from it to ${\mathrm{\Pi }}_1(B)$.

For a based loop downstairs, [F4] gives a lift from $x$ ending at a unique $nx$ by step 1.1. Endpoint-fixed homotopy lifting makes $n$ independent of the representative. If lifts of loops $\alpha$ and $\beta$ end at $nx$ and $mx$, respectively, then the lift of their first-path-first concatenation is the lift of $\alpha$ followed by the $n$-translate of the lift of $\beta$; it ends at $nmx$. Thus the endpoint map is a homomorphism.

Each point of $B$ is an orbit, and [F4] lifts every base path from a chosen point over its source. Thus the functor of step 2.1 is surjective on arrows. If two projected paths are endpoint-fixed homotopic, first translate one lift so their initial points agree. Lift the homotopy starting with the first path. Its initial endpoint remains fixed by uniqueness of path lifts; its final endpoint also remains fixed, since it lifts a constant path. The final lifted path is therefore the second path by uniqueness, and the two original arrow classes differ by a translation. The functor is consequently injective on arrows and is an isomorphism. The same lifting argument gives the asserted bijection on arrows starting at any specified point.

Every $n\in N$ occurs: path-connectedness supplies a path from $x$ to $nx$, whose projection is a loop. The endpoint map has kernel exactly the projected classes of loops at $x$: a lifted loop has endpoint $x$, and conversely endpoint $x$ makes the lifted path a loop. Finally $p_{\ast }$ is injective by [F5]. These facts prove exactness; no semilocal simple connectedness or universal cover was used. The separate condition in [F6] is relevant only to an additional universal-cover invocation.