Diffeomorphisms intertwine maximal flows

Let ψ : M → M' be a C^n diffeomorphism, n ≠ 0, carrying a vector field X on M to a vector field Y on M': dψ_x (X x) = Y (ψ x) for every x. Then ψ sends integral curves of X to integral curves of Y, and its inverse carries Y back to X (Diffeomorph.mfderiv_symm_apply_eq_of_mfderiv_apply_eq). Hence the maximal interval of existence of Y through ψ x is that of X through x (Diffeomorph.maximalIntegralCurveInterval_apply), and ψ conjugates the maximal flows:

ψ (flowOf X t x) = flowOf Y t (ψ x) (Diffeomorph.apply_flowOf).

This holds at every time, inside and outside the flow domain, since outside it both sides take the junk value of the initial point. The comparison of intervals needs no regularity of the fields; the identification of the flows uses uniqueness of integral curves of Y, so Y is C^1 on a Hausdorff boundaryless manifold.

Main results

• Diffeomorph.mfderiv_symm_apply_eq_of_mfderiv_apply_eq: the inverse of a diffeomorphism carrying X to Y carries Y to X.
• Diffeomorph.maximalIntegralCurveInterval_apply, Diffeomorph.mem_flowDomain_apply_iff: related fields have the same maximal intervals of existence at corresponding points.
• Diffeomorph.apply_flowOf: a diffeomorphism carrying X to Y conjugates their maximal flows.

References

• John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Graduate Texts in Mathematics 218, Springer, 2013, Proposition 9.13 (naturality of flows).

theorem Diffeomorph.mfderiv_symm_apply_eq_of_mfderiv_apply_eq {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'] {n : WithTop ℕ∞} (ψ : Diffeomorph I I' M M' n) (hn : n ≠ 0) {X : (x : M) → TangentSpace I x} {Y : (y : M') → TangentSpace I' y} (hXY : ∀ (x : M), (mfderiv% ⇑ψ x) (X x) = Y (ψ x)) (y : M') : (mfderiv% ⇑ψ.symm y) (Y y) = X (ψ.symm y)

If a diffeomorphism carries the vector field X to Y, its inverse carries Y to X.

theorem Diffeomorph.maximalIntegralCurveInterval_apply {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'] {n : WithTop ℕ∞} (ψ : Diffeomorph I I' M M' n) (hn : n ≠ 0) {X : (x : M) → TangentSpace I x} {Y : (y : M') → TangentSpace I' y} (hXY : ∀ (x : M), (mfderiv% ⇑ψ x) (X x) = Y (ψ x)) (x : M) : maximalIntegralCurveInterval Y (ψ x) = maximalIntegralCurveInterval X x

Related vector fields have the same maximal intervals. If a diffeomorphism ψ carries X to Y, the maximal interval of existence of Y through ψ x is that of X through x.

theorem Diffeomorph.mem_flowDomain_apply_iff {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'] {n : WithTop ℕ∞} (ψ : Diffeomorph I I' M M' n) (hn : n ≠ 0) {X : (x : M) → TangentSpace I x} {Y : (y : M') → TangentSpace I' y} (hXY : ∀ (x : M), (mfderiv% ⇑ψ x) (X x) = Y (ψ x)) {t : ℝ} {x : M} : (t, ψ x) ∈ TauCeti.flowDomain Y ↔ (t, x) ∈ TauCeti.flowDomain X

If a diffeomorphism ψ carries X to Y, the flow of Y is defined at (t, ψ x) exactly when the flow of X is defined at (t, x).

theorem Diffeomorph.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'] {n : WithTop ℕ∞} (ψ : Diffeomorph I I' M M' n) (hn : n ≠ 0) {X : (x : M) → TangentSpace I x} {Y : (y : M') → TangentSpace I' y} [T2Space M'] [IsManifold I' 1 M'] [BoundarylessManifold I' M'] (hY : ContMDiff I' I'.tangent 1 fun (y : M') => ⟨y, Y y⟩) (hXY : ∀ (x : M), (mfderiv% ⇑ψ x) (X x) = Y (ψ x)) (t : ℝ) (x : M) : ψ (TauCeti.flowOf X t x) = TauCeti.flowOf Y t (ψ x)

Naturality of flows. A diffeomorphism ψ carrying the vector field X to the C^1 vector field Y conjugates their maximal flows: ψ (flowOf X t x) = flowOf Y t (ψ x). Outside the flow domain both sides are the junk value ψ x.