The exterior derivative squares to zero

For a twice continuously differentiable fixed-coefficient differential form, the second exterior derivative vanishes. The relative theorem applies to subsets with unique derivatives that are contained in the closure of their interior. The unrestricted theorem therefore includes manifolds with boundary and corners and needs neither finite dimensionality nor completeness.

The unbundled results assume C² section regularity; differentiability of the exterior derivative is not a separate hypothesis. A simp theorem gives the square-zero identity for bundled smooth forms, and TauCeti.mextDerivₗ_comp_mextDerivₗ gives the identity for the bundled linear maps.

References

• John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Chapter 14.
• Mathlib's flat square-zero theorem (extDerivWithin_extDerivWithin_apply).

theorem TauCeti.mextDerivWithin_mextDerivWithin {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] {k : ℕ} [IsManifold I 2 M] (φ : RoughForm I M F k) {s : Set M} (hφ : ContMDiffOn I (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin k]→L[ℝ] F))) 2 (fun (y : M) => ⟨y, φ y⟩) s) (hs : UniqueMDiff[s]) (hsc : s ⊆ closure (interior s)) {x : M} (hx : x ∈ s) : mextDerivWithin (mextDerivWithin φ s) s x = 0

The exterior derivative within a subset squares to zero for a C² section. The subset has unique derivatives and is contained in the closure of its interior.

theorem TauCeti.mextDeriv_mextDeriv {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] {k : ℕ} [IsManifold I 2 M] (φ : RoughForm I M F k) (hφ : IsSmoothBundleForm I F (Bundle.Trivial M F) 2 φ) : mextDeriv (mextDeriv φ) = 0

The exterior derivative squares to zero on twice continuously differentiable fixed-coefficient forms, over any model with corners.

@[simp]

theorem TauCeti.SmoothForm.mextDeriv_mextDeriv {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] {k : ℕ} [IsManifold I 2 M] (φ : SmoothForm I M F k) : mextDeriv (mextDeriv ↑φ) = 0

In particular, the second exterior derivative of a bundled smooth form vanishes.

@[simp]

theorem TauCeti.mextDeriv_mextDeriv_ofFunction {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] [IsManifold I 2 M] {f : M → F} (hf : ContMDiff I (modelWithCornersSelf ℝ F) 2 f) : mextDeriv (mextDeriv (RoughForm.ofFunction I f)) = 0

The second exterior derivative of the 0-form of a C² function vanishes.

@[simp]

theorem TauCeti.mextDerivₗ_comp_mextDerivₗ {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] [IsManifold I 2 M] (k : ℕ) : mextDerivₗ I (k + 1) ∘ₗ mextDerivₗ I k = 0

Successive exterior derivatives compose to zero as linear maps.