Closed smooth differential forms

Closedness is the vanishing of the generic manifold exterior derivative of a smooth form. This module also characterizes it by vanishing of the exterior derivatives of the chart expressions (and hence of ordinary extDeriv on the interior of any chart target, TauCeti.SmoothForm.IsClosed.extDeriv_inChartAt_eq_zero). It also restates closedness through the bundled derivative mextDerivₗ and shows that exterior derivatives are closed. The degree-two specialization in TwoForm.Closed supplies a constant-form convenience theorem. Since pullback commutes with the exterior derivative, smooth pullback sends closed forms to closed forms (TauCeti.SmoothForm.IsClosed.mpullback). The predicate and its generic API live here so they can be reused at every degree.

def TauCeti.SmoothForm.IsClosed {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [IsManifold I 1 M] (form : SmoothForm I M F k) : Prop

A smooth form is closed when the generic manifold exterior derivative vanishes.

theorem TauCeti.SmoothForm.isClosed_def {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [IsManifold I 1 M] (form : SmoothForm I M F k) : form.IsClosed ↔ mextDeriv ↑form = 0

Closedness is exactly the vanishing of the manifold exterior derivative.

theorem TauCeti.SmoothForm.isClosed_of_finrank_le {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [IsManifold I 1 M] [FiniteDimensional ℝ E] (h : Module.finrank ℝ E ≤ k) (form : SmoothForm I M F k) : form.IsClosed

On a manifold of finite dimension at most k, every smooth k-form is closed, since there are no nonzero (k + 1)-forms. In particular, top-degree forms are closed.

theorem TauCeti.SmoothForm.isClosed_iff_forall_mextDeriv_apply_eq_zero {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [IsManifold I 1 M] (form : SmoothForm I M F k) : form.IsClosed ↔ ∀ (x : M), mextDeriv (↑form) x = 0

Closedness can equivalently be checked pointwise on the exterior derivative.

theorem TauCeti.SmoothForm.isClosed_zero {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [IsManifold I 1 M] : IsClosed 0

The zero smooth form is closed.

theorem TauCeti.SmoothForm.IsClosed.add {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [IsManifold I 1 M] {form form' : SmoothForm I M F k} (h : form.IsClosed) (h' : form'.IsClosed) : (form + form').IsClosed

The sum of two closed smooth forms is closed.

theorem TauCeti.SmoothForm.IsClosed.smul {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [IsManifold I 1 M] {form : SmoothForm I M F k} {S : Type u_5} [Monoid S] [DistribMulAction S F] [ContinuousConstSMul S F] [SMulCommClass ℝ S F] (c : S) (h : form.IsClosed) : (c • form).IsClosed

A scalar multiple of a closed smooth form is closed, for any scalars acting continuously on the coefficients and commuting with the real action (for instance ℝ, or ℂ on complex-valued forms).

theorem TauCeti.SmoothForm.IsClosed.neg {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [IsManifold I 1 M] {form : SmoothForm I M F k} (h : form.IsClosed) : (-form).IsClosed

The negative of a closed smooth form is closed.

theorem TauCeti.SmoothForm.IsClosed.sub {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [IsManifold I 1 M] {form form' : SmoothForm I M F k} (h : form.IsClosed) (h' : form'.IsClosed) : (form - form').IsClosed

The difference of two closed smooth forms is closed.

theorem TauCeti.SmoothForm.isClosed_const {V : Type u_5} {F : Type u_6} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} (A : V [⋀^Fin k]→L[ℝ] F) : (const A).IsClosed

Constant forms on a model space are closed.

theorem TauCeti.SmoothForm.isClosed_realLineCoordForm : realLineCoordForm.IsClosed

The coordinate one-form dz of the real line is closed.

The statements below assume a C² manifold; the C¹ structure that SmoothForm and IsClosed ask for is derived from it.

theorem TauCeti.SmoothForm.isClosed_iff_forall_extDerivWithin_inChartAt_eq_zero {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [IsManifold I 2 M] (form : SmoothForm I M F k) : form.IsClosed ↔ ∀ (x₀ : M), ∀ z ∈ (extChartAt I x₀).target, extDerivWithin (RoughForm.inChartAt (↑form) x₀) (Set.range ↑I) z = 0

Closedness is equivalent to vanishing of the exterior derivative of every chart expression within the model range, at every point of the chart target.

theorem TauCeti.SmoothForm.IsClosed.extDeriv_inChartAt_eq_zero {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [IsManifold I 2 M] {form : SmoothForm I M F k} (h : form.IsClosed) (x₀ : M) {z : E} (hz : z ∈ interior (extChartAt I x₀).target) : extDeriv (RoughForm.inChartAt (↑form) x₀) z = 0

For a closed smooth form on a C² manifold, the ordinary flat exterior derivative extDeriv of its coordinate expression in any preferred chart vanishes on the interior of the chart target.

theorem TauCeti.SmoothForm.isClosed_iff_mextDerivₗ_eq_zero {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [IsManifold I 2 M] (form : SmoothForm I M F k) : form.IsClosed ↔ (mextDerivₗ I k) form = 0

Closedness is the vanishing of the bundled exterior derivative.

theorem TauCeti.SmoothForm.isClosed_mextDerivₗ {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [IsManifold I 2 M] (form : SmoothForm I M F k) : ((mextDerivₗ I k) form).IsClosed

The exterior derivative of a smooth form is closed.

theorem TauCeti.SmoothForm.IsClosed.mpullback {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [IsManifold I 2 M] {E' : Type u_5} {H' : Type u_6} {M' : Type u_7} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' 2 M'] {φ : SmoothForm I' M' F k} (hφ : φ.IsClosed) (f : M → M') (hf : ContMDiff I I' (↑⊤) f) : ((SmoothForm.mpullback f hf) φ).IsClosed

The smooth pullback of a closed form is closed.

theorem TauCeti.SmoothForm.isClosed_mpullback_iff_of_surjective {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [IsManifold I 2 M] {E' : Type u_5} {H' : Type u_6} {M' : Type u_7} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' 2 M'] {φ : SmoothForm I' M' F k} {f : M → M'} (hf : ContMDiff I I' (↑⊤) f) (hsurj : Function.Surjective f) (hdf : ∀ (x : M), Function.Surjective ⇑(mfderiv% f x)) : ((mpullback f hf) φ).IsClosed ↔ φ.IsClosed

Along a surjective smooth map whose derivatives are all surjective, a smooth form is closed exactly when its pullback is.