The Poincaré lemma on manifolds

A closed differential form of positive degree on a manifold is locally exact: near every point it is the exterior derivative of a globally defined form of the same regularity (TauCeti.exists_mextDeriv_eq_nhds). Boundary and corner points are included.

The form is read in the preferred extended chart at the point. Mathlib's range I is convex, so the intersection of a small ball about the chart point with range I is a convex set with unique derivatives inside the chart target, although it need not be open. The relative flat Poincaré lemma Convex.exists_contDiffOn_forall_extDerivWithin_eq gives a primitive there. Its pullback along the chart is cut off by a smooth bump function supported in the chart domain, which gives a primitive on all of M near the point.

The cutoff is the only place where [FiniteDimensional ℝ E] and [T2Space M] are used: smooth bump functions need both. The coefficient space is complete because the flat primitive is an integral.

Main declarations

• TauCeti.exists_mextDeriv_eq_nhds: the manifold Poincaré lemma.

References

• John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Theorem 17.14 and Corollary 17.15.

theorem TauCeti.exists_mextDeriv_eq_nhds {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {k : ℕ} [FiniteDimensional ℝ E] [T2Space M] [IsManifold I (↑⊤) M] {r : ℕ∞} (hr : 1 ≤ r) {φ : RoughForm I M F (k + 1)} (hφ : IsSmoothForm I (↑r) φ) {x : M} (hclosed : ∀ᶠ (y : M) in nhds x, mextDeriv φ y = 0) : ∃ U ∈ nhds x, ∃ (ψ : RoughForm I M F k), IsSmoothForm I (↑r) ψ ∧ ∀ y ∈ U, mextDeriv ψ y = φ y

The Poincaré lemma on manifolds. A C^r form of positive degree, r ≥ 1, that is closed near a point x is, on a neighbourhood of x, the exterior derivative of a C^r form defined on the whole manifold. The manifold may have boundary or corners.

The coefficient space is complete: with values in the finitely supported sequences there is a smooth closed 1-form on ℝ with no local primitive. Finite dimensionality of the model and the Hausdorff property are used only to cut the local primitive off by a smooth bump function.