The constancy theorem for top-degree currents

Let E be a real vector space of finite dimension m with an orientation o, and let Ω be a connected open subset of E. A top-degree current on Ω is a continuous linear functional T on the test m-forms 𝓓(Ω, E [⋀^Fin m]→L[ℝ] ℝ), and its boundary is ∂T = T ∘ d. The constancy theorem says that if ∂T = 0, then T = c • [[Ω]] for a unique real constant c, where [[Ω]] is the oriented integration current Orientation.integrationCurrent o Ω. Conversely [[Ω]] has zero boundary, so this characterizes the top-degree currents without boundary on a connected open set. No order-zero or finite-mass assumption is made on T.

In degree zero the space E is a point, the boundary condition is vacuous (the current complex is zero in negative degrees), and every 0-current on the connected set Ω = E is a multiple of the Dirac current [[Ω]]. Restricting a current without boundary to a connected open subset U of an arbitrary open set Ω gives the local form: on each such U, T is a constant multiple of [[U]]. A current on a disconnected open set may have different constants on different components.

The proof reduces to scalar distributions. Fix a basis b of orientation o, so that [[Ω]] ω = ∫ x, ω x b ∂b.addHaar. The scalar distribution g ↦ T (g • det_b) has vanishing derivatives when ∂T = 0 (TestFunction.map_postcompCLM_toSpanSingleton_lineDerivOp_eq_zero), so it is integration against a unique constant c (Distribution.existsUnique_eq_ofFun_const_of_forall_lineDerivOp_eq_zero). Since every top-degree test form is g • det_b for the scalar test g = ω (·) b (Module.Basis.testTopFormEquiv), this says T = c • [[Ω]].

Main declarations

• Orientation.existsUnique_eq_smul_integrationCurrent_of_comp_extDerivCLM_eq_zero: a top-degree current with zero boundary on a connected open set is a unique constant multiple of the integration current.
• Orientation.comp_extDerivCLM_eq_zero_iff: zero boundary characterizes these multiples.
• Orientation.existsUnique_comp_monoCLM_eq_smul_integrationCurrent: the local form, on connected open subsets of an arbitrary open set.
• Orientation.existsUnique_eq_smul_integrationCurrent_of_finrank_eq_zero: the degree-zero case.

References

• H. Federer, Geometric Measure Theory, §4.1.7 (constancy theorem).
• L. Simon, Introduction to Geometric Measure Theory, Chapter 6, Theorem 2.1.

theorem Orientation.existsUnique_eq_smul_integrationCurrent_of_comp_extDerivCLM_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {Ω : TopologicalSpace.Opens E} {k : ℕ} (o : Orientation ℝ E (Fin (k + 1))) (hE : Module.finrank ℝ E = k + 1) (hΩ : IsConnected ↑Ω) {T : TestFunction Ω (E [⋀^Fin (k + 1)]→L[ℝ] ℝ) ⊤ →L[ℝ] ℝ} (hT : T ∘SL TestFunction.extDerivCLM = 0) : ∃! c : ℝ, T = c • o.integrationCurrent Ω

The constancy theorem. On a connected open subset Ω of an oriented real vector space of dimension k + 1, a top-degree current with zero boundary, T ∘ d = 0, is a unique real multiple of the oriented integration current [[Ω]].

theorem Orientation.comp_extDerivCLM_eq_zero_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {Ω : TopologicalSpace.Opens E} {k : ℕ} (o : Orientation ℝ E (Fin (k + 1))) (hE : Module.finrank ℝ E = k + 1) (hΩ : IsConnected ↑Ω) (T : TestFunction Ω (E [⋀^Fin (k + 1)]→L[ℝ] ℝ) ⊤ →L[ℝ] ℝ) : T ∘SL TestFunction.extDerivCLM = 0 ↔ ∃! c : ℝ, T = c • o.integrationCurrent Ω

On a connected open subset of an oriented real vector space of dimension k + 1, a top-degree current has zero boundary if and only if it is a (necessarily unique) real multiple of the oriented integration current.

theorem Orientation.existsUnique_comp_monoCLM_eq_smul_integrationCurrent {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {Ω U : TopologicalSpace.Opens E} {k : ℕ} (o : Orientation ℝ E (Fin (k + 1))) (hE : Module.finrank ℝ E = k + 1) {T : TestFunction Ω (E [⋀^Fin (k + 1)]→L[ℝ] ℝ) ⊤ →L[ℝ] ℝ} (hT : T ∘SL TestFunction.extDerivCLM = 0) (hUc : IsConnected ↑U) : ∃! c : ℝ, T ∘SL TestFunction.monoCLM ℝ = c • o.integrationCurrent U

The local constancy theorem. A top-degree current with zero boundary on an arbitrary open subset Ω of an oriented real vector space of dimension k + 1 restricts, on every connected open subset U ⊆ Ω, to a unique real multiple of the integration current [[U]]. (If U ⊄ Ω the restriction map monoCLM is zero, and the multiple is 0.)

theorem Orientation.existsUnique_eq_smul_integrationCurrent_of_finrank_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {Ω : TopologicalSpace.Opens E} (o : Orientation ℝ E (Fin 0)) (hE : Module.finrank ℝ E = 0) (hΩ : IsConnected ↑Ω) (T : TestFunction Ω (E [⋀^Fin 0]→L[ℝ] ℝ) ⊤ →L[ℝ] ℝ) : ∃! c : ℝ, T = c • o.integrationCurrent Ω

The constancy theorem in degree zero. On a zero-dimensional oriented real vector space every 0-current on a connected open set, which is then the whole point, is a unique real multiple of the integration current, the signed Dirac current at the origin. No boundary condition enters: the boundary of a 0-current is zero.