# Restrict differential forms that vanish along fibres to the base

I am reading Jean-Luc Brylinski's book on loop space. At the end of section 1.6 Leray Spectral Sequence, he claims without proof that

Let $$f: Y\to X$$ be a smooth bundle of paracompact manifolds. A $$p$$-form $$\omega$$ on $$Y$$ is called basic if it satisfies:

For any vertical vector field $$\xi$$ on $$Y$$,

1. $$i(\xi)\omega =0$$;
2. $$i(\xi)\mathrm{d} \omega =0.$$

Assume the fiber $$F$$ is connected, then $$f^*$$ identifies space of smooth $$p$$-forms $$A^p(X)$$ with space of basic $$p$$-forms on $$Y$$.

I wonder whether it can be proved by Cartan homotopy formula.

More precisely, given $$\omega$$ basic, define $$\eta (x_0) =\omega (x_0, z)$$ for $$(x_0,z)\in f^{-1}(x_0)$$. Choose a local coordinate we see that $$\omega$$ has no fiber components.

Since $$L_{\gamma '(t)}\omega =0$$ for path in $$f^{-1}(x_0)$$, it is well-defined.

Does this work? The following are some info that I thought might help.

A somewhat related post is here.

Brylinski also describes basic forms in language of Cartan filtration $$F^k$$, which is subcomplexes of $$A^{\bullet}(Y)$$ where $$F^k(A^n(Y))$$ consists of those $$n$$-forms $$\omega$$ such that for any vertical vector fields $$\xi _1, \cdots ,\xi _{n-k+1}$$, $$i(\xi _1)\cdots i(\xi _{n-k+1})\omega=0.$$

I looked up some related books. Brylinski referred Cartan filtration to Cartan's article La transgression dans un groupe de Lie et dans un fibré principal .

The same filtration appears in Akio Hattori's paper Spectral Sequence in the de Rham Cohomology of fibre bundles, in which Hattori referred that filtration to

1. Leray L'anneau spectral et l'anneau filtré d'homologie d'un espace localement compact et d'une application continue
2. Serre Homologie singulière Des espace fibrés

But I can hardly read French.