The exterior derivative of test forms

For an open set Ω of a real normed space E, a test k-form on Ω with coefficients in F is a test function ω ∈ 𝓓(Ω, E [⋀^Fin k]→L[ℝ] F): a smooth compactly supported k-form whose support lies in Ω. This file packages Mathlib's exterior derivative extDeriv of differential forms on normed spaces as a continuous linear map between test forms, in the style of Mathlib's TestFunction.fderivCLM.

Test forms are the Euclidean chart model of the test forms acted on by currents: a k-current on Ω is a continuous linear functional T on test k-forms, and its boundary is the transpose ∂T = T ∘ d of this exterior derivative. The identity d ∘ d = 0 gives ∂ ∘ ∂ = 0.

In degree k + 1 ≥ dim E, the interior product ι_y α of a constant form α times a scalar test function g has exterior derivative ∂_y g • α. Consequently, if a continuous linear functional T on test (k + 1)-forms annihilates every exact test form, then the scalar distribution g ↦ T (g • α) has vanishing distributional derivatives in every direction. This is the step that reduces the constancy theorem for top-degree currents without boundary to the constancy of scalar distributions whose derivatives all vanish.

Main declarations

• TestFunction.extDerivCLM: the exterior derivative 𝓓(Ω, Λᵏ) →L[ℝ] 𝓓(Ω, Λᵏ⁺¹).
• TestFunction.extDerivCLM_apply: pointwise, it is Mathlib's extDeriv.
• TestFunction.extDerivCLM_extDerivCLM: d (d ω) = 0.
• TestFunction.extDerivCLM_monoCLM: the exterior derivative commutes with extending a test form from Ω' to a larger open set Ω.
• ContinuousLinearMap.comp_monoCLM_comp_extDerivCLM: restricting a current to an open subset commutes with the boundary.
• TestFunction.extDerivCLM_postcompCLM_toSpanSingleton_curryLeft: the top-degree formula d (g • ι_y α) = ∂_y g • α.
• TestFunction.map_postcompCLM_toSpanSingleton_lineDerivOp_eq_zero: a functional on top-degree test forms annihilating exact forms induces scalar distributions with vanishing derivatives.

References

• H. Federer, Geometric Measure Theory, §4.1.7.
• L. Simon, Introduction to Geometric Measure Theory, Chapter 6, §1.

noncomputable def TestFunction.extDerivCLM {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {k : ℕ} : TestFunction Ω (E [⋀^Fin k]→L[ℝ] F) ⊤ →L[ℝ] TestFunction Ω (E [⋀^Fin (k + 1)]→L[ℝ] F) ⊤

The exterior derivative of test k-forms on Ω with coefficients in F, as a continuous linear map into the test (k + 1)-forms. It is the alternatization ContinuousAlternatingMap.alternatizeUncurryFinCLM of the Fréchet derivative TestFunction.fderivCLM, so pointwise it is Mathlib's extDeriv.

@[simp]

theorem TestFunction.extDerivCLM_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {k : ℕ} (ω : TestFunction Ω (E [⋀^Fin k]→L[ℝ] F) ⊤) (x : E) : (extDerivCLM ω) x = extDeriv (⇑ω) x

The exterior derivative of a test form is pointwise its exterior derivative as a differential form.

theorem TestFunction.coe_extDerivCLM {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {k : ℕ} (ω : TestFunction Ω (E [⋀^Fin k]→L[ℝ] F) ⊤) : ⇑(extDerivCLM ω) = extDeriv ⇑ω

The exterior derivative of a test form, as a function, is its exterior derivative as a differential form.

@[simp]

theorem TestFunction.extDerivCLM_extDerivCLM {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {k : ℕ} (ω : TestFunction Ω (E [⋀^Fin k]→L[ℝ] F) ⊤) : extDerivCLM (extDerivCLM ω) = 0

d ∘ d = 0 on test forms.

@[simp]

theorem TestFunction.extDerivCLM_comp_extDerivCLM {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {k : ℕ} : extDerivCLM ∘SL extDerivCLM = 0

d ∘ d = 0 on test forms, as an identity of continuous linear maps.

theorem TestFunction.tsupport_extDerivCLM_subset {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {k : ℕ} (ω : TestFunction Ω (E [⋀^Fin k]→L[ℝ] F) ⊤) : tsupport ⇑(extDerivCLM ω) ⊆ tsupport ⇑ω

The exterior derivative does not enlarge the support of a test form.

@[simp]

theorem TestFunction.extDerivCLM_monoCLM {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω Ω' : TopologicalSpace.Opens E} {k : ℕ} (ω : TestFunction Ω' (E [⋀^Fin k]→L[ℝ] F) ⊤) : extDerivCLM ((monoCLM ℝ) ω) = (monoCLM ℝ) (extDerivCLM ω)

The exterior derivative of a test form extended from Ω' to a larger open set Ω is the extension of its exterior derivative. If Ω' ⊄ Ω both sides are 0, since monoCLM is then the zero map.

theorem TestFunction.extDerivCLM_postcompCLM_constOfIsEmptyLIE {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} (f : TestFunction Ω F ⊤) : extDerivCLM ((postcompCLM ↑↑(ContinuousAlternatingMap.constOfIsEmptyLIE ℝ E F (Fin 0))) f) = (postcompCLM ↑↑(ContinuousAlternatingMap.ofSubsingletonLIE 0)) ((fderivCLM ℝ ⊤ ⊤) f)

In degree zero, the exterior derivative of the 0-form with values f is the 1-form Df.

theorem TestFunction.extDerivCLM_postcompCLM_toSpanSingleton_curryLeft {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {k : ℕ} [FiniteDimensional ℝ E] (hk : Module.finrank ℝ E ≤ k + 1) (α : E [⋀^Fin (k + 1)]→L[ℝ] F) (y : E) (g : TestFunction Ω ℝ ⊤) : extDerivCLM ((postcompCLM (ContinuousLinearMap.toSpanSingleton ℝ (α.curryLeft y))) g) = (postcompCLM (ContinuousLinearMap.toSpanSingleton ℝ α)) (LineDeriv.lineDerivOp y g)

The exterior derivative in top degree. If dim E ≤ k + 1, then for a constant (k + 1)-form α, a vector y and a scalar test function g, the test k-form g • ι_y α has exterior derivative ∂_y g • α. Here ι_y α = α.curryLeft y is the interior product.

theorem TestFunction.map_postcompCLM_toSpanSingleton_lineDerivOp_eq_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {k : ℕ} [FiniteDimensional ℝ E] {G : Type u_3} [AddCommGroup G] [Module ℝ G] [TopologicalSpace G] {T : TestFunction Ω (E [⋀^Fin (k + 1)]→L[ℝ] F) ⊤ →L[ℝ] G} (hT : T ∘SL extDerivCLM = 0) (hk : Module.finrank ℝ E ≤ k + 1) (α : E [⋀^Fin (k + 1)]→L[ℝ] F) (y : E) (g : TestFunction Ω ℝ ⊤) : T ((postcompCLM (ContinuousLinearMap.toSpanSingleton ℝ α)) (LineDeriv.lineDerivOp y g)) = 0

A continuous linear functional T on test (k + 1)-forms, dim E ≤ k + 1, that annihilates every exact test form (that is, a top-degree current with zero boundary T ∘ d = 0) annihilates ∂_y g • α for every constant (k + 1)-form α, vector y and scalar test function g. Thus the scalar distribution g ↦ T (g • α) has vanishing distributional derivatives.

theorem ContinuousLinearMap.comp_monoCLM_comp_extDerivCLM {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [AddCommGroup G] [Module ℝ G] [TopologicalSpace G] {Ω Ω' : TopologicalSpace.Opens E} {k : ℕ} (T : TestFunction Ω (E [⋀^Fin (k + 1)]→L[ℝ] F) ⊤ →L[ℝ] G) : (T ∘SL TestFunction.monoCLM ℝ) ∘SL TestFunction.extDerivCLM = (T ∘SL TestFunction.extDerivCLM) ∘SL TestFunction.monoCLM ℝ

Restriction commutes with the boundary: for a current T on Ω and an open subset Ω' ⊆ Ω, the boundary of the restriction T ∘ monoCLM of T to Ω' is the restriction of the boundary ∂ T = T ∘ d.