The local Liouville flow out of a hypersurface

Let Z be a smooth vector field on a manifold M which is the Liouville field of a one-form α, ι_Z dα = α, and let ι : S → M be a smooth map, typically the inclusion of a hypersurface. No completeness of Z is assumed. The local Liouville flow map is Φ(t, s) = φₜ(ι s), where φ is the maximal flow of Z (TauCeti.flowOf). It is defined on the open set D = {(t, s) | φₜ(ι s) is defined} of ℝ × S, which contains {0} × S; its slice over each s is an open interval around 0 whose length varies with s. On this domain:

• Φ pulls α back to the symplectization form eᵗ ι^* α (TauCeti.mpullback_flowOf_comp_apply_eq_symplectization), and dα back to d(eᵗ ι^* α) (TauCeti.mpullback_flowOf_comp_mextDeriv_apply). In the convention ω = -dλ of an exact symplectic manifold, whose Liouville field satisfies ι_Z ω = -λ, this says Φ^*(-λ) = eᵗ (-λ)|_S and Φ^* ω = d(eᵗ (-λ)|_S), taking α = -λ.
• If ι^* α is a contact form, then Φ pulls dα back to the symplectic form d(eᵗ ι^* α), so its differential is injective at every point of D (TauCeti.injective_mfderiv_flowOf_comp). When S has one dimension less than M, Φ is therefore a local diffeomorphism at every point of D (TauCeti.isLocalDiffeomorphAt_flowOf_comp).
• If moreover ι is a topological embedding, then Φ is injective and a local diffeomorphism on a collar {(t, s) | |t| < ε s} of {0} × S inside D, whose width ε is a positive continuous function on S (TauCeti.exists_continuous_pos_injOn_flowOf_comp). So Φ is a diffeomorphism from this collar onto an open neighbourhood of the image of ι. No compactness of S is needed, only that S and M are pseudometrizable, as second countable Hausdorff manifolds are.
• If S is compact and ι is injective, the width can be taken constant: Φ is injective and a local diffeomorphism on (-ε, ε) × S for some ε > 0 (TauCeti.exists_pos_injOn_flowOf_comp).

A hypersurface transverse to the Liouville field of a nondegenerate dα carries the contact form ι^* α (TauCeti.IsContactType.isContactForm_mpullback), so for such a hypersurface the local Liouville flow map is a local diffeomorphism on its whole domain (TauCeti.isLocalDiffeomorphAt_flowOf_comp_of_isTransverseAlong). For a complete Liouville field, the identity Φ^* α = eᵗ ι^* α holds on all of ℝ × S (TauCeti.mpullback_globalFlow_comp_eq_symplectization).

Main results

• TauCeti.mpullback_flowOf_comp_apply_eq_symplectization: Φ^* α = eᵗ ι^* α on D.
• TauCeti.mpullback_flowOf_comp_mextDeriv_apply: Φ^* dα = d(eᵗ ι^* α) on D.
• TauCeti.injective_mfderiv_flowOf_comp: for a contact form ι^* α, Φ is an immersion on D.
• TauCeti.isLocalDiffeomorphAt_flowOf_comp, TauCeti.isLocalDiffeomorphAt_flowOf_comp_of_isTransverseAlong: for a hypersurface, Φ is a local diffeomorphism at every point of D.
• TauCeti.exists_continuous_pos_injOn_flowOf_comp: the collar of variable width of an embedded hypersurface.
• TauCeti.exists_pos_injOn_flowOf_comp: the collar of uniform width of a compact hypersurface.

References

• D. McDuff, D. Salamon, Introduction to Symplectic Topology, 3rd ed., Oxford, 2017, Section 3.5 (hypersurfaces of contact type).
• H. Geiges, An Introduction to Contact Topology, Cambridge University Press, 2008, Section 1.4 (hypersurfaces of contact type).

theorem TauCeti.mpullback_flowOf_comp_apply_eq_symplectization {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] [T2Space M] [IsManifold I (↑⊤) M] {Z : (x : M) → TangentSpace I x} {E' : Type u_4} {H' : Type u_5} {S : Type u_6} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} [TopologicalSpace S] [ChartedSpace H' S] (hZ : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Z x⟩) {ι : S → M} (hι : ContMDiff J I (↑⊤) ι) [IsManifold J (↑⊤) S] {α : SmoothForm I M ℝ 1} (hZα : RoughForm.interior Z (mextDeriv ↑α) = ↑α) {p : ℝ × S} (hp : (p.1, ι p.2) ∈ flowDomain Z) : mpullback ((modelWithCornersSelf ℝ ℝ).prod J) I (fun (q : ℝ × S) => flowOf Z q.1 (ι q.2)) (↑α) p = ↑((SmoothForm.mpullback ι hι) α).symplectization p

The local Liouville flow map pulls the primitive back to the symplectization form. Let the smooth vector field Z be the Liouville field of the one-form α, ι_Z dα = α, and let ι : S → M be smooth. At every point of its domain, the local flow map (t, s) ↦ φₜ(ι s) pulls α back to the symplectization form eᵗ ι^* α of the restricted form.

theorem TauCeti.mpullback_flowOf_comp_mextDeriv_apply {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] [T2Space M] [IsManifold I (↑⊤) M] {Z : (x : M) → TangentSpace I x} {E' : Type u_4} {H' : Type u_5} {S : Type u_6} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} [TopologicalSpace S] [ChartedSpace H' S] (hZ : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Z x⟩) {ι : S → M} (hι : ContMDiff J I (↑⊤) ι) [IsManifold J (↑⊤) S] {α : SmoothForm I M ℝ 1} (hZα : RoughForm.interior Z (mextDeriv ↑α) = ↑α) {p : ℝ × S} (hp : (p.1, ι p.2) ∈ flowDomain Z) : mpullback ((modelWithCornersSelf ℝ ℝ).prod J) I (fun (q : ℝ × S) => flowOf Z q.1 (ι q.2)) (mextDeriv ↑α) p = mextDeriv (↑((SmoothForm.mpullback ι hι) α).symplectization) p

The local Liouville flow map pulls dα back to d(eᵗ ι^* α). Let the smooth vector field Z be the Liouville field of the one-form α, ι_Z dα = α, and let ι : S → M be smooth. At every point of its domain, the local flow map (t, s) ↦ φₜ(ι s) pulls dα back to the exterior derivative of the symplectization form eᵗ ι^* α.

theorem TauCeti.injective_mfderiv_flowOf_comp {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] [T2Space M] [IsManifold I (↑⊤) M] {Z : (x : M) → TangentSpace I x} {E' : Type u_4} {H' : Type u_5} {S : Type u_6} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} [TopologicalSpace S] [ChartedSpace H' S] (hZ : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Z x⟩) {ι : S → M} (hι : ContMDiff J I (↑⊤) ι) [IsManifold J (↑⊤) S] {α : SmoothForm I M ℝ 1} (hZα : RoughForm.interior Z (mextDeriv ↑α) = ↑α) (hα : ((SmoothForm.mpullback ι hι) α).IsContactForm) {p : ℝ × S} (hp : (p.1, ι p.2) ∈ flowDomain Z) : Function.Injective ⇑((mfderiv% fun (q : ℝ × S) => flowOf Z q.1 (ι q.2)) p)

The local Liouville flow map is an immersion. Let the smooth vector field Z be the Liouville field of the one-form α, ι_Z dα = α, and let ι : S → M be smooth with ι^* α a contact form. Then the local flow map (t, s) ↦ φₜ(ι s) has injective differential at every point of its domain, since it pulls dα back to the symplectic form d(eᵗ ι^* α).

theorem TauCeti.isLocalDiffeomorphAt_flowOf_comp {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] [T2Space M] [IsManifold I (↑⊤) M] {Z : (x : M) → TangentSpace I x} {E' : Type u_4} {H' : Type u_5} {S : Type u_6} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} [TopologicalSpace S] [ChartedSpace H' S] (hZ : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Z x⟩) {ι : S → M} (hι : ContMDiff J I (↑⊤) ι) [IsManifold J (↑⊤) S] {α : SmoothForm I M ℝ 1} [FiniteDimensional ℝ E'] [J.Boundaryless] (hdim : Module.finrank ℝ E' + 1 = Module.finrank ℝ E) (hZα : RoughForm.interior Z (mextDeriv ↑α) = ↑α) (hα : ((SmoothForm.mpullback ι hι) α).IsContactForm) {p : ℝ × S} (hp : (p.1, ι p.2) ∈ flowDomain Z) : IsLocalDiffeomorphAt ((modelWithCornersSelf ℝ ℝ).prod J) I (↑⊤) (fun (q : ℝ × S) => flowOf Z q.1 (ι q.2)) p

The local Liouville flow map is a local diffeomorphism. Let the smooth vector field Z be the Liouville field of the one-form α, ι_Z dα = α, and let ι : S → M be smooth from a boundaryless manifold of one dimension less, with ι^* α a contact form. Then the local flow map (t, s) ↦ φₜ(ι s) is a local diffeomorphism at every point of its domain.

theorem TauCeti.exists_pos_injOn_flowOf_comp {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] [T2Space M] [IsManifold I (↑⊤) M] {Z : (x : M) → TangentSpace I x} {E' : Type u_4} {H' : Type u_5} {S : Type u_6} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} [TopologicalSpace S] [ChartedSpace H' S] (hZ : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Z x⟩) {ι : S → M} (hι : ContMDiff J I (↑⊤) ι) [IsManifold J (↑⊤) S] {α : SmoothForm I M ℝ 1} [FiniteDimensional ℝ E'] [J.Boundaryless] [CompactSpace S] (hdim : Module.finrank ℝ E' + 1 = Module.finrank ℝ E) (hZα : RoughForm.interior Z (mextDeriv ↑α) = ↑α) (hα : ((SmoothForm.mpullback ι hι) α).IsContactForm) (hιi : Function.Injective ι) : ∃ ε > 0, Set.Ioo (-ε) ε ×ˢ Set.univ ⊆ {p : ℝ × S | (p.1, ι p.2) ∈ flowDomain Z} ∧ Set.InjOn (fun (q : ℝ × S) => flowOf Z q.1 (ι q.2)) (Set.Ioo (-ε) ε ×ˢ Set.univ) ∧ IsLocalDiffeomorphOn ((modelWithCornersSelf ℝ ℝ).prod J) I (↑⊤) (fun (q : ℝ × S) => flowOf Z q.1 (ι q.2)) (Set.Ioo (-ε) ε ×ˢ Set.univ)

The Liouville collar of a compact hypersurface has uniform width. Let the smooth vector field Z be the Liouville field of the one-form α, ι_Z dα = α, and let ι : S → M be a smooth injective map from a compact boundaryless manifold of one dimension less, with ι^* α a contact form. Then for some ε > 0 the flow φₜ(ι s) is defined for |t| < ε, and on the collar (-ε, ε) × S the local flow map (t, s) ↦ φₜ(ι s) is injective and a local diffeomorphism, that is, a diffeomorphism onto an open subset of M.

theorem TauCeti.exists_continuous_pos_injOn_flowOf_comp {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] [T2Space M] [IsManifold I (↑⊤) M] {Z : (x : M) → TangentSpace I x} {E' : Type u_4} {H' : Type u_5} {S : Type u_6} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} [TopologicalSpace S] [ChartedSpace H' S] (hZ : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Z x⟩) {ι : S → M} (hι : ContMDiff J I (↑⊤) ι) [IsManifold J (↑⊤) S] {α : SmoothForm I M ℝ 1} [FiniteDimensional ℝ E'] [J.Boundaryless] [TopologicalSpace.PseudoMetrizableSpace M] [TopologicalSpace.PseudoMetrizableSpace S] (hdim : Module.finrank ℝ E' + 1 = Module.finrank ℝ E) (hZα : RoughForm.interior Z (mextDeriv ↑α) = ↑α) (hα : ((SmoothForm.mpullback ι hι) α).IsContactForm) (hιe : Topology.IsInducing ι) : ∃ (ε : C(S, ℝ)), (∀ (s : S), 0 < ε s) ∧ {p : ℝ × S | |p.1| < ε p.2} ⊆ {p : ℝ × S | (p.1, ι p.2) ∈ flowDomain Z} ∧ Set.InjOn (fun (q : ℝ × S) => flowOf Z q.1 (ι q.2)) {p : ℝ × S | |p.1| < ε p.2} ∧ IsLocalDiffeomorphOn ((modelWithCornersSelf ℝ ℝ).prod J) I (↑⊤) (fun (q : ℝ × S) => flowOf Z q.1 (ι q.2)) {p : ℝ × S | |p.1| < ε p.2}

The Liouville collar of a noncompact hypersurface. Let the smooth vector field Z be the Liouville field of the one-form α, ι_Z dα = α, and let ι : S → M be a smooth topological embedding of a boundaryless manifold of one dimension less, with ι^* α a contact form. Then for some positive continuous width ε : S → ℝ the flow φₜ(ι s) is defined for |t| < ε s, and on the collar {(t, s) | |t| < ε s} of {0} × S the local flow map (t, s) ↦ φₜ(ι s) is injective and a local diffeomorphism, that is, a diffeomorphism onto an open subset of M.

No compactness of S is needed. The embedding hypothesis is necessary: the collar map is a homeomorphism onto its open image and restricts to ι on {0} × S.

theorem TauCeti.isLocalDiffeomorphAt_flowOf_comp_of_isTransverseAlong {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] [T2Space M] [IsManifold I (↑⊤) M] {Z : (x : M) → TangentSpace I x} {E' : Type u_4} {H' : Type u_5} {S : Type u_6} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} [TopologicalSpace S] [ChartedSpace H' S] (hZ : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Z x⟩) {ι : S → M} (hι : ContMDiff J I (↑⊤) ι) [IsManifold J (↑⊤) S] {α : SmoothForm I M ℝ 1} [FiniteDimensional ℝ E'] [J.Boundaryless] (hdim : Module.finrank ℝ E' + 1 = Module.finrank ℝ E) (hσ : SmoothTwoForm.IsNondegenerate ((mextDerivₗ I 1) α)) (hZα : RoughForm.interior Z (mextDeriv ↑α) = ↑α) (hιs : ∀ (s : S), Function.Injective ⇑(mfderiv% ι s)) (hZι : IsTransverseAlong J Z ι) {p : ℝ × S} (hp : (p.1, ι p.2) ∈ flowDomain Z) : IsLocalDiffeomorphAt ((modelWithCornersSelf ℝ ℝ).prod J) I (↑⊤) (fun (q : ℝ × S) => flowOf Z q.1 (ι q.2)) p

The Liouville collar of a transverse hypersurface is locally diffeomorphic. Let the smooth vector field Z be the Liouville field of the one-form α, ι_Z dα = α, with dα nondegenerate, and let ι : S → M be a smooth immersion of a boundaryless manifold of one dimension less, to which Z is transverse. Then ι^* α is a contact form, and the local flow map (t, s) ↦ φₜ(ι s) is a local diffeomorphism at every point of its domain.