Spivak Thm 4-11 (proof): homotopy formula dK + Kd = id

Open

ContWeatherall.homotopy_formula

by Alien60 · Oct 14, 2026 · Mathlib 0df444a (Lean v4.33.1)

category-theorydifferential-formsgauge-theoryphilosophy-of-physicspoincare-lemma

Throughout, $E$ is a real normed space, $F$ a real normed space (Banach where stated), forms are Mathlib's E → E [⋀^Fin k]→L[ℝ] F, $d$ is extDeriv ( $d\omega(x)(v_0,\dots,v_k)=\sum_i(-1)^iD\omega(x)(v_i)(v_0,\dots,\widehat{v_i},\dots,v_k)$ ), smooth means ContDiff ℝ ∞, and $(K\omega)(x)(v)=\int_0^1t^k\,\omega(tx)(x,v)\,dt$ for a $(k+1)$ -form $\omega$ . If $F$ is complete and $\omega$ is a smooth form of degree $k+1\ge1$ , then $d(K\omega)+K(d\omega)=\omega$ .

Preamble

import Mathlib
import Definitions.Def_ContWeatherall_defs

open CategoryTheory ContinuousAlternatingMap
open scoped ContDiff

Formal statement

namespace ContWeatherall

/-- The homotopy formula `d K + K d = id` on smooth forms of degree `k + 1 ≥ 1`. -/
theorem homotopy_formula {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {k : ℕ} {w : E → E [⋀^Fin (k + 1)]→L[ℝ] F}
    (hw : ContDiff ℝ ∞ w) : extDeriv (homotopyOp w) + homotopyOp (extDeriv w) = w := by
  sorry

end ContWeatherall

Source

M. Spivak, Calculus on Manifolds (W. A. Benjamin, 1965), Theorem 4-11 (Poincaré lemma) and its proof (the identity ω = d(Iω) + I(dω))

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Let $E,F$ be real normed spaces with $F$ complete, $k\in\mathbb{N}$ , and $w:E\to\mathrm{Alt}^{k+1}(E;F)$ smooth. Then, as functions $E\to\mathrm{Alt}^{k+1}(E;F)$ ,

d(Kw)+K(dw)=w,

where $K$ is applied to the $(k+1)$ -form $w$ (giving a $k$ -form, to which $d$ is applied) and to the $(k+2)$ -form $dw$ (giving a $(k+1)$ -form), and $d$ has the convention above: $(d\omega)(x)(v_0,\dots,v_m)=\sum_i(-1)^i(D\omega(x)v_i)(\dots\widehat{v_i}\dots)$ .

View graph