Normal-cover local homology detects mixed-derived kernels without choice

The supplied contractible basis consists of path-connected open sets, so connectedness implies path-connectedness: path components are open and their complements are open. Form the set of paths $\gamma :o\to x$, identifying two with the same endpoint when the loop $\gamma \ast ({\gamma }^{\mathrm{\prime }}{)}^{-1}$ belongs to $N$. The subgroup laws make this an equivalence relation. For a member $U$ of the supplied contractible basis and a path $\gamma$ ending in $U$, let $U_{[\gamma ]}$ consist of $[\gamma \ast \eta ]$ for paths $\eta$ lying in $U$ and starting at that endpoint. The projection to $U$ is bijective because any two such paths with the same endpoint are homotopic rel endpoints in $U$. If two such sets over $U$ meet they coincide; for two different basis neighborhoods, a smaller basis neighborhood of a common endpoint shows their intersections contain a basic set of this same form. They therefore define a topology for which $p^{-1}(U)$ is a disjoint union of open sets each homeomorphic to $U$. Surjectivity uses a path to each individual endpoint, rather than selecting all such paths. Thus this is an actual covering space constructed without a representative section.

For completeness the degree-one constant-coefficient calculation needs no universal-coefficient theorem. For any path-connected based space $Y$, concatenate paths by the first-loop-first rule. A constant edge is the boundary of a constant triangle; a path homotopy gives the boundary of its two-triangle prism up to constant endpoint edges; and $uv$ is homologous to $u+v$ by mapping a triangle to the concatenated path with vertex parameters $0,1\mathrm{/}2,1$. A reversed path is homologous to the negative path, since its concatenation with the original contracts by retracing. These finite relations show that $[u{]}_{\mathrm{a}\mathrm{b}}\otimes c\mapsto c[u]\in H_1(Y;k)$ is a well-defined additive balanced map $S:{\pi }_1(Y{)}_{\mathrm{a}\mathrm{b}}{\otimes }_{\mathbb{Z}}k\to H_1(Y;k)$. For a fixed finite cycle $z={\sum }_e{c}_{e}e$, choose paths ${\gamma }_v$ from the basepoint to the finitely many endpoint images and put $T_{\gamma }(z)={\sum }_e[{\gamma }_{e(0)}\ast e\ast {\gamma }_{e(1)}^{-1}{]}_{\mathrm{a}\mathrm{b}}\otimes c_e\mathrm{.}$ Finite choice follows by finite induction in ZF, so these paths exist without an axiom of choice.

A path $\gamma$ lifts from the constant-path point by $t\mapsto [\gamma {\mathrm{\mid }}_{[0,t]}]$, with the restricted path reparametrized and held stationary after its endpoint. This is continuous on the basic sets of step 1.1, and reaches $[\gamma ]$, so $W_N$ is path-connected. For any fixed starting lift, path lifting exists uniquely by finite subdivision into evenly covered basis neighborhoods. A homotopy lifts uniquely by the same finite-grid construction on its compact square: choose a finite fine grid subordinate to the inverse-image cover and extend sheet by sheet, with uniqueness on overlaps. The square is compact metric, so this finite construction uses no choice principle. Hence $p_{\ast }$ is injective on fundamental groups, and its image consists exactly of based loops whose lifted endpoint is the constant-path point, that is, exactly $N$. This identifies ${\pi }_1(W_N)$ with $N$ by the actual projection. The same lifting statement for a singular simplex follows directly by sending a point to the lift obtained along the straight segment from its first vertex; segments joined by a triangle are homotopic inside the simplex, so this gives the unique continuous lift with prescribed first vertex.

Another finite path family changes each loop term by $d_{e(0)}-d_{e(1)}$ in the abelianization. After tensoring, its total coefficient at a vertex is that of the cycle boundary, hence zero. Thus $T_{\gamma }(z)$ has one uniquely defined value $T(z)$, independent of paths or enlargement of the finite endpoint list. On a singular triangle the loops for edges $01,12,02$ satisfy $L_{01}{L}_{12}=L_{02}$ because the triangle fills their concatenation, so $T$ kills its signed boundary. For any finite two-chain use the finite union of its vertex images to get the same conclusion termwise, with its $k$ coefficients. Thus $T$ descends to homology. The relations in step 1.2 say ${\gamma }_{e(0)}\ast e\ast {\gamma }_{e(1)}^{-1}$ is homologous to ${\gamma }_{e(0)}+e-{\gamma }_{e(1)}$; in the weighted sum the extra path terms cancel by the cycle condition. Hence $ST=\mathrm{i}\mathrm{d}$. On a based loop use the constant connector at its endpoint, giving $TS=\mathrm{i}\mathrm{d}$ on every generator $[u{]}_{\mathrm{a}\mathrm{b}}\otimes c$. This proves the natural isomorphism $H_1(Y;k)\cong {\pi }_1(Y{)}_{\mathrm{a}\mathrm{b}}\otimes k$. Naturality follows by mapping a finite connector family forward; independence then removes that family from the map. No paths to all points of $Y$ and no basis of an infinite vector space were chosen.

For $g\in G$ and any representative loop $a$, define the right action by $[\gamma ]\cdot g=[a^{-1}\ast \gamma ]$. Replacing $a$ by another representative gives the same path class, since $N$ is normal; replacing $\gamma$ by an equivalent path also does. The action law follows from $b^{-1}\ast a^{-1}=(a\ast b{)}^{-1}$, and its maps carry the basic sets in step 1.1 to basic sets. On each fiber it is free and transitive: for paths $\gamma ,\delta$ to the same endpoint take the quotient class of $\gamma \ast {\delta }^{-1}$, which sends $[\gamma ]$ to $[\delta ]$. The formula specifies the action uniquely without choosing representatives for all quotient elements. Free $k$-linearization of each fiber gives ${\mathcal{R}}_x$; path transport commutes with this right action because it appends a path at the end, while deck action prepends $a^{-1}$. Thus it is a right-$k[G]$ local system, each fiber individually having a torsor point as a free basis. At the basepoint the constant-path point is a specified basis, and transport along $a$ sends it to $[a]=[1]\cdot g^{-1}$, giving exactly the stated inverse convention and a right-linear map.

A basis generator in the local chain group consists of a base singular simplex $\sigma$ together with one point of the covering fiber over its first vertex and a scalar in $k$. Send it to the unique lift of $\sigma$ with that first vertex, given in step 2.1, with the same scalar. Pairs of this kind are in bijection with covering singular simplices: projection gives the inverse map. Both directions are uniquely specified on generators, hence define inverse maps on all finite chains without selecting a lift for each base simplex. For the face omitting the first vertex, the first point of the lifted face is the transport of the old first point along that edge, exactly the local coefficient boundary rule. The other faces keep the first point. Thus the bijection commutes with all signed boundary terms. It commutes with the right deck action on generators too, so gives the claimed actual chain isomorphism of right $k[G]$-module complexes.

Apply steps 1.2 and 2.2 to $Y=W_N$ and combine with steps 2.1 and 4.1. A based loop $u\in N$ lifts to the based loop whose projection is $u$, so its coefficient-one class maps precisely to $[u]\otimes 1$. For the right action, move the constant-path base lift by $g=[a]$. The lift of $a^{-1}$ joins the old base lift to that new one. Rebase the translated lift of $u$ by this path and its inverse; its projection is $a^{-1}ua$. Connector contributions cancel in first homology by step 1.2, so this gives the stated conjugation action on $N_{\mathrm{a}\mathrm{b}}\otimes k$. Different representatives of $g$ change it by an inner automorphism of $N$, trivial on $N_{\mathrm{a}\mathrm{b}}$. The zero criterion is now exactly the displayed isomorphism and its coefficient-one formula; for $N=P^s\pi$ in the finite mixed series defined in the Statement, it is the next kernel $P^{s+1}\pi$. For a based continuous map $f:(W,o)\to (W^{\mathrm{\prime }},o^{\mathrm{\prime }})$ between spaces with the stated connected, Hausdorff and contractible-neighborhood hypotheses, if $f_{\ast }(N)\subseteq N^{\mathrm{\prime }}◃{\pi }_1(W^{\mathrm{\prime }},o^{\mathrm{\prime }})$, the covering map is explicitly $[\gamma ]\mapsto [f\circ \gamma ]$; the equivalence relation makes it well-defined. It commutes with endpoint projection, the induced quotient-group action and simplex lifting, so step 4.1 is natural for its coefficient maps. Steps 1.2 and 2.2 already prove naturality of the constant-coefficient identification, yielding the stated commutative homology comparison. All covering, chain and homology maps were explicit quotient maps or uniquely defined finite-lift maps, so the full coefficient and choice scope in the Statement is proved.