Darboux's theorem

Let ω be a closed differential two-form on an open subset W of a finite-dimensional real normed space V, of class C^r with r ≥ 1, and nondegenerate at a point x₀ ∈ W. Darboux's theorem says that near x₀ the form ω is constant in suitable coordinates: there is a C^r diffeomorphism ψ of V fixing x₀ with ψ^* ω = ω(x₀) on a neighbourhood of x₀ (TauCeti.exists_diffeomorph_eventually_compContinuousLinearMap_fderiv_eq). Its inverse is therefore a chart around x₀ in which ω is the constant form ω(x₀). Choosing a symplectic basis of the constant nondegenerate form ω(x₀) is a separate linear step, which turns these coordinates into the classical ones with ω = ∑ dxᵢ ∧ dyᵢ.

The proof is Moser's deformation argument, which this file states in its local form (TauCeti.exists_diffeomorph_eventually_compContinuousLinearMap_fderiv_eq_of_extDeriv_eq). Let ω₀, ω₁ be closed two-forms near x₀ which agree and are nondegenerate at x₀, and let α be a one-form with dα = ω₁ - ω₀ and α(x₀) = 0. Along the straight-line family ωₜ = (1 - t) ω₀ + t ω₁, which is nondegenerate near x₀ for all t ∈ [0, 1], the Moser field Xₜ is defined by ι_{Xₜ} ωₜ = -α (TauCeti.exists_contDiffOn_moserField). It vanishes wherever α does, in particular at x₀, so its time-dependent flow ψₜ exists near x₀ up to time one and fixes the zeros of α (TauCeti.exists_eventually_forall_hasDerivAt_fderiv_of_contDiffOn), and Moser's identity (TauCeti.compContinuousLinearMap_fderiv_eq_of_curryLeft_eq_neg) gives ψ₁^* ω₁ = ψ₀^* ω₀ = ω₀ near x₀. For Darboux's theorem, ω₀ is the constant form ω(x₀), ω₁ = ω, and the Poincaré lemma on a ball around x₀ supplies α. Choosing α to vanish along a submanifold instead gives the relative Darboux theorem, in TauCeti.Geometry.Symplectic.Darboux.Relative.

Forms are Mathlib's continuous alternating maps, V [⋀^Fin 2]→L[ℝ] ℝ, with Mathlib's exterior derivative extDeriv, and the pullback of ω along ψ at x is (ω (ψ x)).compContinuousLinearMap (fderiv ℝ ψ x). Nondegeneracy of ω(x₀) is the statement that no nonzero vector v has ω(x₀)(v, w) = 0 for every w.

References

• D. McDuff and D. Salamon, Introduction to Symplectic Topology, 3rd ed., Oxford, 2017, Section 3.2 (Moser's argument and Darboux's theorem).
• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Theorem 22.13 (Darboux's theorem).

theorem TauCeti.exists_diffeomorph_eventually_compContinuousLinearMap_fderiv_eq_of_extDeriv_eq {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {ω₀ ω₁ : V → V [⋀^Fin 2]→L[ℝ] ℝ} {α : V → V [⋀^Fin 1]→L[ℝ] ℝ} {W : Set V} {x₀ : V} {r : ℕ∞} (hr : 1 ≤ r) (hW : IsOpen W) (hx₀ : x₀ ∈ W) (hω₀ : ContDiffOn ℝ (↑r) ω₀ W) (hω₁ : ContDiffOn ℝ (↑r) ω₁ W) (hα : ContDiffOn ℝ (↑r) α W) (hdω₀ : ∀ x ∈ W, extDeriv ω₀ x = 0) (hdω₁ : ∀ x ∈ W, extDeriv ω₁ x = 0) (hdα : ∀ x ∈ W, extDeriv α x = ω₁ x - ω₀ x) (hα₀ : α x₀ = 0) (heq : ω₁ x₀ = ω₀ x₀) (hnd : ∀ (v : V), (∀ (w : V), (ω₀ x₀) ![v, w] = 0) → v = 0) : ∃ (ψ : Diffeomorph (modelWithCornersSelf ℝ V) (modelWithCornersSelf ℝ V) V V ↑r), (∀ᶠ (x : V) in nhds x₀, α x = 0 → ψ x = x) ∧ ∀ᶠ (x : V) in nhds x₀, (ω₁ (ψ x)).compContinuousLinearMap (fderiv ℝ (⇑ψ) x) = ω₀ x

Moser's lemma, local form. Let ω₀, ω₁ be closed C^r two-forms (r ≥ 1) on an open subset W of a finite-dimensional real normed space, with ω₁ - ω₀ = dα on W for a C^r one-form α vanishing at x₀ ∈ W. If ω₀ and ω₁ agree at x₀ and are nondegenerate there, then some C^r diffeomorphism ψ of the space pulls ω₁ back to ω₀ on a neighbourhood of x₀. Moreover ψ fixes, near x₀, every point at which α vanishes; in particular ψ x₀ = x₀.

theorem TauCeti.exists_diffeomorph_eventually_compContinuousLinearMap_fderiv_eq {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {ω : V → V [⋀^Fin 2]→L[ℝ] ℝ} {W : Set V} {x₀ : V} {r : ℕ∞} (hr : 1 ≤ r) (hW : IsOpen W) (hx₀ : x₀ ∈ W) (hω : ContDiffOn ℝ (↑r) ω W) (hdω : ∀ x ∈ W, extDeriv ω x = 0) (hnd : ∀ (v : V), (∀ (w : V), (ω x₀) ![v, w] = 0) → v = 0) : ∃ (ψ : Diffeomorph (modelWithCornersSelf ℝ V) (modelWithCornersSelf ℝ V) V V ↑r), ψ x₀ = x₀ ∧ ∀ᶠ (x : V) in nhds x₀, (ω (ψ x)).compContinuousLinearMap (fderiv ℝ (⇑ψ) x) = ω x₀

Darboux's theorem. A closed C^r two-form ω (r ≥ 1) on an open subset of a finite-dimensional real normed space, nondegenerate at x₀, is constant in suitable coordinates near x₀: there is a C^r diffeomorphism ψ of the space fixing x₀ such that the pullback ψ^* ω equals the constant form ω(x₀) on a neighbourhood of x₀.

theorem TauCeti.exists_diffeomorph_centered_forall_mem_eq_compContinuousLinearMap_fderiv {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {ω : V → V [⋀^Fin 2]→L[ℝ] ℝ} {W : Set V} {x₀ : V} {r : ℕ∞} (hr : 1 ≤ r) (hW : IsOpen W) (hx₀ : x₀ ∈ W) (hω : ContDiffOn ℝ (↑r) ω W) (hdω : ∀ x ∈ W, extDeriv ω x = 0) (hnd : ∀ (v : V), (∀ (w : V), (ω x₀) ![v, w] = 0) → v = 0) : ∃ (Φ : Diffeomorph (modelWithCornersSelf ℝ V) (modelWithCornersSelf ℝ V) V V ↑r) (V₀ : Set V), Φ x₀ = 0 ∧ IsOpen V₀ ∧ x₀ ∈ V₀ ∧ V₀ ⊆ W ∧ ∀ y ∈ V₀, ω y = (ω x₀).compContinuousLinearMap (fderiv ℝ (⇑Φ) y)

Darboux's theorem, centred inverse form. In the situation of exists_diffeomorph_eventually_compContinuousLinearMap_fderiv_eq, subtracting x₀ from the inverse of the diffeomorphism gives a C^r diffeomorphism Φ of the space with Φ x₀ = 0 such that the form ω is, on an open neighbourhood V₀ ⊆ W of x₀, the pullback of the constant form ω(x₀) by Φ.