The flat map of a contact form #
A one-form α on a manifold M gives at each point its contact flat map
α♭_x : T_x M → T_x^* M, v ↦ ι_v dα + α(v) α (TauCeti.SmoothForm.contactFlat). It is the sum
of the flat map v ↦ ι_v dα of the two-form dα and of the rank-one map v ↦ α(v) α, and these
maps form a smooth section of the bundle Hom(TM, Hom(TM, ℝ))
(TauCeti.SmoothForm.contMDiff_contactFlat).
For a contact form on a finite-dimensional manifold, the flat map v ↦ ι_v dα alone is never
invertible, since an alternating form in odd dimension is degenerate. Adding α ⊗ α repairs this:
every contact flat map is then invertible
(TauCeti.SmoothForm.IsContactForm.isInvertible_contactFlat). Indeed if ι_v dα + α(v) α = 0,
then evaluating at v gives α(v)² = 0, so v ∈ ker α is dα-orthogonal to ker α, and v = 0
because dα is nondegenerate on ker α. Inverting it solves the pointwise linear equations which
define vector fields from a contact form, such as the Reeb vector field R_α and contact
Hamiltonian vector fields. The Reeb vector field is the preimage of α itself: the solutions
of ι_v dα + α(v) α = α are exactly the vectors with α(v) = 1 and ι_v dα = 0
(TauCeti.SmoothForm.IsContactForm.contactFlat_apply_eq_iff), so the Reeb vector field
TauCeti.SmoothForm.reebVectorField is the inverse contact flat map applied to α
(TauCeti.SmoothForm.IsContactForm.reebVectorField_eq_inverse_contactFlat).
On smooth sections, X ↦ ι_X dα + α(X) α is a linear map from smooth vector fields to smooth
one-forms (TauCeti.SmoothForm.contactFlatₗ). For a contact form in finite dimensions it is a
linear equivalence (TauCeti.SmoothForm.IsContactForm.contactFlatEquiv), so the preimage of a
smooth one-form is a smooth vector field. In particular the Reeb vector field of a contact form is
smooth (TauCeti.SmoothForm.IsContactForm.contMDiff_reebVectorField). This smooth-section
construction and its evaluation and cancellation lemmas are adapted from the symplectic flat
equivalence TauCeti.SmoothTwoForm.IsNondegenerate.interiorEquiv and its accompanying API in
TauCeti.Geometry.Symplectic.Manifold.Flat.
Main declarations #
TauCeti.SmoothForm.contactFlat: the contact flat mapv ↦ ι_v dα + α(v) αat a point.TauCeti.SmoothForm.contMDiff_contactFlat: the contact flat maps form a smooth section.TauCeti.SmoothForm.contMDiffAt_sectionAlong_contactFlat: the contact flat maps of a smooth family of one-forms depend smoothly on the parameter.TauCeti.SmoothForm.IsContactForm.isInvertible_contactFlat: for a contact form in finite dimensions the contact flat maps are invertible.TauCeti.SmoothForm.IsContactForm.contactFlat_apply_eq_iff: the preimage ofαis characterized by the Reeb equations.TauCeti.SmoothForm.contactFlatₗ,TauCeti.SmoothForm.IsContactForm.contactFlatEquiv: the contact flat map on smooth sections, and its inverse for a contact form.TauCeti.SmoothForm.IsContactForm.contactFlatEquiv_symm_self,TauCeti.SmoothForm.IsContactForm.contMDiff_reebVectorField: the Reeb vector field corresponds toαunder the contact flat equivalence, and is smooth.TauCeti.SmoothForm.contMDiffAt_sectionAlong_reebVectorField: the Reeb vector fields of a smooth family of contact forms depend smoothly on the parameter.
References #
- H. Geiges, An Introduction to Contact Topology, Cambridge University Press, 2008, Section 1.1.
- A. Kriegl, P. W. Michor, The Convenient Setting of Global Analysis, AMS, 1997, Proposition 43.18.
The contact flat map of a real one-form α at a point x: the map
v ↦ ι_v dα + α(v) α from the tangent space to its dual. For a contact form on a
finite-dimensional manifold it is invertible
(TauCeti.SmoothForm.IsContactForm.isInvertible_contactFlat).
Instances For
The contact flat map evaluates as (v, w) ↦ dα(v, w) + α(v) α(w).
Contact flat maps of a smooth family of one-forms. Let α m be one-forms on M depending
on a parameter m ∈ N, and let b : N → M. If the values (α m)_(b m) and the exterior
derivatives (dα m)_(b m) depend C^n on m, as sections along b, then so do the contact flat
maps (α m)♭_(b m), as a section of Hom(TM, Hom(TM, ℝ)) along b.
The contact flat maps form a smooth section of the bundle Hom(TM, Hom(TM, ℝ)).
Contact flat maps of contact forms #
A vector v solves ι_v dα + α(v) α = α exactly when it satisfies the Reeb equations
α(v) = 1 and ι_v dα = 0.
The contact flat map of a contact form is invertible at every point of a finite-dimensional manifold.
The Reeb vector field of a contact form is the image of α under the inverse contact flat
map.
Smooth sections #
The contact flat map on smooth sections, X ↦ ι_X dα + α(X) α, as a linear map from smooth
vector fields to smooth one-forms.
Instances For
As a section of the bundle of covectors, ι_X dα + α(X) α is the contact flat map applied
to X.
The one-form ι_X dα + α(X) α evaluates a tangent vector as the contact flat map applied to
X.
For a contact form on a finite-dimensional manifold, X ↦ ι_X dα + α(X) α is a linear
equivalence between smooth vector fields and smooth one-forms. Its inverse sends a one-form θ
to the vector field x ↦ (α♭_x)⁻¹ θ_x.
Instances For
The contact flat equivalence is the contact flat map on smooth sections.
The vector field corresponding to a one-form θ is x ↦ (α♭_x)⁻¹ θ_x.
The contact flat map sends the vector field corresponding to θ back to θ, pointwise.
The vector field corresponding to θ is sent back to θ by X ↦ ι_X dα + α(X) α.
The Reeb vector field of a contact form is the vector field corresponding to α under the
contact flat equivalence.
The Reeb vector field of a contact form is smooth.
Reeb vector fields of a smooth family of contact forms. Let α m be one-forms on M
depending on a parameter m ∈ N which are contact forms for m near m₀, and let b : N → M.
If the values (α m)_(b m) and the exterior derivatives (dα m)_(b m) depend C^n on m, as
sections along b, then so do the Reeb vectors R_(α m)(b m), as a map to the tangent bundle.