The symplectization of a contact form

Let α be a one-form on a manifold M. Its symplectization is the product ℝ × M, with real coordinate t, carrying the one-form

θ = eᵗ α (TauCeti.SmoothForm.symplectization α),

where α is pulled back along the projection to M. Its exterior derivative is dθ = eᵗ (dt ∧ α + dα): on tangent vectors (s, v) and (t', w) at (t, x) it takes the value eᵗ (s α(w) - t' α(v) + dα(v, w)) (TauCeti.SmoothForm.mextDeriv_symplectization_apply). The two-form dθ is symplectic exactly when α is a contact form (TauCeti.SmoothForm.isSymplectic_mextDerivₗ_symplectization_iff). Closedness is automatic, and nondegeneracy is, at each point, the linear algebra of Module.Dual.isContact_iff_nondegenerate_symplectizationForm.

With the conventions ω = -dλ for exact symplectic manifolds and ι_Z ω = -λ for their Liouville fields, the symplectization of a contact form is the exact symplectic manifold (ℝ × M, ω = dθ) with primitive λ = -θ. Its Liouville field is the unit vector field ∂_t along the real factor: ι_(∂_t) dθ = θ (TauCeti.SmoothForm.interior_mextDeriv_symplectization), so ∂_t is a Liouville vector field of dθ (TauCeti.SmoothForm.isLiouvilleVectorField_symplectization).

If a smooth map F : M → M' pulls a one-form α' back to f α for a smooth positive function f, then its lift (t, x) ↦ (t - log f(x), F(x)) pulls eᵗ α' back to eᵗ α (TauCeti.SmoothForm.mpullback_symplectizationLift_symplectization). For a coorientation-preserving contactomorphism this is its lift to the symplectizations; it preserves the primitive θ and not only dθ. Taking F to be the identity, the map (t, x) ↦ (t - log f(x), x) pulls the symplectization form of f α back to that of α.

If instead f is negative, the lift for -f pulls the symplectization form of -α' back to that of α (TauCeti.SmoothForm.mpullback_symplectizationLift_neg_symplectization). For a nowhere vanishing α, the strict lift has no free constant: a map (t, x) ↦ (φ(t, x), F(x)) covering F pulls eᵗ α' back to eᵗ α only when f > 0 and φ(t, x) = t - log f(x) (TauCeti.SmoothForm.eq_symplectizationLift_of_mpullback_symplectization_eq).

This file treats the symplectization of a chosen contact form, that is, of a trivialized cooriented contact structure. In terms of the annihilator line (ker α)⁰ ⊂ T*M, the point (t, x) corresponds to the covector eᵗ α_x of its positive half.

Main definitions

• TauCeti.SmoothForm.symplectization α: the one-form eᵗ α on ℝ × M.
• TauCeti.symplectizationLift: the map (t, x) ↦ (t - log f(x), F(x)).

Main results

• TauCeti.SmoothForm.mextDeriv_symplectization_apply: d(eᵗ α) = eᵗ (dt ∧ α + dα).
• TauCeti.SmoothForm.isSymplectic_mextDerivₗ_symplectization_iff: d(eᵗ α) is symplectic exactly when α is a contact form.
• TauCeti.SmoothForm.interior_mextDeriv_symplectization, TauCeti.SmoothForm.isLiouvilleVectorField_symplectization: ∂_t is the Liouville field.
• TauCeti.SmoothForm.mpullback_symplectizationLift_symplectization: lifts of conformal maps of one-forms preserve the symplectization form.
• TauCeti.SmoothForm.eq_symplectizationLift_of_mpullback_symplectization_eq: uniqueness of the strict lift.

References

• H. Geiges, An Introduction to Contact Topology, Cambridge University Press, 2008, Section 1.1 and Appendix B (symplectization).
• D. McDuff, D. Salamon, Introduction to Symplectic Topology, 3rd ed., Oxford, 2017, Section 3.5 (the symplectization of a contact manifold).

noncomputable def TauCeti.SmoothForm.symplectization {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 (↑⊤) M] (α : SmoothForm I M ℝ 1) : SmoothForm ((modelWithCornersSelf ℝ ℝ).prod I) (ℝ × M) ℝ 1

The symplectization form eᵗ α on ℝ × M of a one-form α on M, where t is the real coordinate and α is pulled back along the projection to M. When α is a contact form, its exterior derivative is a symplectic form (TauCeti.SmoothForm.isSymplectic_mextDerivₗ_symplectization_iff).

theorem TauCeti.SmoothForm.coe_symplectization {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 (↑⊤) M] (α : SmoothForm I M ℝ 1) : ↑α.symplectization = fun (p : ℝ × M) => Real.exp p.1 • ↑((mpullback Prod.snd ⋯) α) p

The symplectization form is eᵗ times the pullback of the form along the projection.

@[simp]

theorem TauCeti.SmoothForm.symplectization_apply {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 (↑⊤) M] (α : SmoothForm I M ℝ 1) (p : ℝ × M) (v : TangentSpace ((modelWithCornersSelf ℝ ℝ).prod I) p) : (↑α.symplectization p) ![v] = Real.exp p.1 * (↑α p.2) ![((Manifold.tangentSpaceProdEquiv p) v).2]

The symplectization form sends a tangent vector (s, v) at (t, x) to eᵗ α_x(v).

theorem TauCeti.SmoothForm.mextDeriv_symplectization_apply {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 (↑⊤) M] (α : SmoothForm I M ℝ 1) (p : ℝ × M) (v w : TangentSpace ((modelWithCornersSelf ℝ ℝ).prod I) p) : (mextDeriv (↑α.symplectization) p) ![v, w] = Real.exp p.1 * ((NormedSpace.fromTangentSpace p.1) ((Manifold.tangentSpaceProdEquiv p) v).1 * (↑α p.2) ![((Manifold.tangentSpaceProdEquiv p) w).2] - (NormedSpace.fromTangentSpace p.1) ((Manifold.tangentSpaceProdEquiv p) w).1 * (↑α p.2) ![((Manifold.tangentSpaceProdEquiv p) v).2] + (mextDeriv (↑α) p.2) ![((Manifold.tangentSpaceProdEquiv p) v).2, ((Manifold.tangentSpaceProdEquiv p) w).2])

The exterior derivative of the symplectization form eᵗ α is eᵗ (dt ∧ α + dα): it takes the value eᵗ (s α_x(w) - s' α_x(v) + dα_x(v, w)) on tangent vectors (s, v) and (s', w) at (t, x).

theorem TauCeti.SmoothForm.eval₂_mextDerivₗ_symplectization {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 (↑⊤) M] (α : SmoothForm I M ℝ 1) (p : ℝ × M) (v w : TangentSpace ((modelWithCornersSelf ℝ ℝ).prod I) p) : SmoothBundleForm.eval₂ ((mextDerivₗ ((modelWithCornersSelf ℝ ℝ).prod I) 1) α.symplectization) p v w = Real.exp p.1 * ((NormedSpace.fromTangentSpace p.1) ((Manifold.tangentSpaceProdEquiv p) v).1 * (↑α p.2) ![((Manifold.tangentSpaceProdEquiv p) w).2] - (NormedSpace.fromTangentSpace p.1) ((Manifold.tangentSpaceProdEquiv p) w).1 * (↑α p.2) ![((Manifold.tangentSpaceProdEquiv p) v).2] + SmoothBundleForm.eval₂ ((mextDerivₗ I 1) α) p.2 ((Manifold.tangentSpaceProdEquiv p) v).2 ((Manifold.tangentSpaceProdEquiv p) w).2)

The exterior derivative of the symplectization form, evaluated as a smooth two-form on two tangent vectors.

theorem TauCeti.SmoothForm.isNondegenerate_mextDerivₗ_symplectization_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 (↑⊤) M] {α : SmoothForm I M ℝ 1} : SmoothTwoForm.IsNondegenerate ((mextDerivₗ ((modelWithCornersSelf ℝ ℝ).prod I) 1) α.symplectization) ↔ α.IsContactForm

The symplectization is symplectic. The exterior derivative d(eᵗ α) of the symplectization form is nondegenerate exactly when α is a contact form.

theorem TauCeti.SmoothForm.isSymplectic_mextDerivₗ_symplectization_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 (↑⊤) M] {α : SmoothForm I M ℝ 1} : SmoothTwoForm.IsSymplectic ((mextDerivₗ ((modelWithCornersSelf ℝ ℝ).prod I) 1) α.symplectization) ↔ α.IsContactForm

The symplectization is symplectic. The exterior derivative d(eᵗ α) of the symplectization form is a symplectic form on ℝ × M exactly when α is a contact form.

theorem TauCeti.SmoothForm.IsContactForm.isSymplectic_mextDerivₗ_symplectization {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 (↑⊤) M] {α : SmoothForm I M ℝ 1} (hα : α.IsContactForm) : SmoothTwoForm.IsSymplectic ((mextDerivₗ ((modelWithCornersSelf ℝ ℝ).prod I) 1) α.symplectization)

The exterior derivative of the symplectization form of a contact form is symplectic.

The Liouville field

theorem TauCeti.SmoothForm.interior_mextDeriv_symplectization {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 (↑⊤) M] (α : SmoothForm I M ℝ 1) : RoughForm.interior (Manifold.prodVectorField (constVectorField 1) 0) (mextDeriv ↑α.symplectization) = ↑α.symplectization

The Liouville field of the symplectization. The unit vector field ∂_t along the real factor of ℝ × M satisfies ι_(∂_t) d(eᵗ α) = eᵗ α.

theorem TauCeti.SmoothForm.isLiouvilleVectorField_symplectization {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 (↑⊤) M] (α : SmoothForm I M ℝ 1) : IsLiouvilleVectorField (mextDeriv ↑α.symplectization) (Manifold.prodVectorField (constVectorField 1) 0)

The Liouville field of the symplectization. The unit vector field ∂_t along the real factor of ℝ × M is a Liouville vector field of d(eᵗ α).

Lifts of conformal maps

noncomputable def TauCeti.symplectizationLift {M : Type u_3} {M' : Type u_6} (F : M → M') (f : M → ℝ) (p : ℝ × M) : ℝ × M'

The lift (t, x) ↦ (t - log f(x), F(x)) of a map F : M → M' to ℝ × M → ℝ × M', for a function f on M. When F pulls a one-form α' back to f α with f positive, it pulls the symplectization form of α' back to that of α (TauCeti.SmoothForm.mpullback_symplectizationLift_symplectization).

@[simp]

theorem TauCeti.symplectizationLift_apply {M : Type u_3} {M' : Type u_6} (F : M → M') (f : M → ℝ) (p : ℝ × M) : symplectizationLift F f p = (p.1 - Real.log (f p.2), F p.2)

theorem TauCeti.contMDiff_symplectizationLift {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace M'] [ChartedSpace H' M'] {F : M → M'} (hF : ContMDiff I I' (↑⊤) F) {f : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f) (hf₀ : ∀ (x : M), f x ≠ 0) : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) ((modelWithCornersSelf ℝ ℝ).prod I') (↑⊤) (symplectizationLift F f)

The lift of a smooth map along a smooth nowhere vanishing function is smooth.

theorem TauCeti.SmoothForm.mpullback_symplectization_apply_of_snd_eq {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] {F : M → M'} (hF : ContMDiff I I' (↑⊤) F) {f : M → ℝ} {α : SmoothForm I M ℝ 1} {α' : SmoothForm I' M' ℝ 1} (hα : ∀ (x : M), ↑((mpullback F hF) α') x = f x • ↑α x) {Ψ : ℝ × M → ℝ × M'} (hΨ : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) ((modelWithCornersSelf ℝ ℝ).prod I') (↑⊤) Ψ) (hcover : ∀ (p : ℝ × M), (Ψ p).2 = F p.2) (p : ℝ × M) (v : TangentSpace ((modelWithCornersSelf ℝ ℝ).prod I) p) : (↑((mpullback Ψ hΨ) α'.symplectization) p) ![v] = Real.exp (Ψ p).1 * f p.2 * (↑α p.2) ![((Manifold.tangentSpaceProdEquiv p) v).2]

Pulling back a symplectization form along a map covering F depends on its real component only through its exponential. No derivative of that component occurs.

theorem TauCeti.SmoothForm.mpullback_symplectizationLift_symplectization {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] {F : M → M'} (hF : ContMDiff I I' (↑⊤) F) {f : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f) (hf₀ : ∀ (x : M), 0 < f x) {α : SmoothForm I M ℝ 1} {α' : SmoothForm I' M' ℝ 1} (hα : ∀ (x : M), ↑((mpullback F hF) α') x = f x • ↑α x) : (mpullback (symplectizationLift F f) ⋯) α'.symplectization = α.symplectization

Lifts of conformal maps preserve the symplectization form. If a smooth map F : M → M' pulls a one-form α' back to f α, for a smooth positive function f, then its lift (t, x) ↦ (t - log f(x), F(x)) pulls the symplectization form eᵗ α' back to eᵗ α. For a contactomorphism F preserving coorientations, this is its exact symplectic lift to the symplectizations.

theorem TauCeti.SmoothForm.mpullback_symplectizationLift_neg_symplectization {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] {F : M → M'} (hF : ContMDiff I I' (↑⊤) F) {f : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f) (hf₀ : ∀ (x : M), f x < 0) {α : SmoothForm I M ℝ 1} {α' : SmoothForm I' M' ℝ 1} (hα : ∀ (x : M), ↑((mpullback F hF) α') x = f x • ↑α x) : (mpullback (symplectizationLift F (-f)) ⋯) (-α').symplectization = α.symplectization

Lifts of coorientation-reversing maps. If a smooth map F : M → M' pulls a one-form α' back to f α, for a smooth negative function f, then the lift (t, x) ↦ (t - log(-f(x)), F(x)) pulls the symplectization form eᵗ (-α') of the oppositely cooriented form back to eᵗ α. In terms of annihilator lines, it interchanges their two halves.

theorem TauCeti.SmoothForm.eq_symplectizationLift_of_mpullback_symplectization_eq {E : Type u_1} {H : Type u_2} {M : Type u_3} {E' : Type u_4} {H' : Type u_5} {M' : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] {F : M → M'} (hF : ContMDiff I I' (↑⊤) F) {f : M → ℝ} {α : SmoothForm I M ℝ 1} {α' : SmoothForm I' M' ℝ 1} (hα : ∀ (x : M), ↑((mpullback F hF) α') x = f x • ↑α x) (hα₀ : ∀ (x : M), ↑α x ≠ 0) {φ : ℝ × M → ℝ} (hφ : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) (modelWithCornersSelf ℝ ℝ) (↑⊤) φ) (h : (mpullback (fun (p : ℝ × M) => (φ p, F p.2)) ⋯) α'.symplectization = α.symplectization) : (∀ (x : M), 0 < f x) ∧ (fun (p : ℝ × M) => (φ p, F p.2)) = symplectizationLift F f

Uniqueness of the strict lift. Let a smooth map F : M → M' pull a one-form α' back to f α, where α vanishes nowhere. If a smooth map of the form (t, x) ↦ (φ(t, x), F(x)) pulls the symplectization form eᵗ α' back to eᵗ α, then f is positive and the map is the lift (t, x) ↦ (t - log f(x), F(x)). In particular a strict lift of a contactomorphism to the symplectizations has no free additive constant.