Naturality of the manifold exterior derivative

Pullback by a twice continuously differentiable map commutes with the exterior derivative of a continuously differentiable fixed-coefficient form. The pointwise and on-set forms expose the local hypotheses needed by later constructions, while the global theorem is the cochain-map law used by de Rham cohomology; in particular pullback preserves closed forms (TauCeti.IsSmoothForm.mextDeriv_mpullback_eq_zero).

For a map from a subset s of a normed space, such as a cylinder s ×ˢ Icc 0 1 or a simplex, the within-set pullback commutes with the flat exterior derivative within s (TauCeti.extDerivWithin_mpullbackWithin). This is how flat constructions on non-open parameter domains are compared with the manifold exterior derivative.

References

• John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Proposition 14.26.
• Mathlib's extDerivWithin_pullback.

theorem TauCeti.mpullback_mextDeriv_ofFunction_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} {F : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace M'] [ChartedSpace H' M'] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : M → M'} {x : M} (hf : MDiffAt f x) {g : M' → F} (hg : MDiffAt g (f x)) : mpullback I I' f (mextDeriv (RoughForm.ofFunction I' g)) x = mextDeriv (RoughForm.ofFunction I (g ∘ f)) x

At a point where f and g are differentiable, pullback by f of the exterior derivative of g is the exterior derivative of the composite.

theorem TauCeti.mpullback_mextDeriv_ofFunction {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} {F : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace M'] [ChartedSpace H' M'] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : M → M'} (hf : MDiff f) {g : M' → F} (hg : MDiff g) : mpullback I I' f (mextDeriv (RoughForm.ofFunction I' g)) = mextDeriv (RoughForm.ofFunction I (g ∘ f))

Pullback by a differentiable map of the exterior derivative of a differentiable function is the exterior derivative of the composite.

theorem TauCeti.SmoothForm.mpullback_realLineCoordForm {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] (h : M → ℝ) : TauCeti.mpullback I (modelWithCornersSelf ℝ ℝ) h ↑realLineCoordForm = mextDeriv (RoughForm.ofFunction I h)

The pullback of the coordinate one-form dz of the real line along a real function h is the differential dh.

theorem TauCeti.mpullback_mextDeriv_at {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} {F : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace M'] [ChartedSpace H' M'] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [IsManifold I 2 M] [IsManifold I' 2 M'] {x : M} {f : M → M'} (hf : ContMDiffAt I I' 2 f x) {φ : RoughForm I' M' F k} (hφ : ContMDiffAt I' (I'.prod (modelWithCornersSelf ℝ (E' [⋀^Fin k]→L[ℝ] F))) 1 (fun (y : M') => ⟨y, φ y⟩) (f x)) : mpullback I I' f (mextDeriv φ) x = mextDeriv (mpullback I I' f φ) x

At a point, pullback commutes with the exterior derivative.

theorem TauCeti.mpullback_mextDeriv_on {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} {F : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace M'] [ChartedSpace H' M'] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [IsManifold I 2 M] [IsManifold I' 2 M'] {f : M → M'} {s : Set M} (hf : ∀ x ∈ s, ContMDiffAt I I' 2 f x) {φ : RoughForm I' M' F k} (hφ : ∀ x ∈ s, ContMDiffAt I' (I'.prod (modelWithCornersSelf ℝ (E' [⋀^Fin k]→L[ℝ] F))) 1 (fun (y : M') => ⟨y, φ y⟩) (f x)) (x : M) : x ∈ s → mpullback I I' f (mextDeriv φ) x = mextDeriv (mpullback I I' f φ) x

On a set, pullback commutes pointwise with the exterior derivative.

theorem TauCeti.mpullback_mextDeriv {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} {F : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace M'] [ChartedSpace H' M'] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [IsManifold I 2 M] [IsManifold I' 2 M'] {f : M → M'} (hf : ContMDiff I I' 2 f) {φ : RoughForm I' M' F k} (hφ : IsSmoothBundleForm I' F (Bundle.Trivial M' F) 1 φ) : mpullback I I' f (mextDeriv φ) = mextDeriv (mpullback I I' f φ)

Pullback by a C² map commutes with the exterior derivative of a C¹ form.

theorem TauCeti.IsSmoothForm.mextDeriv_mpullback_eq_zero {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} {F : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace M'] [ChartedSpace H' M'] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [IsManifold I 2 M] [IsManifold I' 2 M'] {θ : RoughForm I' M' F k} (hθ : IsSmoothForm I' 1 θ) (hclosed : mextDeriv θ = 0) {f : M → M'} (hf : ContMDiff I I' 2 f) : mextDeriv (TauCeti.mpullback I I' f θ) = 0

The pullback of a closed C¹ form along a C² map is closed.

theorem TauCeti.extDerivWithin_mpullbackWithin {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} [IsManifold I 2 M] {E'' : Type u_8} [NormedAddCommGroup E''] [NormedSpace ℝ E''] {f : E'' → M} {s : Set E''} {z : E''} (hf : ContMDiffWithinAt (modelWithCornersSelf ℝ E'') I 2 f s z) (hs : UniqueDiffOn ℝ s) (hzc : z ∈ closure (interior s)) (hz : z ∈ s) {φ : RoughForm I M F k} (hφ : (MDiffAt fun (y : M) => ⟨y, φ y⟩) (f z)) : extDerivWithin (mpullbackWithin (modelWithCornersSelf ℝ E'') I f s φ) s z = mpullbackWithin (modelWithCornersSelf ℝ E'') I f s (mextDeriv φ) z

Pullback within a subset s of a normed space, along a map that is C² within s, commutes with exterior differentiation: the flat exterior derivative within s of the pulled-back form is the pullback of the manifold exterior derivative. The set s has unique derivatives and the point lies in the closure of its interior, as for extDerivWithin_pullback; it need not be open.

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

The bundled exterior derivative commutes with smooth pullback.