Naturality of maximal flows under related maps

A differentiable map f relating vector fields X and Y sends each integral curve of X to one of Y. Consequently the maximal interval through x is contained in the maximal interval through f x. If Y has unique integral curves, the maximal flows intertwine on the source flow domain. Surjectivity of f therefore lets completeness descend from X to Y, without requiring an inverse or a submersion hypothesis.

Unlike the diffeomorphism case, the flow identity is only asserted on the source domain: a related map can collapse an escaping trajectory to a stationary point, so the target flow may exist longer. Outside the source domain its junk value need not intertwine.

The proofs use IsMIntegralCurveOn.map_of_mfderiv_eq and the witness and uniqueness characterizations of maximalIntegralCurve.

References

• John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Chapter 9, Proposition 9.6 (naturality of integral curves).

theorem MDifferentiable.maximalIntegralCurveInterval_subset {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u_6} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {X : (x : M) → TangentSpace I x} {Y : (y : M') → TangentSpace I' y} (hf : MDiff f) (hXY : ∀ (x : M), (mfderiv% f x) (X x) = Y (f x)) (x : M) : maximalIntegralCurveInterval X x ⊆ maximalIntegralCurveInterval Y (f x)

A differentiable map relating two vector fields can only enlarge the maximal interval of existence. No uniqueness or regularity assumption on either field is needed.

theorem MDifferentiable.isCompleteVectorField_of_surjective {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u_6} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {X : (x : M) → TangentSpace I x} {Y : (y : M') → TangentSpace I' y} (hf : MDiff f) (hsurj : Function.Surjective f) (hXY : ∀ (x : M), (mfderiv% f x) (X x) = Y (f x)) (hX : TauCeti.IsCompleteVectorField X) : TauCeti.IsCompleteVectorField Y

Completeness descends through any surjective differentiable map relating the fields. The map need not be injective, proper, or a submersion.

theorem MDifferentiable.apply_flowOf {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u_6} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {X : (x : M) → TangentSpace I x} {Y : (y : M') → TangentSpace I' y} [T2Space M'] [IsManifold I' 1 M'] [BoundarylessManifold I' M'] (hf : MDiff f) (hY : ContMDiff I' I'.tangent 1 fun (y : M') => ⟨y, Y y⟩) (hXY : ∀ (x : M), (mfderiv% f x) (X x) = Y (f x)) {t : ℝ} {x : M} (ht : (t, x) ∈ TauCeti.flowDomain X) : f (TauCeti.flowOf X t x) = TauCeti.flowOf Y t (f x)

A differentiable map relating X to a C¹ field Y intertwines their maximal flows at every time in the source flow domain. No smoothness of X is required.