Regularity of the exterior derivative

The exterior derivative of a C^(r+1) form is C^r. The relative statements use UniqueDiffOn, not openness, so they apply to boundary and corner chart ranges. In particular, the exterior derivative preserves smooth fixed-coefficient forms. Neither the model space nor the coefficient space needs to be finite-dimensional or complete.

We use Mathlib's ContinuousAlternatingMap.alternatizeUncurryFinCLM: the exterior derivative is this continuous linear map applied to the derivative of the form. Thus regularity follows from the corresponding regularity of fderivWithin without a new alternatization construction.

References

• John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Chapter 14.

theorem TauCeti.contDiffWithinAt_extDerivWithin {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k : ℕ} {r p : WithTop ℕ∞} {ω : E → E [⋀^Fin k]→L[𝕜] F} {s : Set E} {x : E} (hω : ContDiffWithinAt 𝕜 p ω s x) (hs : UniqueDiffOn 𝕜 s) (hrp : r + 1 ≤ p) (hx : x ∈ s) : ContDiffWithinAt 𝕜 r (extDerivWithin ω s) s x

A C^p form has a C^r exterior derivative within a unique-differentiability set at a point of that set, provided r + 1 ≤ p.

theorem TauCeti.contDiffOn_extDerivWithin {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k : ℕ} {r p : WithTop ℕ∞} {ω : E → E [⋀^Fin k]→L[𝕜] F} {s : Set E} (hω : ContDiffOn 𝕜 p ω s) (hs : UniqueDiffOn 𝕜 s) (hrp : r + 1 ≤ p) : ContDiffOn 𝕜 r (extDerivWithin ω s) s

A C^p form on a unique-differentiability set has a C^r exterior derivative within that set, provided r + 1 ≤ p. This includes smooth forms by taking r = p = ∞.

theorem TauCeti.contDiffOn_extDerivWithin_succ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k : ℕ} {ω : E → E [⋀^Fin k]→L[𝕜] F} {s : Set E} {n : WithTop ℕ∞} (hs : UniqueDiffOn 𝕜 s) (hω : ContDiffOn 𝕜 (n + 1) ω s) : ContDiffOn 𝕜 n (extDerivWithin ω s) s

A C^(n+1) differential form has a C^n exterior derivative within a set with unique derivatives; this is contDiffOn_extDerivWithin with p = n + 1, and covers n = ∞ and n = ω.

theorem TauCeti.contDiffAt_extDeriv {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k : ℕ} {r p : WithTop ℕ∞} {ω : E → E [⋀^Fin k]→L[𝕜] F} {x : E} (hω : ContDiffAt 𝕜 p ω x) (hrp : r + 1 ≤ p) : ContDiffAt 𝕜 r (extDeriv ω) x

A C^p form has a C^r exterior derivative at a point, provided r + 1 ≤ p.

theorem TauCeti.contDiffOn_extDeriv {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k : ℕ} {r p : WithTop ℕ∞} {ω : E → E [⋀^Fin k]→L[𝕜] F} {s : Set E} (hω : ContDiffOn 𝕜 p ω s) (hs : IsOpen s) (hrp : r + 1 ≤ p) : ContDiffOn 𝕜 r (extDeriv ω) s

A C^p form on an open set has a C^r exterior derivative on that set, provided r + 1 ≤ p.

theorem TauCeti.continuousAt_extDeriv_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k : ℕ} {ω : E → E [⋀^Fin k]→L[𝕜] F} {x : E} (hω : ContDiffAt 𝕜 1 ω x) (v : Fin (k + 1) → E) : ContinuousAt (fun (y : E) => (extDeriv ω y) v) x

The exterior derivative of a form that is C¹ at x, evaluated on fixed vectors, is continuous at x.

theorem ContDiffAt.differentialForm_pullback {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k : ℕ} {r : WithTop ℕ∞} {x : E} {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → F} {η : F → F [⋀^Fin k]→L[𝕜] G} (hf : ContDiffAt 𝕜 (r + 1) f x) (hη : ContDiffAt 𝕜 r η (f x)) (hr : r = ⊤ → ↑k.factorial ≠ 0 := by intro h first | exact NeZero.ne _ | cases h) : ContDiffAt 𝕜 r (fun (y : E) => (η (f y)).compContinuousLinearMap (fderiv 𝕜 f y)) x

Pulling back a C^r differential form by a C^(r+1) map gives a C^r form at a point. Only the analytic order requires the arity factorial to be nonzero in the scalar field.

theorem TauCeti.contDiff_extDeriv {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {k : ℕ} {r p : WithTop ℕ∞} {ω : E → E [⋀^Fin k]→L[𝕜] F} (hω : ContDiff 𝕜 p ω) (hrp : r + 1 ≤ p) : ContDiff 𝕜 r (extDeriv ω)

A C^p form has a C^r exterior derivative, provided r + 1 ≤ p. In particular, the exterior derivative preserves smooth forms.