The linear normal form of a contact covector

On Kⁿ × Kⁿ × K, with coordinates (q, p, z), the standard contact covector is dz (TauCeti.stdContactCovector) and the standard contact bilinear form is Σᵢ dqᵢ ∧ dpᵢ, ((q, p, z), (q', p', z')) ↦ q ⬝ᵥ p' - p ⬝ᵥ q' (TauCeti.stdContactBilinForm). These are the values at the origin of the standard contact form dz - Σᵢ pᵢ dqᵢ and of its exterior derivative. The standard covector is contact for the standard form (TauCeti.isContact_stdContactCovector), with Reeb vector ∂_z = (0, 0, 1) (TauCeti.reebVector_stdContactCovector).

This file proves that every contact covector is standard in suitable linear coordinates. If a is contact for an alternating form B on a finite-dimensional space V, there is a linear equivalence e : V ≃ Kⁿ × Kⁿ × K with a = dz ∘ e and B = (Σᵢ dqᵢ ∧ dpᵢ) ∘ (e × e) (Module.Dual.IsContact.exists_linearEquiv_eq_stdContact). Conversely such coordinates make a contact for B (Module.Dual.isContact_iff_exists_linearEquiv_eq_stdContact). Consequently any two contact covectors for alternating forms on spaces of the same dimension are carried to each other by a linear equivalence that also carries one form to the other (Module.Dual.IsContact.exists_linearEquiv_of_finrank_eq).

The coordinates are built from the splitting V = ker a ⊕ K r along the Reeb vector r, and a symplectic basis of the nondegenerate alternating form that B restricts to on ker a (LinearMap.BilinForm.IsAlt.exists_basis_toMatrix_eq_J). They map the Reeb vector to ∂_z, as both contactness and the Reeb vector are transported by linear equivalences (Module.Dual.isContact_comp_linearEquiv_compl₁₂_iff, Module.Dual.IsContact.reebVector_comp_linearEquiv_compl₁₂).

This is the pointwise normal form underlying the contact Darboux theorem: at a point of a contact manifold, the contact form and its exterior derivative take the standard values in a suitable basis of the tangent space.

References

• H. Geiges, An Introduction to Contact Topology, Cambridge University Press, 2008, Section 2.5 (the linear algebra behind the contact Darboux theorem).

def TauCeti.stdContactCovector (K : Type u_1) [CommRing K] (n : ℕ) : Module.Dual K ((Fin n → K) × (Fin n → K) × K)

The standard contact covector dz on Kⁿ × Kⁿ × K, with coordinates (q, p, z). It is the value at the origin of the standard contact form dz - Σᵢ pᵢ dqᵢ.

@[simp]

theorem TauCeti.stdContactCovector_apply (K : Type u_1) [CommRing K] (n : ℕ) (x : (Fin n → K) × (Fin n → K) × K) : (stdContactCovector K n) x = x.2.2

def TauCeti.stdContactBilinForm (K : Type u_1) [CommRing K] (n : ℕ) : LinearMap.BilinForm K ((Fin n → K) × (Fin n → K) × K)

The standard contact bilinear form Σᵢ dqᵢ ∧ dpᵢ on Kⁿ × Kⁿ × K, with coordinates (q, p, z): ((q, p, z), (q', p', z')) ↦ q ⬝ᵥ p' - p ⬝ᵥ q'. It is the exterior derivative of the standard contact form dz - Σᵢ pᵢ dqᵢ.

@[simp]

theorem TauCeti.stdContactBilinForm_apply (K : Type u_1) [CommRing K] (n : ℕ) (x y : (Fin n → K) × (Fin n → K) × K) : ((stdContactBilinForm K n) x) y = x.1 ⬝ᵥ y.2.1 - x.2.1 ⬝ᵥ y.1

theorem TauCeti.isAlt_stdContactBilinForm (K : Type u_1) [CommRing K] (n : ℕ) : (stdContactBilinForm K n).IsAlt

The standard contact bilinear form is alternating.

theorem TauCeti.isContact_stdContactCovector (K : Type u_2) [Field K] (n : ℕ) : (stdContactCovector K n).IsContact (stdContactBilinForm K n)

The standard contact covector dz is contact for the standard bilinear form Σᵢ dqᵢ ∧ dpᵢ.

@[simp]

theorem TauCeti.reebVector_stdContactCovector {K : Type u_1} [Field K] {n : ℕ} : (stdContactCovector K n).reebVector (stdContactBilinForm K n) = (0, 0, 1)

The Reeb vector of the standard contact covector is ∂_z = (0, 0, 1).

The normal form

theorem Module.Dual.IsContact.exists_linearEquiv_eq_stdContact {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {a : Dual K V} {B : LinearMap.BilinForm K V} [FiniteDimensional K V] (hB : B.IsAlt) (h : a.IsContact B) : ∃ (n : ℕ) (e : V ≃ₗ[K] (Fin n → K) × (Fin n → K) × K), TauCeti.stdContactCovector K n ∘ₗ ↑e = a ∧ LinearMap.compl₁₂ (TauCeti.stdContactBilinForm K n) ↑e ↑e = B

Linear normal form of a contact covector. If a is contact for an alternating form B on a finite-dimensional space V, there are linear coordinates e : V ≃ Kⁿ × Kⁿ × K in which a is the standard contact covector dz and B is the standard form Σᵢ dqᵢ ∧ dpᵢ. Such coordinates send the Reeb vector of a to ∂_z (Module.Dual.IsContact.reebVector_comp_linearEquiv_compl₁₂, TauCeti.reebVector_stdContactCovector).

theorem Module.Dual.isContact_iff_exists_linearEquiv_eq_stdContact {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {a : Dual K V} {B : LinearMap.BilinForm K V} [FiniteDimensional K V] (hB : B.IsAlt) : a.IsContact B ↔ ∃ (n : ℕ) (e : V ≃ₗ[K] (Fin n → K) × (Fin n → K) × K), TauCeti.stdContactCovector K n ∘ₗ ↑e = a ∧ LinearMap.compl₁₂ (TauCeti.stdContactBilinForm K n) ↑e ↑e = B

Contact covectors are those with standard linear coordinates. For an alternating form B on a finite-dimensional space, a is contact for B exactly when some linear coordinates e : V ≃ Kⁿ × Kⁿ × K make a the standard covector dz and B the standard form Σᵢ dqᵢ ∧ dpᵢ.

theorem Module.Dual.IsContact.exists_linearEquiv_of_finrank_eq {K : Type u_1} {V : Type u_2} {V' : Type u_3} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup V'] [Module K V'] {a : Dual K V} {B : LinearMap.BilinForm K V} [FiniteDimensional K V] [FiniteDimensional K V'] (hB : B.IsAlt) (h : a.IsContact B) {a' : Dual K V'} {B' : LinearMap.BilinForm K V'} (hB' : B'.IsAlt) (h' : a'.IsContact B') (hV : finrank K V = finrank K V') : ∃ (e : V ≃ₗ[K] V'), a' ∘ₗ ↑e = a ∧ LinearMap.compl₁₂ B' ↑e ↑e = B

Uniqueness of linear contact structures. Two contact covectors for alternating forms, on finite-dimensional spaces of the same dimension, are carried to each other by a linear equivalence which also carries one form to the other.