Proof.The two sides are evidently equivalent in the case where is homeomorphic to , so to establish the result it suffices, as usual, to check by induction over a handle decomposition of . Given a handle decomposition , we have a homotopy pullback diagram of spaces
(8)
which gives rise to a natural map in -homology
from the homology of the mapping spaces to the cotensor product of the comodules and over the coalgebra . This map is an equivalence exactly if the homological Eilenberg–Moore, or Rothenberg–Steenrod, spectral sequence for this homotopy Cartesian diagram converges. By Dwyer [Dw], the convergence of this Eilenberg–Moore spectral sequence is assured if the base is connected and the action
is nilpotent for a choice of basepoint .
Since is -connective, for any map is nullhomotopic, and therefore the base is connected.
We can thus take to be the constant map valued at the basepoint of , and so identify .
We now show the action of on is nilpotent.
Consider the fiber sequence .
This fibration admits a section, given by the constant maps.
Consequently, there is an identification as a semi-direct product:
Through this identification, the action of on is the unique action that extends the standard actions of and of on .
By assumption, the action of on is nilpotent.
In the case that , the same assumption grants that the action of on is nilpotent.
In the case that , the action of on is automatically nilpotent due to commutativity.
Nilpotence of the action of on follows. Consequently, the natural map in -homology above is an equivalence.
The remainder of this argument is checking that we have imposed sufficient finiteness conditions to ensure the convergence in cohomology as well as homology. Dualizing, we obtain an equivalence
Since is finite, the mapping space has finitely many components for any -dimensional finite CW complex . Because the source spaces, , , , and , all have have the homotopy types of finite -dimensional CW complexes, we obtain that all these mapping spaces have finitely many components. Since they are additionally finite CW complexes and is finite type, the homology groups of the mapping spaces are finite rank over , and therefore is its own double dual: the map is an equivalence. Likewise, there is an equivalence between the dual of the tensor product and the cotensor product
– this can be seen by commuting duality with the colimit to obtain a limit of a cosimplicial object, then comparing termwise.
Continuing, one then concludes the equivalence