Contact forms #
A real one-form α on a manifold M is a contact form when, at every point x, the covector
α_x is nonzero and the two-form dα_x is nondegenerate on the hyperplane ker α_x
(TauCeti.SmoothForm.IsContactForm). Its kernel ξ = ker α (TauCeti.SmoothForm.kerDistribution)
is then a field of hyperplanes, the contact distribution. Pointwise, this is the linear condition
Module.Dual.IsContact applied to α_x and dα_x.
This intrinsic formulation needs no dimension index. In finite dimension it forces the model
space to have odd dimension 2 n + 1 (TauCeti.SmoothForm.IsContactForm.odd_finrank), and the
contact distribution then has rank 2 n
(TauCeti.SmoothForm.IsContactForm.finrank_kerDistribution_add_one). At each point the form
and its exterior derivative are then the standard dz and Σᵢ dqᵢ ∧ dpᵢ in suitable linear
coordinates on the tangent space
(TauCeti.SmoothForm.IsContactForm.exists_linearEquiv_eq_stdContact).
Only the hyperplane field ξ is invariant: multiplying α by a nowhere vanishing C¹ function
f leaves ξ unchanged and gives again a contact form
(TauCeti.SmoothForm.isContactForm_iff_of_eq_smul). The proof is the Leibniz rule
d(f α) = df ∧ α + f dα: the term df ∧ α vanishes on ξ × ξ, so on ξ the form d(f α) is
f dα. In particular -α, which defines the opposite coorientation of ξ, is again a contact
form (TauCeti.SmoothForm.isContactForm_neg_iff).
A rough one-form satisfies the pointwise condition TauCeti.IsContactFormAt at x when it is
nonzero there and its exterior derivative is nondegenerate on its kernel. This condition imposes
no global regularity. For a smooth one-form it agrees with the canonical contact condition, by
TauCeti.SmoothForm.isContactForm_iff_forall_isContactFormAt. For a one-form and a scalar
function that are both differentiable at x, rescaling by the function preserves the pointwise
condition whenever its value at x is nonzero (TauCeti.isContactFormAt_fun_smul_iff).
Main declarations #
TauCeti.SmoothForm.kerDistribution: the hyperplane fieldker αof a real one-form.TauCeti.SmoothForm.IsContactForm: the contact condition.TauCeti.SmoothForm.isContactForm_def,TauCeti.SmoothForm.isContactForm_iff: the pointwise and elementwise statements of the contact condition.TauCeti.SmoothForm.isContactForm_iff_of_eq_smul,TauCeti.SmoothForm.kerDistribution_of_eq_smul: rescaling by a nowhere vanishing function.TauCeti.SmoothForm.isContactForm_smul_iff,TauCeti.SmoothForm.isContactForm_neg_iff: rescaling by a nonzero constant.TauCeti.SmoothForm.IsContactForm.odd_finrank: contact manifolds are odd-dimensional.TauCeti.SmoothForm.IsContactForm.exists_linearEquiv_eq_stdContact: at each point, a contact form and its exterior derivative are standard in suitable linear coordinates.TauCeti.IsContactFormAt: the pointwise contact condition for a rough one-form, withTauCeti.isContactFormAt_neg_iff,TauCeti.isContactFormAt_fun_smul_iffandTauCeti.SmoothForm.isContactForm_iff_forall_isContactFormAt.
References #
- H. Geiges, An Introduction to Contact Topology, Cambridge University Press, 2008, Sections 1.1 and 2.1.
- D. McDuff, D. Salamon, Introduction to Symplectic Topology, 3rd ed., Oxford, 2017, Section 3.5.
The kernel ker α_x of a real one-form α at each point x, as a family of subspaces of
the tangent spaces. For a contact form this is the contact distribution.
Instances For
The kernel distribution of a smooth one-form is the pointwise kernel of its underlying rough form.
At each point, kerDistribution α is the kernel of the covector α_x.
A real one-form α is a contact form when, at every point x, the covector α_x is
nonzero and dα_x restricts to a nondegenerate bilinear form on ker α_x.
Instances For
The contact condition, pointwise: at each point, α_x is a contact covector for dα_x.
The contact condition, elementwise: at each point α does not vanish, and the only vector
of ker α which is dα-orthogonal to all of ker α is zero.
A contact form does not vanish.
A contact form vanishes nowhere.
Two one-forms with the same kernels vanish at the same points: a covector vanishes exactly when its kernel is the whole tangent space.
If β = f α for a nowhere vanishing function f, then α and β have the same kernel.
Rescaling of contact forms. If β = f α for a nowhere vanishing C¹ function f, then
β is a contact form exactly when α is.
A nonzero constant multiple of a one-form has the same kernel as the form.
The negative of a one-form has the same kernel as the form.
A nonzero constant multiple of a one-form is a contact form exactly when the form is.
The negative of a one-form, which defines the opposite coorientation of its kernel, is a contact form exactly when the form is.
The contact distribution of a contact form has codimension one.
The model space of a manifold carrying a contact form is odd-dimensional, as soon as the manifold is nonempty.
Linear normal form of a contact form at a point. At each point x, there are linear
coordinates e : T_x M ≃ ℝⁿ × ℝⁿ × ℝ on the tangent space in which α_x is the standard contact
covector dz and dα_x is the standard form Σᵢ dqᵢ ∧ dpᵢ. These are the values at the origin
of the standard contact form dz - Σᵢ pᵢ dqᵢ and of its exterior derivative.
A one-form α is a contact form at x when α_x ≠ 0 and dα_x is nondegenerate on the
hyperplane ker α_x: the only vector of ker α_x that is dα_x-orthogonal to all of
ker α_x is zero. This is the pointwise algebraic condition only: it imposes no regularity on α,
and is meaningful when α is differentiable at x. The global notion
TauCeti.SmoothForm.IsContactForm is defined on smooth forms.
A contact form does not vanish, so its kernel is a hyperplane.
- nondegenerate (v : TangentSpace I x) : v ∈ α.ker x → (∀ w ∈ α.ker x, (mextDeriv α x) ![v, w] = 0) → v = 0
The exterior derivative of a contact form is nondegenerate on its kernel.
Instances For
Reversing the coorientation, α ↦ -α, preserves the contact condition.
Rescaling a contact form: for a one-form α differentiable at x and a function f
differentiable at x with f x ≠ 0, the one-form f α is a contact form at x exactly when
α is. On ker α_x the Leibniz rule reads d(f α)_x = f x • dα_x.
A smooth one-form is contact exactly when it satisfies the pointwise contact condition at every point.