Topological support of rough differential forms #
This file establishes how the topological support of a rough differential form behaves under
scalar multiplication, pullback, exterior differentiation and finite partition localization.
Pullback along a continuous open map with invertible derivative carries the support to its
preimage.
A form supported in the source of an open partial homeomorphism e and agreeing there with the
pullback of φ along a map that coincides with e on that source has its support carried by e
into that of φ, and compact when the support of φ is compact and lies in the target of e.
Locality of the exterior derivative
preserves support and compact support without any regularity assumption. A rough form is a dependent
function whose fibre at x is
TangentSpace I x [⋀^Fin k]→L[ℝ] F, so Mathlib's tsupport is used with the model-space codomain
E [⋀^Fin k]→L[ℝ] F supplied explicitly.
A locally finite partition of unity has only finitely many terms meeting a compact form support. The weights give a finite decomposition; containment in charts requires subordination separately. Extension by zero in a chart preserves compact support when the form is supported inside that chart; on its target the extension has the same germ within the model range.
Scalar multiplication does not enlarge the support of a rough form.
Multiplication by a nonzero constant preserves the support of a rough form.
A point lies in the support of a rough form, taken with the model-space codomain
E [⋀^Fin k]→L[ℝ] F, exactly when the form is nonzero in the tangent fibre there.
The zero form has compact topological support.
The sum of two forms with compact topological support has compact topological support.
The topological support of a pullback is contained in the preimage of the original support.
Pullback by a proper map preserves compact topological support.
Along a continuous open map whose manifold derivative is invertible at every point, for instance a homeomorphism or an open embedding, the topological support of a pullback is the preimage of the support of the form.
Let e be an open partial homeomorphism agreeing with a map f on its source. A form ψ
supported in the source of e that agrees there with f^*φ has its support carried by e into
the support of φ.
Let e be an open partial homeomorphism agreeing with a map f on its source, and let φ be
a form with compact support in the target of e. A form ψ supported in the source of e that
agrees there with f^*φ has compact support: a closed subset of the image of the support of φ
under the inverse of e.
Locality of the actual exterior derivative prevents enlargement of a form's support. No regularity assumption is needed.
Compact support is preserved by the actual exterior derivative, without a regularity assumption.
A partition of unity localizes any compactly supported rough form into finitely many actual terms. All terms outside the chosen finite set vanish identically.
Weights summing to one on the support give an actual finite form decomposition.
The coordinate extension of a form supported inside a chart has support inside the compact coordinate image of the original support.
The zero extension of a compact chart-supported form has no support outside the target.
Compact support survives extension by zero from a chart containing the form's support.
On the target, extension by zero has the same germ within the model range as the original coordinate form.
The zero extension of a compact chart-supported form whose support avoids the boundary is supported inside the interior of the coordinate target.