Now we’ve seen that differentiable manifolds, smooth maps, and homotopies form a 2-category, but it’s not the only 2-category around. The algebra of differential forms — together with the exterior derivative — gives us a chain complex. Since pullbacks of differential forms commute with the exterior derivative, they define a chain map between two chain complexes.
And now I say that a homotopy between two maps induces a chain homotopy between the two chain maps and . And, indeed, if the homotopy is given by a smooth map then we can write , where and are the two boundary inclusions of into the “homotopy cylinder” , and we will work with these inclusions first.
Since , we have chain maps , and we’re going to construct a chain homotopy . That is, for any differential form we will have the equation
Given this, we can write
which shows that is then a chain homotopy from to .
Sometimes the existence of the chain homotopy is referred to as the Poincaré lemma; sometimes it’s the general fact that a homotopy induces the chain homotopy ; sometimes it’s a certain corollary of this fact, which we will get to later. Given my categorical bent, I take it to be the general assertion that we have a 2-functor between the homotopy 2-category and that of chain complexes, chain maps, and chain homotopies.
As a side note: now we can finally understand what the name “chain homotopy” means.