Relative Poincaré lemma (source code)

= Relative Poincaré lemma

Let a neighborhood of a submanifold retract onto it by fiberwise radial contraction in a <tubular neighborhood>. If a <closed differential form> $\beta$ pulls back to zero on the submanifold, the radial homotopy formula gives $\beta=d\alpha$, with $\alpha$ vanishing along the zero section. Applying the homotopy operator to $\beta$ gives the primitive directly. This is the relative ingredient in the <relative Moser theorem>.