Change of chart for rough differential forms #
The coordinate expression of a rough form in two overlapping preferred charts is related by the
pullback along the coordinate change. Exterior differentiation within a manifold subset obeys
the same transport law, provided the subset has unique derivatives and accumulates from its
interior at the point. Consequently, reading mextDerivWithin in any preferred chart gives the
flat exterior derivative of the coordinate expression. These identities allow naturality and
iteration of the exterior derivative to be checked in a fixed chart, including at boundary and
corner points. The unrestricted results are the specializations to the whole manifold.
The transport uses Mathlib's extDerivWithin_pullback, localized to the chart overlap.
References #
- John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Chapter 14.
Evaluating a chart expression at a chart image transports each argument through the actual tangent coordinate change.
Two rough forms have the same coordinate expression at the chart image of a point of the chart source exactly when they agree at that point.
On an overlap of two preferred charts, a rough form read in the first chart is the pullback of its expression in the second chart by the coordinate change.
Change of preferred chart for exterior differentiation within a manifold subset. The subset has unique derivatives and accumulates from its interior at the point; it need not be open. The derivative of the coordinate change is taken within the full model range.
If the coordinate expression of a rough form in the preferred chart at x₀ is differentiable
within the model range at a chart point z, then so is its expression in the preferred chart at
any x whose source contains the corresponding point of the manifold: by the change of chart, the
second expression is the pullback of the first by a C² coordinate change.
The exterior derivative of a rough form's coordinate expression is transported by a change of
preferred chart. This is the chart-independence statement behind mextDerivWithin. Where the
expression is not differentiable in either chart, both sides are zero.
Reading the manifold exterior derivative within a subset in any preferred chart gives the flat exterior derivative of the coordinate expression within the corresponding coordinate set. Only differentiability in the chart centred at the point is needed.
Reading the exterior derivative in any preferred chart gives the flat exterior derivative within the model range. This includes boundary and corner chart points.
The scalar coefficient of a manifold top form transforms by the signed Jacobian between preferred charts, including derivatives taken within the model range at the boundary.