The homotopy operator on a cylinder over a subset of a normed space #

Let ω : E × ℝ → (E × ℝ) [⋀^Fin (n + 1)]→L[ℝ] F be a differential (n + 1)-form on the product of a real normed space E with the time line. The cylinder homotopy operator (TauCeti.cylinderHomotopy) contracts ω with the unit time vector ∂ₜ = (0, 1) and integrates the result over the time interval [0, 1]:

(h ω)(x)(v₁, …, vₙ) = ∫₀¹ ω(x, t)(∂ₜ, v₁, …, vₙ) dt,

where each vᵢ ∈ E is viewed in E × ℝ through ContinuousLinearMap.inl. Writing ιₜ^* ω = x ↦ (ω (x, t)).compContinuousLinearMap (.inl ℝ E ℝ) for the pullback of ω along the slice x ↦ (x, t), the operator satisfies the cochain-homotopy identity

d (h ω) + h (d ω) = ι₁^* ω - ι₀^* ω.

Everything is relative to a cylinder s ×ˢ Icc 0 1: the form only needs to be C¹ on it, and the exterior derivatives are taken within it (and within s for h ω). The base s is a convex set with unique derivatives that need not be open, such as a closed half-ball, the local shape of the image of a boundary chart of a manifold with boundary; the time direction always has boundary. Convexity is what Mathlib's mean value inequality needs to differentiate under the integral within s. In degree zero the identity reduces to the fundamental theorem of calculus h (d f) = ι₁^* f - ι₀^* f (TauCeti.cylinderHomotopy_extDerivWithin_eq_sub), which needs no convexity.

The proof differentiates under the integral sign and uses the fundamental theorem of calculus in the time variable. Pointwise, the derivative terms combine through the constant-coefficient Cartan formula ContinuousAlternatingMap.alternatizeUncurryFin_curryLeft_comp_add_curryLeft for the vector ∂ₜ, pulled back along inl by ContinuousAlternatingMap.alternatizeUncurryFin_compContinuousLinearMap, into the time derivative of ιₜ^* ω.

This is the chart-level form of the homotopy operator on forms on M × [0, 1] for a manifold M with or without boundary, the analytic input for homotopy invariance of de Rham cohomology. It is proved directly, without Stokes' theorem on the manifold with corners M × [0, 1].

Main declarations #

TauCeti.cylinderHomotopy: the cylinder homotopy operator.
Convex.contDiffOn_cylinderHomotopy, TauCeti.contDiff_cylinderHomotopy: it preserves C^r regularity.
Convex.extDerivWithin_cylinderHomotopy_add_cylinderHomotopy_extDerivWithin: the cochain-homotopy identity d (h ω) + h (d ω) = ι₁^* ω - ι₀^* ω.
Convex.extDerivWithin_cylinderHomotopy: for a closed form, ι₁^* ω - ι₀^* ω = d (h ω).
TauCeti.cylinderHomotopy_extDerivWithin_eq_sub: the degree-zero case h (d f) = ι₁^* f - ι₀^* f.
TauCeti.extDeriv_cylinderHomotopy_add_cylinderHomotopy_extDeriv, TauCeti.cylinderHomotopy_extDeriv_eq_sub: the same identities for forms C¹ on all of E × ℝ, with exterior derivatives on the whole spaces.
TauCeti.support_cylinderHomotopy_subset, TauCeti.tsupport_cylinderHomotopy_subset, TauCeti.norm_cylinderHomotopy_le, TauCeti.norm_iteratedFDeriv_cylinderHomotopy_le: support and sup-norm bounds for h ω and its derivatives, which make h continuous on compactly supported smooth forms.

References #

John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Chapter 17, section Homotopy Invariance, whose homotopy operator on M × [0, 1] is the manifold version of this one.
R. Bott and L. W. Tu, Differential Forms in Algebraic Topology, GTM 82, §4 (the homotopy operator K of the Poincaré lemma, integration along the fibre of M × ℝ → M).