A homotopy operator for Spencer’s sequence in the C ∞-case

The main result of the formal theory of overdetermined systems of differential equations says that any regular system Au = f with smooth coefficients on an open set U ⊂ ℝ ⁿ admits a solution in smooth sections of the bundle of formal power series provided that f satisfies a compatibility condition in U. Our contribution consists in detailed study of the dependence of formal solutions on the point of the base U of the bundle. We also parameterize these solutions by their Cauchy data. In doing so, we prove that, under absence of topological obstructions, there is a formal solution which smoothly depends on the point of the base. This leads to a concept of a finitely generated system (do not mix up it with holonomic or finite -type systems) for which we then prove a C ^∞-Poincaré lemma. The text was submitted by the authors in English.