The aim is to prove Kunneth formula, namely if is finitely generated and free -module, then . We first show it for CW complexes. For this there is a slick way to do it, and it hinges on the fact that the category of CW complexes are generated by taking homotopy colimit from points, so it boils down to just checking Kunneth formula holds for , which is trivial.
To be more precise about this, we need the notion of a general cohomology theory. The key lemma is the following:
If there is a natural transformation from one cohomology theory to another that commutes with boundary maps and agree on points, then it is a natural isomorphism on CW complexes.
The idea is to induct on skeletons and 5-lemma. Note that for any cohomology theory we have and induces an isomorphism between . This does the job for finite-dimensional CW complexes.
For infinite dimensional CW complexes, we can use Milnor sequence: If , we can understand built out of . Assuming , then we have a map . Define to be the cokernel of (note that is the kernel of ).
There is a short exact sequence . Let us sketch the proof: Consider the infinite mapping telescope (infinite wedding cake), , which is homotopy equivalent to (This uses the homotopy extension property of CW pairs). The idea is that even we don’t know how to do infinite Mayer-Vietoris, we can use mapping telescope to reduce to doing finite Mayer vietoris. Consider the even piece and the odd piece . Each of these piece is disjoint union of infinitely many cylinders, and we can use the infinite disjoint union axiom to calculate the cohomology of and . Their intersection is a disjoint union of indexed by . The map of to is inclusion while to is the identity. Now use the Mayer-Vietoris.
Finally, since any space is weakly homotopy equivalent to a CW-complex by the CW approximation theory, and practically any cohomology theory descends to the weak homotopy category.
Now we use the key lemma to prove Kunneth formula. if is a space, then is a cohomology theory, so is if is finitely generated free module for each (finitely generated is needed for the infinite product axiom).