Local naturality of the exterior derivative within a set

The exterior derivative commutes with pullback when the map sends the source set into the target set locally at the point. This version of Mathlib's extDerivWithin_pullback lets coordinate changes be used only on their chart overlaps, without conditions on their total extensions.

The source set can have boundary: it need only have unique derivatives and accumulate at the point from its interior. The latter condition guarantees symmetry of the second derivative.

References

• John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Chapter 14.

theorem TauCeti.extDerivWithin_pullback_of_preimage_mem_nhdsWithin {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {k : ℕ} {r : WithTop ℕ∞} {ω : F → F [⋀^Fin k]→L[𝕜] G} {f : E → F} {s : Set E} {t : Set F} {x : E} (hω : DifferentiableWithinAt 𝕜 ω t (f x)) (hf : ContDiffWithinAt 𝕜 r f s x) (hr : minSmoothness 𝕜 2 ≤ r) (hs : UniqueDiffOn 𝕜 s) (hxc : x ∈ closure (interior s)) (hxs : x ∈ s) (hst : f ⁻¹' t ∈ nhdsWithin x s) : extDerivWithin (fun (y : E) => (ω (f y)).compContinuousLinearMap (fderivWithin 𝕜 f s y)) s x = (extDerivWithin ω t (f x)).compContinuousLinearMap (fderivWithin 𝕜 f s x)

Exterior differentiation within a set commutes with pullback if the map sends that set into the target set near the base point. No condition is imposed away from that neighbourhood.