The relative Darboux theorem in adapted coordinates

Let E and N be finite-dimensional real normed spaces. In adapted coordinates an embedded submanifold is the zero section E × {0} of E × N, included by q ↦ (q, 0), whose differential is ContinuousLinearMap.inl ℝ E N. Let ω₀, ω₁ be closed two-forms of class C^r (r ≥ 1) near a point (q₀, 0), nondegenerate at that point, with the same pullback to the zero section: ω₀(q, 0) and ω₁(q, 0) agree on pairs of vectors of E × {0}, for every q. The pullbacks may have any rank, and away from the zero section the forms are unrelated.

The relative Darboux theorem (TauCeti.exists_diffeomorph_fix_zeroSection_eventually_compContinuousLinearMap_fderiv_eq) says that ω₀ and ω₁ have symplectomorphic germs at (q₀, 0) by a germ fixing the zero section: some C^r diffeomorphism ψ of E × N fixes every point (q, 0) with q near q₀, and pulls ω₁ back to ω₀ near (q₀, 0).

It is proved in two steps.

• The relative Moser step treats the case where ω₀ and ω₁ agree as full forms at (q₀, 0). On a ball around (q₀, 0), which is stable under the fibre scaling (q, n) ↦ (q, t • n) for t ∈ [0, 1], the relative Poincaré lemma (Convex.exists_contDiffOn_relative_primitive) gives a one-form β with dβ = ω₁ - ω₀, vanishing as a full covector at every point of the zero section since ω₁ - ω₀ pulls back to zero there. Moser's lemma (TauCeti.exists_diffeomorph_eventually_compContinuousLinearMap_fderiv_eq_of_extDeriv_eq) applied to this primitive gives a diffeomorphism fixing the zeros of β, hence the zero section.
• The linear step (TauCeti.exists_continuousLinearEquiv_fix_inl_of_compContinuousLinearMap_inl_eq). The identity of E × {0} preserves the restrictions of the forms at (q₀, 0), so Witt's extension theorem (TauCeti.SymplecticForm.exists_isSymplectomorphism_extend) extends it to a linear symplectomorphism A from (E × N, ω₀(q₀, 0)) to (E × N, ω₁(q₀, 0)). It fixes the zero section pointwise, so A^* ω₁ agrees with ω₀ as a full form at (q₀, 0) and has the same pullback to the zero section as ω₀; hence the relative Moser step applies to ω₀ and A^* ω₁.

As in TauCeti.exists_diffeomorph_eventually_compContinuousLinearMap_fderiv_eq, forms are Mathlib's continuous alternating maps with its exterior derivative extDeriv, the pullback of ω along ψ at x is (ω (ψ x)).compContinuousLinearMap (fderiv ℝ ψ x), and nondegeneracy of ω(x) says that no nonzero v has ω(x)(v, w) = 0 for every w.

References

• A. Weinstein, Symplectic manifolds and their Lagrangian submanifolds, Advances in Mathematics 6 (1971), 329–346 (the relative Darboux theorem).
• A. Cannas da Silva, Lectures on Symplectic Geometry, Lecture Notes in Mathematics 1764, Springer, 2001, Sections 6–7 (the relative Poincaré lemma and Moser's relative theorem).
• D. McDuff and D. Salamon, Introduction to Symplectic Topology, 3rd ed., Oxford, 2017, Section 3.2 (Moser's argument).

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

The relative Darboux theorem in adapted coordinates. Let ω₀, ω₁ be closed C^r two-forms (r ≥ 1) on an open subset W of E × N containing (q₀, 0), both nondegenerate at (q₀, 0), with the same pullback to the zero section E × {0}. Then some C^r diffeomorphism ψ of E × N fixes every point (q, 0) with q near q₀ and pulls ω₁ back to ω₀ near (q₀, 0). The pullback to the zero section may be degenerate, of any rank.