Darboux's theorem on symplectic manifolds #
Let form be a symplectic two-form (TauCeti.SmoothTwoForm.IsSymplectic: closed and fiberwise
nondegenerate) on a smooth manifold M with finite-dimensional real model space E. Darboux's
theorem states that around any interior point x₀ of M—in particular, around every point when
M is boundaryless—there is a smooth partial diffeomorphism chart from M to E with
x₀ ∈ chart.source and chart x₀ = 0 in which form becomes constant: for every
x ∈ chart.source and v, w : TangentSpace I x,
form.eval₂ x v w = form₀ (mvfderiv I chart x v) (mvfderiv I chart x w).
Equivalently (TauCeti.SmoothTwoForm.mpullback_constSmooth_eq_mpullback_subtype_val_iff), on the
open submanifold chart.source, pulling the constant smooth symplectic form form₀.constSmooth
back along chart recovers the restriction of form.
Because any two symplectic forms on E are continuous-linearly symplectomorphic
(TauCeti.SymplecticForm.exists_isSymplectomorphism), the model symplectic form form₀ on E may
be prescribed arbitrarily (IsSymplectic.exists_darbouxChart_of_symplecticForm). Composing instead
with a Darboux-basis isomorphism to EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n) produces
standard Euclidean Darboux coordinates pulling TauCeti.stdSymplecticForm back to form
(IsSymplectic.exists_standardDarbouxChart), and using a basis adapted to a nonzero vector
straightens any prescribed nonzero tangent vector at x₀ to (0, EuclideanSpace.single 0 1) or
(EuclideanSpace.single 0 1, 0).
The proof reads form in the preferred extended chart at x₀ on the interior of its target,
applies the centred flat Moser–Darboux theorem
TauCeti.exists_diffeomorph_centered_forall_mem_eq_compContinuousLinearMap_fderiv, composes its
diffeomorphism with the extended chart restricted to an open set
(TauCeti.exists_partialDiffeomorph_comp_extChartAt), and transports the constant model form along
continuous linear symplectomorphisms.
Main declarations #
TauCeti.SmoothTwoForm.IsSymplectic.exists_darbouxChart_of_isInteriorPointandTauCeti.SmoothTwoForm.IsSymplectic.exists_darbouxChart: Darboux charts into the model spaceE.TauCeti.SmoothTwoForm.IsSymplectic.exists_darbouxChart_of_symplecticForm_of_isInteriorPointandTauCeti.SmoothTwoForm.IsSymplectic.exists_darbouxChart_of_symplecticForm: Darboux charts pulling back any prescribedform₀ : SymplecticForm E.TauCeti.SmoothTwoForm.IsSymplectic.exists_standardDarbouxChart,TauCeti.SmoothTwoForm.IsSymplectic.exists_standardDarbouxChart_of_finrank_eq, and their_of_isInteriorPointcounterparts: standard Euclidean Darboux charts ontoEuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n)withstdSymplecticForm.TauCeti.SmoothTwoForm.IsSymplectic.exists_standardDarbouxChart_snd_single,TauCeti.SmoothTwoForm.IsSymplectic.exists_standardDarbouxChart_fst_single, and their_of_isInteriorPointcounterparts: standard Euclidean Darboux charts straightening a prescribed nonzero tangent vector atx₀.
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., Springer, 2013, Theorem 22.13.
Darboux's theorem at an interior point. Around any interior point x₀ of a smooth manifold
carrying a symplectic two-form form, there are a smooth partial diffeomorphism chart into the
model space E with x₀ ∈ chart.source and chart x₀ = 0 and a constant symplectic form form₀
on E whose pullback by mvfderiv I chart equals form on chart.source.
Darboux's theorem for a prescribed model symplectic form at an interior point. Around any
interior point x₀ of (M, form) and for any chosen symplectic form form₀ on E, there is a
centered smooth partial diffeomorphism pulling form₀ back to form.
Standard Euclidean Darboux coordinates at an interior point. Around any interior point x₀
of (M, form), there are n : ℕ and a smooth partial diffeomorphism onto an open neighborhood of
0 in EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n) pulling stdSymplecticForm back to
form.
Standard Euclidean Darboux coordinates at fixed dimension 2 * n (interior point).
Standard Euclidean Darboux coordinates straightening a nonzero tangent vector to
(0, single 0 1) at an interior point.
Standard Euclidean Darboux coordinates straightening a nonzero tangent vector to
(single 0 1, 0) at an interior point.
Darboux's theorem. Around every point x₀ of a finite-dimensional boundaryless symplectic
manifold (M, form), there are a smooth partial diffeomorphism chart into E with
x₀ ∈ chart.source and chart x₀ = 0 and a constant symplectic form form₀ on E whose pullback
by mvfderiv I chart equals form on chart.source.
Darboux's theorem for a prescribed model symplectic form. Around every point x₀ of a
finite-dimensional boundaryless symplectic manifold (M, form) and for any symplectic form form₀
on E, there is a centered smooth partial diffeomorphism pulling form₀ back to form.
Standard Euclidean Darboux coordinates. Around every point x₀ of a finite-dimensional
boundaryless symplectic manifold (M, form), there are n : ℕ and a smooth partial diffeomorphism
onto an open neighborhood of 0 in EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin n) pulling
stdSymplecticForm back to form.
Standard Euclidean Darboux coordinates at fixed dimension 2 * n.
Standard Euclidean Darboux coordinates straightening a nonzero tangent vector to
(0, single 0 1).
Standard Euclidean Darboux coordinates straightening a nonzero tangent vector to
(single 0 1, 0).