Coordinate expressions of actual manifold pullback #
The coordinate expression of a pullback uses the within-range derivative of the map composed
with the inverse source chart. This is the actual manifold chain rule, including boundary
points, and supplies the coefficient transport used in interval and product comparisons.
In top degree, the coefficient of a pullback in a basis is the coordinate Jacobian determinant
times the coefficient of the form; when the two manifolds are modelled on different spaces, the
Jacobian is read in the source model through a linear equivalence of the model spaces.
Pulling a flat form back along a preferred chart and reading it in the same chart recovers the
flat form on the chart target, which is how flat constructions in a chart are moved to the
manifold; conversely, evaluating a form φ on the chart source agrees with evaluating
φ.inChartAt α on mvfderiv I (extChartAt I α) (TauCeti.RoughForm.apply_eq_inChartAt_mvfderiv).
Near time t, the pullback along a family of maps which sends y into the chart at y at time t
is the flat pullback along the family read in the chart at y
(TauCeti.RoughForm.eventuallyEq_mpullback_compContinuousLinearMap).
The actual pullback's coefficient in a preferred source chart is obtained from the within-range derivative of the composite with its inverse chart.
The within-set pullback of a form along a map f from a normed space, at a point w sent into
the preferred chart at c, is the flat pullback of the coordinate expression of the form in that
chart along the coordinate expression of f.
The coefficient of the pullback in a preferred source chart β, at a chart coordinate z whose
image under f lies in the preferred chart at α, is the flat pullback of the coordinate
expression of the form in the chart at α along the derivative of the coordinate expression
of f.
The pullback of a form at x along a map f, with f x in the preferred chart at c, is the
flat pullback of the coordinate expression of the form in that chart along the coordinate
expression of f from the preferred chart at x.
Near time t, the pullback of a form at y along a family of maps ψᵤ which sends y into
the chart at c at time t and is jointly C¹ at (t, y) is the flat pullback of its chart
expression at c along the family read from the chart at y.
For a model-valued map, actual pullback coefficients use its ordinary within-range Fréchet derivative, with the canonical model tangent identification made explicit.
Pulling a flat form back along a preferred extended chart and reading the result in the same chart recovers the flat form on the chart target.
At any point x of (extChartAt I α).source, evaluating φ on tangent vectors agrees with
evaluating φ.inChartAt α on their mvfderiv images under extChartAt I α.
The coefficient of a pullback in a preferred chart of the source is the determinant of the
coordinate expression of the map times the coefficient of the form in a preferred chart of the
target. The two model spaces are compared through a continuous linear equivalence C : E ≃ E':
the determinant is that of the coordinate derivative followed by C⁻¹, and the target
coefficient is taken in the basis C ∘ b. Derivatives are taken within the model range, so
boundary and corner points are included.