We can now prove the Poincaré lemma by proving its core assertion: there is a chain homotopy between the two chain maps and induced by the inclusions of into either end of the homotopy cylinder . That is, we must define a map satisfying the equation
Before defining the map , we want to show that any -form on the homotopy cylinder can be uniquely written as , where is a -form and is a -form, both of which are “constant in time”, in a certain sense. Specifically, we can pull back the canonical vector field on along the projection to get a “time” vector field on the cylinder. Then we use the interior product to assert that and .
But this should be clear, if we just define then we definitely have , since interior products anticommute. Then we can define , and calculate , since the pairing of with is . The uniqueness should be clear.
So now let’s define
where is the inclusion of into the homotopy cylinder sending to .
Now to check that this is a chain homotopy, which is purely local around each point . This means that we can pick some coordinate patch on , which lifts to a coordinate patch on , where . Since everything in sight is linear we will consider two cases: , where is some multi-index of length ; and , where is some multi-index of length .
In the first case we have , while , which we can write as a bunch of terms not involving at all plus . Therefore we calculate:
and we conclude that , as asserted.
Now, as to the other side. This time, since for any , we know that both terms on the left hand side of the chain homotopy equation is zero. Meanwhile, we calculate
so as well, just as asserted.