Contact covectors

A covector a on a vector space V is contact for a bilinear form B when a ≠ 0 and B restricts to a nondegenerate form on the hyperplane ker a (Module.Dual.IsContact). This is the pointwise linear algebra of a contact form on a manifold: a one-form α is contact exactly when, at every point x, the covector α_x is contact for the bilinear form dα_x.

The condition only depends on B through its values on ker a × ker a (Module.Dual.isContact_congr), and is unchanged when a or B is multiplied by a nonzero scalar. Together these give the pointwise form of the rescaling law for contact forms: since d(f α) = df ∧ α + f dα, and df ∧ α vanishes on ker α × ker α, the forms α and f α are contact together whenever f vanishes nowhere.

For an alternating B, the hyperplane ker a carries a nondegenerate alternating form, so it has even dimension and V has odd dimension (Module.Dual.IsContact.odd_finrank). A subspace of ker a on which B vanishes has at most half the dimension of ker a, so 2 dim W + 1 ≤ dim V (Module.Dual.IsContact.two_mul_finrank_add_one_le). This is the dimension bound for isotropic and Legendrian submanifolds of a contact manifold.

Contact covectors arise on hyperplanes transverse to a vector. If B is nondegenerate and alternating, L : U → V is injective and z is a vector outside the range of L which together with it spans V, then u ↦ B z (L u) is contact for the restriction B (L ·) (L ·) of B to U (Module.Dual.isContact_comp_compl₁₂). This is the pointwise reason why the primitive ι_Z ω of a symplectic form restricts to a contact form on a hypersurface transverse to Z.

The symplectization form ((s, v), (t, w)) ↦ s * a w - t * a v + B v w on K × V (Module.Dual.symplectizationForm) is nondegenerate exactly when a is contact for B (Module.Dual.isContact_iff_nondegenerate_symplectizationForm). This is the pointwise linear algebra of the symplectization: up to the factor eᵗ, it is the value of d(eᵗ α) at a point (t, x) of ℝ × M, with a = α_x and B = dα_x.

For an alternating B and a contact covector a, the bilinear form B + a ⊗ a, (v, w) ↦ B v w + a v * a w, is left-separating (Module.Dual.IsContact.separatingLeft_add_smulRight), so in finite dimension v ↦ B v + a(v) a is an isomorphism onto the dual. This is the pointwise contact flat map X ↦ ι_X dα + α(X) α of a contact form. The preimage of a itself is characterized by the Reeb equations: B r + a(r) a = a exactly when a r = 1 and B r = 0 (Module.Dual.IsContact.add_smulRight_apply_eq_self_iff).

A contact covector a on a finite-dimensional space has a Reeb vector r = a.reebVector B (Module.Dual.reebVector): the unique vector with a r = 1 which is B-orthogonal to ker a. For alternating B it spans the kernel of B, and V = ker a ⊕ K r. Replacing a by c a and B by a form agreeing with c B up to a term l ∧ a changes r into c⁻¹ r plus an explicit correction in ker a (Module.Dual.IsContact.reebVector_smul_eq_inv_smul_add_iff). This is the pointwise form of the Reeb vector field of a contact form and of its rescaling law.

Main declarations

• Module.Dual.IsContact: a ≠ 0 and B is nondegenerate on ker a.
• Module.Dual.isContact_iff_of_isRefl: for a reflexive B, the elementwise criterion: the only vector of ker a which is B-orthogonal to all of ker a is zero.
• Module.Dual.isContact_congr, Module.Dual.isContact_smul_iff, Module.Dual.isContact_smul_bilinForm_iff: invariance under changes of B off ker a and under nonzero rescaling of a and of B.
• Module.Dual.IsContact.even_finrank_ker, Module.Dual.IsContact.odd_finrank: the dimension count.
• Module.Dual.IsContact.two_mul_finrank_add_one_le: the dimension bound for subspaces of ker a on which B vanishes.
• Module.Dual.isContact_comp_compl₁₂: the covector B z restricted to a hyperplane transverse to z is contact for the restriction of a nondegenerate alternating B.
• Module.Dual.isContact_comp_linearEquiv_compl₁₂_iff, Module.Dual.IsContact.reebVector_comp_linearEquiv_compl₁₂: contactness and the Reeb vector are transported by linear equivalences.
• Module.Dual.symplectizationForm, Module.Dual.isContact_iff_nondegenerate_symplectizationForm: the symplectization form, which is nondegenerate exactly for contact covectors.
• Module.Dual.IsContact.separatingLeft_add_smulRight: B + a ⊗ a is left-separating.
• Module.Dual.IsContact.add_smulRight_apply_eq_self_iff: the preimage of a under v ↦ B v + a(v) a.
• Module.Dual.reebVector, Module.Dual.IsContact.eq_reebVector_iff: the Reeb vector and its characterization.
• Module.Dual.IsContact.ker_eq_span_reebVector, Module.Dual.IsContact.isCompl_ker_span_reebVector: the Reeb line is the kernel of B and is complementary to ker a.
• Module.Dual.IsContact.reebVector_smul_eq_inv_smul_add_iff: the rescaling law.

References

• H. Geiges, An Introduction to Contact Topology, Cambridge University Press, 2008, Section 1.1.

def Module.Dual.IsContact {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (a : Dual K V) (B : LinearMap.BilinForm K V) : Prop

A covector a is contact for a bilinear form B when it is nonzero and B restricts to a nondegenerate bilinear form on the hyperplane ker a. For a one-form α on a manifold, the covector α_x being contact for dα_x at every point x is the contact condition.

theorem Module.Dual.isContact_def {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {a : Dual K V} {B : LinearMap.BilinForm K V} : a.IsContact B ↔ a ≠ 0 ∧ (B.restrict (LinearMap.ker a)).Nondegenerate

theorem Module.Dual.IsContact.ne_zero {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {a : Dual K V} {B : LinearMap.BilinForm K V} (h : a.IsContact B) : a ≠ 0

A contact covector is nonzero.

theorem Module.Dual.IsContact.nondegenerate_restrict {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {a : Dual K V} {B : LinearMap.BilinForm K V} (h : a.IsContact B) : (B.restrict (LinearMap.ker a)).Nondegenerate

A contact covector's bilinear form is nondegenerate on its kernel.

theorem Module.Dual.isContact_iff_of_isRefl {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {a : Dual K V} {B : LinearMap.BilinForm K V} (hB : B.IsRefl) : a.IsContact B ↔ a ≠ 0 ∧ ∀ (v : V), a v = 0 → (∀ (w : V), a w = 0 → (B v) w = 0) → v = 0

For a reflexive bilinear form, and in particular for an alternating one, a covector a is contact exactly when it is nonzero and no nonzero vector of ker a is B-orthogonal to all of ker a.

theorem Module.Dual.isContact_congr {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {a : Dual K V} {B B' : LinearMap.BilinForm K V} (h : ∀ (v w : V), a v = 0 → a w = 0 → (B v) w = (B' v) w) : a.IsContact B ↔ a.IsContact B'

Whether a is contact for B only depends on the values of B on ker a × ker a.

@[simp]

theorem Module.Dual.isContact_smul_iff {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {a : Dual K V} {B : LinearMap.BilinForm K V} {c : K} (hc : c ≠ 0) : (c • a).IsContact B ↔ a.IsContact B

A nonzero multiple of a covector is contact for B exactly when the covector is.

@[simp]

theorem Module.Dual.isContact_smul_bilinForm_iff {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {a : Dual K V} {B : LinearMap.BilinForm K V} {c : K} (hc : c ≠ 0) : a.IsContact (c • B) ↔ a.IsContact B

A covector is contact for a nonzero multiple of B exactly when it is contact for B.

theorem Module.Dual.IsContact.even_finrank_ker {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) : Even (finrank K ↥(LinearMap.ker a))

For an alternating B, the kernel of a contact covector has even dimension.

theorem Module.Dual.IsContact.odd_finrank {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) : Odd (finrank K V)

A finite-dimensional space carrying a covector which is contact for an alternating bilinear form has odd dimension.

theorem Module.Dual.IsContact.two_mul_finrank_add_one_le {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] (h : a.IsContact B) {W : Submodule K V} (hWa : W ≤ LinearMap.ker a) (hWB : ∀ v ∈ W, ∀ w ∈ W, (B v) w = 0) : 2 * finrank K ↥W + 1 ≤ finrank K V

Isotropic subspaces of a contact hyperplane. If a is contact for B, then a subspace W of ker a on which B vanishes identically satisfies 2 dim W + 1 ≤ dim V. No symmetry assumption on B is needed.

Hyperplanes transverse to a vector

theorem Module.Dual.isContact_comp_compl₁₂ {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {B : LinearMap.BilinForm K V} {U : Type u_3} [AddCommGroup U] [Module K U] (hB : B.IsAlt) (hB' : LinearMap.SeparatingLeft B) {L : U →ₗ[K] V} (hL : Function.Injective ⇑L) {z : V} (hz : z ∉ L.range) (hLz : L.range ⊔ K ∙ z = ⊤) : IsContact (B z ∘ₗ L) (LinearMap.compl₁₂ B L L)

Transverse hyperplanes of a nondegenerate alternating form carry contact covectors. Let B be a nondegenerate alternating form on V, let L : U → V be injective, and let z be a vector outside the range of L which together with it spans V, so that L identifies U with a hyperplane transverse to z. Then the covector u ↦ B z (L u) on U is contact for the restricted form B (L ·) (L ·).

This is the linear algebra behind hypersurfaces of contact type: when ι_Z ω = α for a vector field Z transverse to a hypersurface, the restriction of α to the hypersurface is a contact form.

Transport along linear equivalences

@[simp]

theorem Module.Dual.isContact_comp_linearEquiv_compl₁₂_iff {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {V' : Type u_3} [AddCommGroup V'] [Module K V'] (e : V ≃ₗ[K] V') {a' : Dual K V'} {B' : LinearMap.BilinForm K V'} : IsContact (a' ∘ₗ ↑e) (LinearMap.compl₁₂ B' ↑e ↑e) ↔ a'.IsContact B'

Contactness is invariant under linear equivalences. For a linear equivalence e : V ≃ V', the pullback a' ∘ e is contact for the pullback B' ∘ (e × e) exactly when a' is contact for B'.

The symplectization form

def Module.Dual.symplectizationForm {K : Type u_3} {V : Type u_4} [CommRing K] [AddCommGroup V] [Module K V] (a : Dual K V) (B : LinearMap.BilinForm K V) : LinearMap.BilinForm K (K × V)

The symplectization form of a covector a and a bilinear form B on V: the bilinear form ((s, v), (t, w)) ↦ s * a w - t * a v + B v w on K × V. Up to the positive factor eᵗ, it is the value of d(eᵗ α) at a point (t, x) of ℝ × M, for a one-form α on a manifold M, with a = α_x and B = dα_x.

@[simp]

theorem Module.Dual.symplectizationForm_apply {K : Type u_3} {V : Type u_4} [CommRing K] [AddCommGroup V] [Module K V] {a : Dual K V} {B : LinearMap.BilinForm K V} (x y : K × V) : ((a.symplectizationForm B) x) y = x.1 * a y.2 - y.1 * a x.2 + (B x.2) y.2

theorem Module.Dual.isAlt_symplectizationForm {K : Type u_3} {V : Type u_4} [CommRing K] [AddCommGroup V] [Module K V] {a : Dual K V} {B : LinearMap.BilinForm K V} (hB : B.IsAlt) : (a.symplectizationForm B).IsAlt

The symplectization form of an alternating form is alternating.

theorem Module.Dual.flip_symplectizationForm {K : Type u_3} {V : Type u_4} [CommRing K] [AddCommGroup V] [Module K V] {a : Dual K V} {B : LinearMap.BilinForm K V} : LinearMap.flip (a.symplectizationForm B) = (-a).symplectizationForm (LinearMap.flip B)

Swapping the arguments of the symplectization form of a and B gives the symplectization form of -a and of the swapped form B.flip.

theorem Module.Dual.separatingLeft_symplectizationForm_iff {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {a : Dual K V} {B : LinearMap.BilinForm K V} : LinearMap.SeparatingLeft (a.symplectizationForm B) ↔ a ≠ 0 ∧ LinearMap.SeparatingLeft (B.restrict (LinearMap.ker a))

The symplectization form of a and B is left-separating exactly when a is nonzero and the restriction of B to ker a is left-separating.

theorem Module.Dual.isContact_iff_nondegenerate_symplectizationForm {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {a : Dual K V} {B : LinearMap.BilinForm K V} : a.IsContact B ↔ (a.symplectizationForm B).Nondegenerate

Symplectization of a contact covector. The symplectization form ((s, v), (t, w)) ↦ s * a w - t * a v + B v w on K × V is nondegenerate exactly when a is contact for B. This is the pointwise reason why d(eᵗ α) is a symplectic form on ℝ × M exactly when α is a contact form on M.

The contact flat map

theorem Module.Dual.IsContact.separatingLeft_add_smulRight {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {a : Dual K V} {B : LinearMap.BilinForm K V} (hB : B.IsAlt) (h : a.IsContact B) : LinearMap.SeparatingLeft (B + LinearMap.smulRight a a)

For an alternating B and a contact covector a, the bilinear form B + a ⊗ a, (v, w) ↦ B v w + a v * a w, is left-separating. This is the linear algebra behind the contact flat map v ↦ ι_v dα + α(v) α of a contact form, which is invertible in finite dimension.

theorem Module.Dual.IsContact.add_smulRight_apply_eq_self_iff {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {a : Dual K V} {B : LinearMap.BilinForm K V} (hB : B.IsAlt) (h : a.IsContact B) {r : V} : (B + LinearMap.smulRight a a) r = a ↔ a r = 1 ∧ B r = 0

For an alternating B and a contact covector a, a vector r solves B r + a(r) a = a exactly when a r = 1 and r is B-orthogonal to everything: these are the Reeb equations.

The Reeb vector

noncomputable def Module.Dual.reebVector {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (a : Dual K V) (B : LinearMap.BilinForm K V) : V

The Reeb vector of a covector a for a bilinear form B: a vector r with a r = 1 which is B-orthogonal to the hyperplane ker a, that is B r w = 0 whenever a w = 0. When a is contact for B on a finite-dimensional space, there is exactly one such vector (Module.Dual.IsContact.eq_reebVector_iff). If there is none, a.reebVector B is 0.

theorem Module.Dual.reebVector_congr {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {a : Dual K V} {B B' : LinearMap.BilinForm K V} (h : ∀ (v w : V), a w = 0 → (B v) w = (B' v) w) : a.reebVector B = a.reebVector B'

The Reeb vector only depends on B through its values on V × ker a.

@[simp]

theorem Module.Dual.reebVector_smul_bilinForm {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {a : Dual K V} {B : LinearMap.BilinForm K V} {c : K} (hc : c ≠ 0) : a.reebVector (c • B) = a.reebVector B

The Reeb vector does not change when B is multiplied by a nonzero scalar.

theorem Module.Dual.reebVector_spec_of_exists {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {a : Dual K V} {B : LinearMap.BilinForm K V} (hex : ∃ (r : V), a r = 1 ∧ ∀ (w : V), a w = 0 → (B r) w = 0) : a (a.reebVector B) = 1 ∧ ∀ (w : V), a w = 0 → (B (a.reebVector B)) w = 0

If a vector takes the value 1 under a and is B-orthogonal to ker a, the Reeb vector is such a vector.

theorem Module.Dual.reebVector_eq_zero_of_not_exists {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {a : Dual K V} {B : LinearMap.BilinForm K V} (hex : ¬∃ (r : V), a r = 1 ∧ ∀ (w : V), a w = 0 → (B r) w = 0) : a.reebVector B = 0

If no vector takes the value 1 under a while being B-orthogonal to ker a, the Reeb vector is the junk value 0.

theorem Module.Dual.IsContact.reebVector_smul {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {a : Dual K V} {B : LinearMap.BilinForm K V} (h : a.IsContact B) {c : K} (hc : c ≠ 0) : (c • a).reebVector B = c⁻¹ • a.reebVector B

Rescaling a contact covector by a nonzero scalar c divides its Reeb vector by c. This holds in every dimension: without a Reeb vector, both sides are the junk value 0.

theorem Module.Dual.IsContact.eq_reebVector_iff {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] (h : a.IsContact B) {r : V} : r = a.reebVector B ↔ a r = 1 ∧ ∀ (w : V), a w = 0 → (B r) w = 0

Characterization of the Reeb vector. For a contact covector a, the Reeb vector is the unique vector r with a r = 1 which is B-orthogonal to ker a.

@[simp]

theorem Module.Dual.IsContact.apply_reebVector {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] (h : a.IsContact B) : a (a.reebVector B) = 1

A contact covector takes the value 1 on its Reeb vector.

theorem Module.Dual.IsContact.apply_reebVector_of_apply_eq_zero {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] (h : a.IsContact B) {w : V} (hw : a w = 0) : (B (a.reebVector B)) w = 0

The Reeb vector is B-orthogonal to the kernel of the contact covector.

theorem Module.Dual.IsContact.reebVector_ne_zero {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] (h : a.IsContact B) : a.reebVector B ≠ 0

The Reeb vector of a contact covector is nonzero.

theorem Module.Dual.IsContact.reebVector_notMem_ker {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] (h : a.IsContact B) : a.reebVector B ∉ LinearMap.ker a

The Reeb vector of a contact covector does not lie in its kernel.

theorem Module.Dual.IsContact.isCompl_ker_span_reebVector {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] (h : a.IsContact B) : IsCompl (LinearMap.ker a) (K ∙ a.reebVector B)

The kernel of a contact covector and the line spanned by its Reeb vector are complementary: V = ker a ⊕ K r.

theorem Module.Dual.IsContact.reebVector_comp_linearEquiv_compl₁₂ {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {V' : Type u_3} [AddCommGroup V'] [Module K V'] {a' : Dual K V'} {B' : LinearMap.BilinForm K V'} (h : a'.IsContact B') (e : V ≃ₗ[K] V') : reebVector (a' ∘ₗ ↑e) (LinearMap.compl₁₂ B' ↑e ↑e) = e.symm (a'.reebVector B')

The Reeb vector is transported by linear equivalences. If a' is contact for B', then the Reeb vector of the pullback a' ∘ e for B' ∘ (e × e) is e⁻¹ of the Reeb vector of a' for B'.

theorem Module.Dual.IsContact.reebVector_smul_eq_inv_smul_add_iff {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {a : Dual K V} {B B' : LinearMap.BilinForm K V} [FiniteDimensional K V] (h : a.IsContact B) {c : K} (hc : c ≠ 0) {l : Dual K V} (hB' : ∀ (v w : V), a w = 0 → (B' v) w = c * (B v) w - l w * a v) (y : V) : (c • a).reebVector B' = c⁻¹ • a.reebVector B + y ↔ a y = 0 ∧ ∀ (w : V), a w = 0 → (B y) w = l w / c ^ 2

Rescaling law for the Reeb vector, pointwise. Let a be contact for B, let c ≠ 0, and let B' be a bilinear form with B' v w = c B v w - l w a v for w ∈ ker a. This is the situation of the contact form f α, where c = f x, l = df_x and B' = d(f α)_x. Then the Reeb vector of c a for B' is c⁻¹ r + y, where r is the Reeb vector of a for B and y is the unique vector of ker a with B y w = l w / c ^ 2 for all w ∈ ker a.

@[simp]

theorem Module.Dual.IsContact.apply_reebVector_left {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) (w : V) : (B (a.reebVector B)) w = 0

For an alternating B, the Reeb vector of a contact covector lies in the kernel of B: B r w = 0 for every w, not only for w ∈ ker a.

@[simp]

theorem Module.Dual.IsContact.apply_reebVector_right {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) (w : V) : (B w) (a.reebVector B) = 0

For an alternating B, every vector is B-orthogonal to the Reeb vector from the left.

theorem Module.Dual.IsContact.reebVector_mem_ker {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) : a.reebVector B ∈ LinearMap.ker B

For an alternating B, the Reeb vector of a contact covector lies in the kernel of B.

theorem Module.Dual.IsContact.eq_reebVector_iff_of_isAlt {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) {r : V} : r = a.reebVector B ↔ a r = 1 ∧ B r = 0

For an alternating B, the Reeb vector of a contact covector is the unique vector r with a r = 1 and B r = 0.

theorem Module.Dual.IsContact.ker_eq_span_reebVector {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) : LinearMap.ker B = K ∙ a.reebVector B

For an alternating B, the kernel of B is the line spanned by the Reeb vector of a contact covector.