The straightening theorem for vector fields on a manifold

Near a point x where a C^m vector field v on a finite-dimensional boundaryless manifold does not vanish, some chart of the C^m maximal atlas carries v to a constant vector field: the differential of the chart, read in the model vector space, sends v y to one fixed nonzero vector u at every point y of its domain (TauCeti.exists_chart_mfderiv_eq_const). In such a chart the integral curves of v are parallel straight lines traversed with constant velocity u.

The field read in the extended chart at x is a nonvanishing C^m vector field on an open subset of the model space, so the flat straightening theorem TauCeti.exists_openPartialHomeomorph_fderiv_eq_const produces a change of coordinates there; read back through the extended chart, it is a chart of the manifold (TauCeti.conj_chartAt_mem_maximalAtlas).

The manifold is C^n with m + 1 ≤ n, since a vector field read in a chart loses one derivative of the chart's regularity. Without the boundaryless hypothesis the statement fails: at a boundary point a chart preserves the boundary, while a field tangent to the boundary at one boundary point and transverse to it at nearby ones cannot become constant.

Main results

• TauCeti.exists_chart_mfderiv_eq_const: a nonvanishing C^m vector field is constant in a suitable chart of the C^m maximal atlas.

References

• John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Graduate Texts in Mathematics 218, Springer, 2013, Theorem 9.22 (canonical form near a regular point).

theorem TauCeti.exists_chart_mfderiv_eq_const {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] {m : ℕ∞} {n : WithTop ℕ∞} (hm : 1 ≤ m) (hmn : ↑m + 1 ≤ n) [IsManifold I 1 M] [IsManifold I n M] {v : (y : M) → TangentSpace I y} {U : Set M} {x : M} (hv : ContMDiffOn I I.tangent (↑m) (fun (y : M) => ⟨y, v y⟩) U) (hU : U ∈ nhds x) (hx : v x ≠ 0) : ∃ (e : OpenPartialHomeomorph M H) (u : E), e ∈ IsManifold.maximalAtlas I (↑m) M ∧ x ∈ e.source ∧ u ≠ 0 ∧ ∀ y ∈ e.source, (mfderiv% (↑I ∘ ↑e) y) (v y) = u

The straightening theorem [Lee, Thm. 9.22]. Let v be a vector field on a C^n manifold with finite-dimensional boundaryless model, C^m on a neighbourhood of x, with 1 ≤ m, m + 1 ≤ n and v x ≠ 0. Then some chart e of the C^m maximal atlas whose domain contains x carries v to a constant nonzero vector field: the differential of I ∘ e sends v y to the same vector u ≠ 0 at every point y of the domain of e.