Hypersurfaces of contact type

Let ω be a two-form on a manifold M and let ι : S → M be a map, typically the inclusion of an embedded hypersurface. The hypersurface is of contact type when some Liouville vector field (L_Z ω = ω) defined near it is transverse to it, and of restricted contact type when such a field exists on all of M. These are the hypersurfaces whose characteristic foliations are preserved, up to conjugation, by the flow of Z, which is how existence of closed characteristics on them is deduced from almost existence.

For a closed ω, a Liouville vector field Z is the same as a primitive α = ι_Z ω of ω (TauCeti.isLiouvilleVectorField_iff_mextDeriv_interior_eq), and when ω is nondegenerate the primitive determines the field. The definitions below keep the primitive explicit:

• TauCeti.IsContactType J ω α ι: on some open neighbourhood U of the image of ι, dα = ω, and some vector field Z, smooth on U and satisfying ι_Z ω = α on U, is transverse along ι;
• TauCeti.IsRestrictedContactType J ω α ι: dα = ω on M, and some smooth vector field Z on M with ι_Z ω = α is transverse along ι.

The primitive is part of the data because a Liouville vector field need not be the Liouville field of a given primitive: on the plane, x ∂_x + ∂_y is a Liouville vector field of d(x dy) whose primitive is x dy - dx, not x dy (Prod.curryLeft_extDeriv_realPlaneXDy_ne).

A hypersurface of restricted contact type is of contact type, with the same primitive (TauCeti.IsRestrictedContactType.isContactType). For a closed C¹ form ω, a hypersurface is of restricted contact type for some primitive exactly when some smooth Liouville vector field of ω is transverse along it (TauCeti.exists_isRestrictedContactType_iff), which is the definition of McDuff and Salamon. The basic example is the unit cosphere bundle of a Riemannian manifold, with the primitive -λ of the canonical symplectic form of the cotangent bundle (TauCeti.CotangentBundle.isRestrictedContactType_cosphereBundle).

A hypersurface of contact type is a contact manifold: if ω is nondegenerate and ι is an immersion of codimension one of contact type for ω with primitive α, then ι^* α is a contact form (TauCeti.IsContactType.isContactForm_mpullback). At a point ι s the image W of the differential of ι is a hyperplane and Z lies outside it. The covector α = ι_Z ω cannot vanish on W, since it vanishes on Z and ω is nondegenerate. A vector of W ∩ ker α that is ω-orthogonal to W ∩ ker α is also ω-orthogonal to Z, hence to all of ker α, so it is a multiple of Z lying in W and therefore zero. The pointwise version (TauCeti.isContactFormAt_mpullback) only uses the data at a single point.

Main definitions

• TauCeti.IsContactType: contact type, with an explicit primitive near the hypersurface.
• TauCeti.IsRestrictedContactType: restricted contact type, with an explicit global primitive.

Main results

• TauCeti.IsRestrictedContactType.isContactType: restricted contact type implies contact type.
• TauCeti.exists_isRestrictedContactType_iff: the characterization by transverse Liouville vector fields.
• TauCeti.isContactFormAt_mpullback, TauCeti.IsContactType.isContactForm_mpullback: the primitive restricts to a contact form on a hypersurface of contact type.

References

• D. McDuff, D. Salamon, Introduction to Symplectic Topology, 3rd ed., Oxford, 2017, Section 3.5 (hypersurfaces of contact type).
• H. Hofer, E. Zehnder, Symplectic Invariants and Hamiltonian Dynamics, Birkhäuser, 1994, Chapter 4.

def TauCeti.IsContactType {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {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] (ω : RoughForm I M ℝ 2) (α : RoughForm I M ℝ 1) (ι : S → M) : Prop

A map ι : S → M, typically an embedded hypersurface, is of contact type for the two-form ω, with primitive α, when on some open neighbourhood U of the image of ι the one-form α is a primitive of ω, dα = ω, and some vector field Z, smooth on U and satisfying ι_Z ω = α on U, is transverse along ι. When ω is smooth, such a Z is a Liouville vector field of ω on U.

def TauCeti.IsRestrictedContactType {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {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] (ω : RoughForm I M ℝ 2) (α : RoughForm I M ℝ 1) (ι : S → M) : Prop

A map ι : S → M, typically an embedded hypersurface, is of restricted contact type for the two-form ω, with primitive α, when α is a primitive of ω on all of M, dα = ω, and some smooth vector field Z on M with ι_Z ω = α is transverse along ι. For a closed C¹ form ω, such a Z is a Liouville vector field of ω (TauCeti.exists_isRestrictedContactType_iff).

theorem TauCeti.isContactType_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {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] {ω : RoughForm I M ℝ 2} {α : RoughForm I M ℝ 1} {ι : S → M} : IsContactType J ω α ι ↔ ∃ (U : Set M), IsOpen U ∧ Set.range ι ⊆ U ∧ (∀ x ∈ U, mextDeriv α x = ω x) ∧ ∃ (Z : (x : M) → TangentSpace I x), ContMDiffOn I I.tangent (↑⊤) (fun (x : M) => ⟨x, Z x⟩) U ∧ (∀ x ∈ U, RoughForm.interior Z ω x = α x) ∧ IsTransverseAlong J Z ι

The defining characterization of contact type.

theorem TauCeti.isRestrictedContactType_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {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] {ω : RoughForm I M ℝ 2} {α : RoughForm I M ℝ 1} {ι : S → M} : IsRestrictedContactType J ω α ι ↔ mextDeriv α = ω ∧ ∃ (Z : (x : M) → TangentSpace I x), (ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Z x⟩) ∧ RoughForm.interior Z ω = α ∧ IsTransverseAlong J Z ι

The defining characterization of restricted contact type.

theorem TauCeti.IsRestrictedContactType.mextDeriv_eq {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {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] {ω : RoughForm I M ℝ 2} {α : RoughForm I M ℝ 1} {ι : S → M} (h : IsRestrictedContactType J ω α ι) : mextDeriv α = ω

The primitive of a hypersurface of restricted contact type is a primitive: dα = ω.

theorem TauCeti.IsRestrictedContactType.isContactType {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {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] {ω : RoughForm I M ℝ 2} {α : RoughForm I M ℝ 1} {ι : S → M} (h : IsRestrictedContactType J ω α ι) : IsContactType J ω α ι

Restricted contact type implies contact type, with the same primitive: take the whole manifold as the neighbourhood of the hypersurface.

theorem TauCeti.exists_isRestrictedContactType_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {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] {ω : RoughForm I M ℝ 2} {ι : S → M} (hω : IsSmoothForm I 1 ω) (hdω : mextDeriv ω = 0) : (∃ (α : RoughForm I M ℝ 1), IsRestrictedContactType J ω α ι) ↔ ∃ (Z : (x : M) → TangentSpace I x), (ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Z x⟩) ∧ IsLiouvilleVectorField ω Z ∧ IsTransverseAlong J Z ι

Restricted contact type through Liouville vector fields. For a closed C¹ two-form ω, a map ι is of restricted contact type for some primitive of ω exactly when some smooth Liouville vector field Z of ω on M is transverse along ι; the primitive is then ι_Z ω.

The contact form of a hypersurface of contact type

theorem TauCeti.isContactFormAt_mpullback {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {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] {ω : RoughForm I M ℝ 2} {α : RoughForm I M ℝ 1} {ι : S → M} [IsManifold I 2 M] [IsManifold J 2 S] {s : S} (hdim : Module.finrank ℝ E' + 1 = Module.finrank ℝ E) (hι : ContMDiffAt J I 2 ι s) (hιs : Function.Injective ⇑(mfderiv% ι s)) (hω : ∀ (v : TangentSpace I (ι s)), (∀ (w : TangentSpace I (ι s)), (ω (ι s)) ![v, w] = 0) → v = 0) (hα : ContMDiffAt I (I.prod (modelWithCornersSelf ℝ (E [⋀^Fin 1]→L[ℝ] ℝ))) 1 (fun (y : M) => ⟨y, α y⟩) (ι s)) (hdα : mextDeriv α (ι s) = ω (ι s)) {z : TangentSpace I (ι s)} (hz : z ∉ (↑(mfderiv% ι s)).range) (hzα : ∀ (v : TangentSpace I (ι s)), (ω (ι s)) ![z, v] = (α (ι s)) ![v]) : IsContactFormAt (mpullback J I ι α) s

The primitive restricts to a contact form on a transverse hypersurface, pointwise. Let ι : S → M be C² at s, with injective differential there, from a manifold of one dimension less. Let ω be nondegenerate at ι s, let α be a C¹ primitive of ω at ι s, and let z be a tangent vector at ι s, outside the image of the differential of ι, with ι_z ω = α. Then the pullback ι^* α is a contact form at s.

theorem TauCeti.IsContactType.isContactForm_mpullback {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {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] {ι : S → M} [IsManifold I (↑⊤) M] [IsManifold J 2 S] {σ : SmoothTwoForm I M} (hσ : σ.IsNondegenerate) {α : SmoothForm I M ℝ 1} (h : IsContactType J (↑σ) (↑α) ι) (hι : ContMDiff J I (↑⊤) ι) (hιs : ∀ (s : S), Function.Injective ⇑(mfderiv% ι s)) (hdim : Module.finrank ℝ E' + 1 = Module.finrank ℝ E) : ((SmoothForm.mpullback ι hι) α).IsContactForm

Hypersurfaces of contact type carry contact forms. If a smooth map ι : S → M with injective differentials, from a manifold of one dimension less, is of contact type for a nondegenerate two-form σ, with primitive α, then the pullback ι^* α is a contact form on S.