Hom of homology is not the definition of singular cohomology

By [F1], ${\mathrm{\partial }}_n{\mathrm{\partial }}_{n+1}=0$, and hence for every cochain $f$ one has ${\delta }^{n+1}{\delta }^{n}f=f{\mathrm{\partial }}_{n+1}{\mathrm{\partial }}_{n+2}=0$. Thus the image in [F2] is a vector subspace of the kernel and the quotient exists. Both kernel and image are specified sets, and forming their quotient makes no selection of representatives. This verifies the choice-free definition.

If $f$ is a cocycle and $z$ a cycle, set $\epsilon ([f])([z])=f(z)$. Replacing $z$ by $z+\mathrm{\partial }c$ changes this value by $f(\mathrm{\partial }c)=(\delta f)(c)=0$. Replacing $f$ by $f+\delta g$ changes it by $g(\mathrm{\partial }z)=0$. Addition and scalar multiplication commute with evaluation, so it defines the claimed linear map on the two quotients. For a continuous map $u:X\to Y$, postcomposition on simplices commutes with each face, and hence with the signed boundary. Its chain map $u_{\mathrm{\#}}$ therefore satisfies $f(u_{\mathrm{\#}}z)=(f\circ u_{\mathrm{\#}})(z)$, which is the naturality identity on classes. Neither construction uses AC.

Assume AC for this step. Apply the positive branch of [F3] to the real complex [F1]. Concretely, any functional on $H_n$ pulls back to the cycles and extends to $C_n$; the extension vanishes on boundaries, so gives a cocycle mapping to that functional. If a cocycle vanishes on cycles, the rule $b(\mathrm{\partial }c)=f(c)$ is well-defined on the boundary subspace in degree $n-1$ and extends to $C_{n-1}$, giving $f=\delta b$ after that extension. These are exactly the surjectivity and injectivity arguments in [F3]; both use its AC extension clause. Conversely every coboundary vanishes on cycles by step 1.2. Thus evaluation is the asserted natural isomorphism. It is not an alternative definition, and no global family of cochain representatives was chosen.

If $X=\mathrm{\varnothing }$, all chain and cochain groups are zero and evaluation is the unique isomorphism between zero spaces in every degree. If $X$ is a point, there is one simplex in every nonnegative degree and ${\mathrm{\partial }}_k$ is multiplication by ${\sum }_{i=0}^k(-1{)}^i$ for $k>0$: it is the identity in positive even degrees and zero in odd degrees, with ${\mathrm{\partial }}_0=0$. Therefore $H_0=\mathbb{R}$ and $H_k=0$ for $k>0$; dually $H^0=\mathbb{R}$ and $H^k=0$ for $k>0$. Evaluation in degree zero sends the constant scalar cochain a to the functional $r\mapsto ar$, an isomorphism without choice. In negative degrees both sides vanish. For general X at degree zero there is no incoming coboundary, so the injectivity argument uses no negative-degree extension. Constant and repeated simplices are retained in these unnormalized complexes; the representative computations in step 1.2 apply to them as written.