The Poincaré lemma for differential forms on star-convex sets

Let s be an open subset of a real normed space E, star-convex with respect to a point x₀, and let ω be a C¹ differential (n + 1)-form on s with values in a Banach space F. The Poincaré homotopy operator (TauCeti.poincareHomotopy) contracts ω along the rays from x₀:

(K ω)(x)(v₁, …, vₙ) = ∫₀¹ tⁿ ω(x₀ + t (x - x₀))(x - x₀, v₁, …, vₙ) dt.

It satisfies the homotopy formula d (K ω) + K (d ω) = ω on s (StarConvex.extDeriv_poincareHomotopy_add_poincareHomotopy_extDeriv). Consequently every closed C¹ form of positive degree on s is exact: if d ω = 0 on s, then K ω is a primitive of ω (StarConvex.extDeriv_poincareHomotopy). The primitive is as smooth as ω (StarConvex.contDiffOn_poincareHomotopy) and vanishes at x₀ (TauCeti.poincareHomotopy_self).

The same holds relative to a convex set s with unique derivatives that need not be open, such as a closed half-ball, the image of a boundary chart of a manifold with boundary. There the derivatives are taken within s, and the homotopy formula reads extDerivWithin (K ω) s + K (extDerivWithin ω s) = ω on s (Convex.extDerivWithin_poincareHomotopy_add_poincareHomotopy_extDerivWithin). Differentiating K ω within s uses Mathlib's mean value inequality along the segments of s, which is why the relative statements ask for convexity rather than star-convexity.

Mathlib proves the Poincaré lemma for 1-forms on convex sets by integrating along segments (Convex.exists_forall_hasFDerivAt_of_fderiv_symmetric); this file treats forms of every positive degree with Mathlib's exterior derivative extDeriv. A smooth primitive vanishing at the centre of a ball is what Moser's deformation argument integrates, for instance in the proof of Darboux's theorem.

The homotopy formula is the integral over t ∈ [0, 1] of the identity d/dt (tⁿ⁺¹ ω(x₀ + t (x - x₀))) = tⁿ⁺¹ Dω(…)(x - x₀) + (n + 1) tⁿ ω(…), after the derivative term is split by the constant-coefficient Cartan formula ContinuousAlternatingMap.alternatizeUncurryFin_curryLeft_comp_add_curryLeft.

Main declarations

• TauCeti.poincareHomotopy: the Poincaré homotopy operator with centre x₀.
• TauCeti.poincareHomotopy_pullback_apply: it commutes with pullback along a continuous linear map, which moves the centre.
• StarConvex.compContinuousLinearMap_poincareHomotopy_eq: centred at a fixed point of a linear map, it preserves invariance of forms under that map.
• StarConvex.contDiffOn_poincareHomotopy: it preserves C^r regularity on s.
• StarConvex.extDeriv_poincareHomotopy_add_poincareHomotopy_extDeriv: the homotopy formula.
• StarConvex.extDeriv_poincareHomotopy and StarConvex.exists_contDiffOn_forall_extDeriv_eq: the Poincaré lemma.
• Convex.contDiffOn_poincareHomotopy, Convex.extDerivWithin_poincareHomotopy_add_poincareHomotopy_extDerivWithin, Convex.extDerivWithin_poincareHomotopy and Convex.exists_contDiffOn_forall_extDerivWithin_eq: the relative versions on convex sets with unique derivatives.

References

• M. Spivak, Calculus on Manifolds, Theorem 4-11, whose proof uses this homotopy operator.
• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Chapter 17 (the Poincaré lemma).

noncomputable def TauCeti.poincareHomotopy {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} (x₀ : E) (ω : E → E [⋀^Fin (n + 1)]→L[ℝ] F) (x : E) : E [⋀^Fin n]→L[ℝ] F

The Poincaré homotopy operator with centre x₀: the n-form x ↦ ∫₀¹ tⁿ ω(x₀ + t (x - x₀))(x - x₀, ·) dt built from a differential (n + 1)-form ω. When ω is C¹ on an open set star-convex with respect to x₀ and takes values in a Banach space, it satisfies d (K ω) + K (d ω) = ω there.

theorem TauCeti.poincareHomotopy_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} (x₀ : E) (ω : E → E [⋀^Fin (n + 1)]→L[ℝ] F) (x : E) : poincareHomotopy x₀ ω x = ∫ (t : ℝ) in 0..1, t ^ n • (ω ((AffineMap.lineMap x₀ x) t)).curryLeft (x - x₀)

@[simp]

theorem TauCeti.poincareHomotopy_self {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} (x₀ : E) (ω : E → E [⋀^Fin (n + 1)]→L[ℝ] F) : poincareHomotopy x₀ ω x₀ = 0

The Poincaré homotopy operator vanishes at its centre.

theorem TauCeti.poincareHomotopy_congr {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} {x₀ x : E} {ω₁ ω₂ : E → E [⋀^Fin (n + 1)]→L[ℝ] F} (h : Set.EqOn ω₁ ω₂ (segment ℝ x₀ x)) : poincareHomotopy x₀ ω₁ x = poincareHomotopy x₀ ω₂ x

The Poincaré homotopy operator at x only depends on the form along the segment [x₀, x].

@[simp]

theorem TauCeti.poincareHomotopy_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} (x₀ : E) : poincareHomotopy x₀ 0 = 0

The Poincaré homotopy operator of the zero form is zero.

theorem TauCeti.poincareHomotopy_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} (x₀ : E) (c : ℝ) (ω : E → E [⋀^Fin (n + 1)]→L[ℝ] F) : poincareHomotopy x₀ (c • ω) = c • poincareHomotopy x₀ ω

The Poincaré homotopy operator commutes with real scalar multiplication of forms.

theorem TauCeti.poincareHomotopy_add_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} {x₀ x : E} {ω₁ ω₂ : E → E [⋀^Fin (n + 1)]→L[ℝ] F} (h₁ : ContinuousOn ω₁ (segment ℝ x₀ x)) (h₂ : ContinuousOn ω₂ (segment ℝ x₀ x)) : poincareHomotopy x₀ (ω₁ + ω₂) x = poincareHomotopy x₀ ω₁ x + poincareHomotopy x₀ ω₂ x

The Poincaré homotopy operator is additive on forms that are continuous along the segment [x₀, x].

theorem TauCeti.poincareHomotopy_pullback_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [CompleteSpace (E [⋀^Fin n]→L[ℝ] F)] [CompleteSpace (E' [⋀^Fin n]→L[ℝ] F)] (A : E →L[ℝ] E') {y₀ x : E} {ω : E' → E' [⋀^Fin (n + 1)]→L[ℝ] F} (hω : ContinuousOn ω (segment ℝ (A y₀) (A x))) : poincareHomotopy y₀ (fun (y : E) => (ω (A y)).compContinuousLinearMap A) x = (poincareHomotopy (A y₀) ω (A x)).compContinuousLinearMap A

Naturality of the Poincaré homotopy operator. Contracting the pullback of a form along a continuous linear map A along the rays from y₀ is the same as pulling back the contraction of the form along the rays from A y₀. In particular, if A fixes the centre, the operator commutes with pullback along A.

theorem StarConvex.compContinuousLinearMap_poincareHomotopy_eq {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} {x₀ : E} {s : Set E} {ω : E → E [⋀^Fin (n + 1)]→L[ℝ] F} (hs : StarConvex ℝ x₀ s) (hωc : ContinuousOn ω s) {A : E →L[ℝ] E} (hAx₀ : A x₀ = x₀) (hAs : Set.MapsTo (⇑A) s s) (hω : ∀ y ∈ s, (ω (A y)).compContinuousLinearMap A = ω y) {x : E} (hx : x ∈ s) : (TauCeti.poincareHomotopy x₀ ω (A x)).compContinuousLinearMap A = TauCeti.poincareHomotopy x₀ ω x

The Poincaré homotopy operator preserves invariance. Let A be a continuous linear map fixing x₀ and mapping a set s, star-convex with respect to x₀, into itself. If a form ω, continuous on s, satisfies A^* ω = ω on s, then so does its Poincaré homotopy operator centred at x₀.

theorem StarConvex.contDiffOn_poincareHomotopy {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} {x₀ : E} {s : Set E} {ω : E → E [⋀^Fin (n + 1)]→L[ℝ] F} (hs : StarConvex ℝ x₀ s) (hso : IsOpen s) {r : ℕ∞} (hω : ContDiffOn ℝ (↑r) ω s) : ContDiffOn ℝ (↑r) (TauCeti.poincareHomotopy x₀ ω) s

The Poincaré homotopy operator of a C^r form on an open star-convex set is C^r there.

theorem StarConvex.extDeriv_poincareHomotopy_add_poincareHomotopy_extDeriv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} {x₀ : E} {s : Set E} {ω : E → E [⋀^Fin (n + 1)]→L[ℝ] F} [CompleteSpace F] (hs : StarConvex ℝ x₀ s) (hso : IsOpen s) (hω : ContDiffOn ℝ 1 ω s) {x : E} (hx : x ∈ s) : extDeriv (TauCeti.poincareHomotopy x₀ ω) x + TauCeti.poincareHomotopy x₀ (extDeriv ω) x = ω x

The homotopy formula d (K ω) + K (d ω) = ω for the Poincaré homotopy operator K of a C¹ form on an open set star-convex with respect to the centre of K.

theorem StarConvex.extDeriv_poincareHomotopy {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} {x₀ : E} {s : Set E} {ω : E → E [⋀^Fin (n + 1)]→L[ℝ] F} [CompleteSpace F] (hs : StarConvex ℝ x₀ s) (hso : IsOpen s) (hω : ContDiffOn ℝ 1 ω s) (hclosed : ∀ y ∈ s, extDeriv ω y = 0) {x : E} (hx : x ∈ s) : extDeriv (TauCeti.poincareHomotopy x₀ ω) x = ω x

The Poincaré lemma. On an open set star-convex with respect to x₀, the Poincaré homotopy operator with centre x₀ of a closed C¹ form is a primitive of it.

theorem StarConvex.exists_contDiffOn_forall_extDeriv_eq {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} {x₀ : E} {s : Set E} {ω : E → E [⋀^Fin (n + 1)]→L[ℝ] F} [CompleteSpace F] (hs : StarConvex ℝ x₀ s) (hso : IsOpen s) {r : ℕ∞} (hr : 1 ≤ r) (hω : ContDiffOn ℝ (↑r) ω s) (hclosed : ∀ y ∈ s, extDeriv ω y = 0) : ∃ (α : E → E [⋀^Fin n]→L[ℝ] F), ContDiffOn ℝ (↑r) α s ∧ α x₀ = 0 ∧ ∀ x ∈ s, extDeriv α x = ω x

The Poincaré lemma. A closed C^r form, r ≥ 1, on an open star-convex set is the exterior derivative of a C^r form, which can be chosen to vanish at the centre.

Convex sets that need not be open

On a convex set s with unique derivatives, such as a closed half-ball (the image of a boundary chart), derivatives are taken within s and the exterior derivative is extDerivWithin.

theorem Convex.contDiffOn_poincareHomotopy {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} {x₀ : E} {s : Set E} {ω : E → E [⋀^Fin (n + 1)]→L[ℝ] F} (hs : Convex ℝ s) (hsu : UniqueDiffOn ℝ s) (hx₀ : x₀ ∈ s) {r : ℕ∞} (hω : ContDiffOn ℝ (↑r) ω s) : ContDiffOn ℝ (↑r) (TauCeti.poincareHomotopy x₀ ω) s

The Poincaré homotopy operator of a C^r form on a convex set with unique derivatives, with centre in that set, is C^r there.

theorem Convex.extDerivWithin_poincareHomotopy_add_poincareHomotopy_extDerivWithin {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} {x₀ : E} {s : Set E} {ω : E → E [⋀^Fin (n + 1)]→L[ℝ] F} [CompleteSpace F] (hs : Convex ℝ s) (hsu : UniqueDiffOn ℝ s) (hx₀ : x₀ ∈ s) (hω : ContDiffOn ℝ 1 ω s) {x : E} (hx : x ∈ s) : extDerivWithin (TauCeti.poincareHomotopy x₀ ω) s x + TauCeti.poincareHomotopy x₀ (extDerivWithin ω s) x = ω x

The homotopy formula d (K ω) + K (d ω) = ω, with exterior derivatives within s, for the Poincaré homotopy operator K of a C¹ form on a convex set s with unique derivatives, whose centre lies in s.

theorem Convex.extDerivWithin_poincareHomotopy {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} {x₀ : E} {s : Set E} {ω : E → E [⋀^Fin (n + 1)]→L[ℝ] F} [CompleteSpace F] (hs : Convex ℝ s) (hsu : UniqueDiffOn ℝ s) (hx₀ : x₀ ∈ s) (hω : ContDiffOn ℝ 1 ω s) (hclosed : ∀ y ∈ s, extDerivWithin ω s y = 0) {x : E} (hx : x ∈ s) : extDerivWithin (TauCeti.poincareHomotopy x₀ ω) s x = ω x

The relative Poincaré lemma. On a convex set with unique derivatives, the Poincaré homotopy operator, centred in the set, of a form closed within the set is a primitive of it within the set.

theorem Convex.exists_contDiffOn_forall_extDerivWithin_eq {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} {x₀ : E} {s : Set E} {ω : E → E [⋀^Fin (n + 1)]→L[ℝ] F} [CompleteSpace F] (hs : Convex ℝ s) (hsu : UniqueDiffOn ℝ s) (hx₀ : x₀ ∈ s) {r : ℕ∞} (hr : 1 ≤ r) (hω : ContDiffOn ℝ (↑r) ω s) (hclosed : ∀ y ∈ s, extDerivWithin ω s y = 0) : ∃ (α : E → E [⋀^Fin n]→L[ℝ] F), ContDiffOn ℝ (↑r) α s ∧ α x₀ = 0 ∧ ∀ x ∈ s, extDerivWithin α s x = ω x

The relative Poincaré lemma. A C^r form, r ≥ 1, closed within a convex set with unique derivatives is the exterior derivative within the set of a C^r form, which can be chosen to vanish at any given point of the set. The set need not be open: a closed half-ball, the image of a boundary chart, is allowed.