Vector fields read in a chart #
A vector field w on the model space E of a manifold M, read in the extended chart at a point
x and extended by zero outside the chart domain, is a vector field chartField x w on M. It is
smooth when w is smooth and supported in a compact subset of the chart target, and a straight
segment in the chart along which w is constant is an integral curve of it.
The basic case is a constant field v cut off by a bump function ρ in the chart at x: the
field bumpChartField x ρ v is compactly supported, and near x its flow lines are the straight
lines in direction v. These are the coordinate motions used to move points of a manifold, as in
Milnor's proof of the homogeneity lemma.
Main declarations #
TauCeti.chartField: a vector field on the model space, read in the extended chart at a point and extended by zero;TauCeti.contMDiff_chartFieldshows it is smooth when the field is supported in a compact subset of the chart target, andTauCeti.hasMFDerivAt_chartFieldthat straight segments along which the field is constant are its integral curves.TauCeti.bumpChartField: a constant field cut off by a bump function, read in the chart;TauCeti.bumpChartField_extChartAt_symmandTauCeti.bumpChartField_extChartAt_symm_of_mem_ballgive its values in the chart;TauCeti.contMDiff_bumpChartField,TauCeti.bumpChartField_eq_zeroandTauCeti.isMIntegralCurveOn_bumpChartFieldrecord its smoothness, compact support and straight flow lines near the centre;TauCeti.maximalIntegralCurve_bumpChartField_extChartAt_symmidentifies its maximal integral curves there with straight lines in the chart.
References #
- J. W. Milnor, Topology from the Differentiable Viewpoint, University Press of Virginia (1965), §4, Homogeneity Lemma; the flow of a cut-off constant vector field is the one used there.
Vector fields read in a chart #
A vector field w on the model space, read in the extended chart at x and extended by zero
outside the chart domain.
Instances For
On the chart domain, the chart field is the pullback of w by the extended chart.
Outside the chart domain, the chart field vanishes.
If w vanishes outside K ⊆ target, the chart field vanishes outside the preimage of
K.
At a point p of the chart target with w p = d, the chart field at (extChartAt I x).symm p
is the image of d under the derivative of the inverse chart.
A segment in a chart, along which w is the constant d, is an integral curve of the chart
field at every time at which it stays in an open set where w = d.
The chart field of a C^m vector field supported in a compact subset of the chart target is
a C^m vector field on M, provided M is C^(m + 1).
Cut-off constant fields #
The constant vector field v on the model space, cut off by the bump function ρ and read in
the chart at x.
Instances For
The cut-off field bumpChartField x ρ v is the chart field of p ↦ ρ p • v.
The cut-off field bumpChartField x ρ v vanishes outside the image under the inverse chart of
the closed outer ball of ρ.
On the chart target, the cut-off field bumpChartField x ρ v is the image of ρ p • v under
the derivative of the inverse chart.
On the inner ball of ρ, where ρ = 1, the cut-off field bumpChartField x ρ v is the image
of v under the derivative of the inverse chart.
The cut-off field bumpChartField x ρ v is C^m when M is C^(m + 1) and the closed outer
ball of ρ lies in the chart target.
A straight segment s ↦ c + s • v in the chart, for times at which it stays in the inner ball
of ρ, is an integral curve of the cut-off field bumpChartField x ρ v.
Near the centre of ρ, the maximal integral curve of the cut-off field bumpChartField x ρ v
through (extChartAt I x).symm c is the straight line t ↦ (extChartAt I x).symm (c + t • v) in
the chart, for every time t with ‖c - extChartAt I x x‖ + |t| * ‖v‖ < ρ.rIn (so the segment
from c to c + t • v stays in the inner ball of ρ).