Darboux bases of a symplectic vector space

Let ω be a symplectic form on a real vector space V. A Darboux basis of (V, ω) (TauCeti.SymplecticForm.IsDarbouxBasis) is a basis (q₁, p₁, …, qₙ, pₙ), indexed by Fin n × Fin 2 with qᵢ = b (i, 0) and pᵢ = b (i, 1), in which

ω(qᵢ, qⱼ) = 0, ω(pᵢ, pⱼ) = 0, ω(qᵢ, pⱼ) = δᵢⱼ,

so that ω = ∑ dqᵢ ∧ dpᵢ in the dual coordinates.

The relabelling TauCeti.SymplecticForm.darbouxIndexEquiv, (i, 0) ↦ inr i and (i, 1) ↦ inl i, identifies Darboux bases with the bases in which the matrix of ω is Mathlib's standard symplectic matrix Matrix.J (TauCeti.SymplecticForm.isDarbouxBasis_iff_toMatrix_reindex, and conversely TauCeti.SymplecticForm.isDarbouxBasis_reindex_symm_iff). Hence Darboux bases exist on a finite-dimensional space (TauCeti.SymplecticForm.exists_isDarbouxBasis), and any two of them have relative determinant 1 (TauCeti.SymplecticForm.IsDarbouxBasis.det_eq_one), from the corresponding facts LinearMap.BilinForm.IsAlt.exists_basis_toMatrix_eq_J and LinearMap.BilinForm.basis_det_eq_one_of_toMatrix_eq_J about nondegenerate alternating forms. Every linear symplectomorphism of (V, ω) has determinant 1 (TauCeti.SymplecticForm.IsSymplectomorphism.det_eq_one), the specialization of TauCeti.BilinForm.IsIsometry.det_eq_one_of_isAlt.

In a Darboux basis, pairing with the basis vectors reads off the coordinates of a vector: ω(qᵢ, v) is its pᵢ-coordinate and ω(pᵢ, v) is minus its qᵢ-coordinate (TauCeti.SymplecticForm.IsDarbouxBasis.apply_fst, TauCeti.SymplecticForm.IsDarbouxBasis.apply_snd).

Darboux bases are carried to Darboux bases by linear symplectomorphisms (TauCeti.SymplecticForm.IsDarbouxBasis.map), and the concatenation of Darboux bases of ω₁ and ω₂ is a Darboux basis of the direct sum ω₁ ⊕ ω₂ (TauCeti.SymplecticForm.IsDarbouxBasis.prod).

Main definitions

• TauCeti.SymplecticForm.IsDarbouxBasis ω b: b is a Darboux basis of (V, ω).
• TauCeti.SymplecticForm.darbouxIndexEquiv n: the relabelling Fin n × Fin 2 ≃ Fin n ⊕ Fin n between the Darboux and the Matrix.J index conventions.

References

• D. McDuff and D. Salamon, Introduction to Symplectic Topology, 3rd ed., Oxford, 2017, Section 2.1 (symplectic bases).
• A. Cannas da Silva, Lectures on Symplectic Geometry, Lecture Notes in Mathematics 1764, Springer, 2001, Section 1.1.

structure TauCeti.SymplecticForm.IsDarbouxBasis {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) {n : ℕ} (b : Module.Basis (Fin n × Fin 2) ℝ V) : Prop

A Darboux basis of a symplectic vector space (V, ω): a basis (q₁, p₁, …, qₙ, pₙ), with qᵢ = b (i, 0) and pᵢ = b (i, 1), satisfying ω(qᵢ, qⱼ) = 0, ω(pᵢ, pⱼ) = 0 and ω(qᵢ, pⱼ) = δᵢⱼ.

• apply_fst_fst (i j : Fin n) : (fun (v w : V) => (ω.toBilinForm v) w) (b (i, 0)) (b (j, 0)) = 0

  The vectors qᵢ pair trivially with each other.

• apply_snd_snd (i j : Fin n) : (fun (v w : V) => (ω.toBilinForm v) w) (b (i, 1)) (b (j, 1)) = 0

  The vectors pᵢ pair trivially with each other.

• apply_fst_snd (i j : Fin n) : (fun (v w : V) => (ω.toBilinForm v) w) (b (i, 0)) (b (j, 1)) = if i = j then 1 else 0

  ω(qᵢ, pⱼ) = δᵢⱼ.

theorem TauCeti.SymplecticForm.IsDarbouxBasis.apply_snd_fst {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {n : ℕ} {b : Module.Basis (Fin n × Fin 2) ℝ V} (hb : ω.IsDarbouxBasis b) (i j : Fin n) : (fun (v w : V) => (ω.toBilinForm v) w) (b (i, 1)) (b (j, 0)) = if i = j then -1 else 0

In a Darboux basis, ω(pᵢ, qⱼ) = -δᵢⱼ.

theorem TauCeti.SymplecticForm.IsDarbouxBasis.apply_fst {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {n : ℕ} {b : Module.Basis (Fin n × Fin 2) ℝ V} (hb : ω.IsDarbouxBasis b) (i : Fin n) (v : V) : (fun (v w : V) => (ω.toBilinForm v) w) (b (i, 0)) v = (b.repr v) (i, 1)

In a Darboux basis, pairing with qᵢ reads off the pᵢ-coordinate: ω(qᵢ, v) = b.repr v (i, 1).

theorem TauCeti.SymplecticForm.IsDarbouxBasis.apply_snd {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {n : ℕ} {b : Module.Basis (Fin n × Fin 2) ℝ V} (hb : ω.IsDarbouxBasis b) (i : Fin n) (v : V) : (fun (v w : V) => (ω.toBilinForm v) w) (b (i, 1)) v = -(b.repr v) (i, 0)

In a Darboux basis, pairing with pᵢ reads off minus the qᵢ-coordinate: ω(pᵢ, v) = -b.repr v (i, 0).

def TauCeti.SymplecticForm.darbouxIndexEquiv (n : ℕ) : Fin n × Fin 2 ≃ Fin n ⊕ Fin n

The relabelling (i, 0) ↦ inr i, (i, 1) ↦ inl i, under which a Darboux basis becomes a basis in which ω has Mathlib's standard symplectic matrix Matrix.J (TauCeti.SymplecticForm.isDarbouxBasis_iff_toMatrix_reindex).

@[simp]

theorem TauCeti.SymplecticForm.darbouxIndexEquiv_apply_zero {n : ℕ} (i : Fin n) : (darbouxIndexEquiv n) (i, 0) = Sum.inr i

@[simp]

theorem TauCeti.SymplecticForm.darbouxIndexEquiv_apply_one {n : ℕ} (i : Fin n) : (darbouxIndexEquiv n) (i, 1) = Sum.inl i

@[simp]

theorem TauCeti.SymplecticForm.darbouxIndexEquiv_symm_inl {n : ℕ} (i : Fin n) : (darbouxIndexEquiv n).symm (Sum.inl i) = (i, 1)

@[simp]

theorem TauCeti.SymplecticForm.darbouxIndexEquiv_symm_inr {n : ℕ} (i : Fin n) : (darbouxIndexEquiv n).symm (Sum.inr i) = (i, 0)

theorem TauCeti.SymplecticForm.isDarbouxBasis_iff_toMatrix_reindex {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {n : ℕ} {b : Module.Basis (Fin n × Fin 2) ℝ V} : ω.IsDarbouxBasis b ↔ (LinearMap.BilinForm.toMatrix (b.reindex (darbouxIndexEquiv n))) ω.toBilinForm = Matrix.J (Fin n) ℝ

A basis is a Darboux basis exactly when, relabelled by darbouxIndexEquiv, it is a basis in which the matrix of ω is Matrix.J.

theorem TauCeti.SymplecticForm.isDarbouxBasis_reindex_symm_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {n : ℕ} {d : Module.Basis (Fin n ⊕ Fin n) ℝ V} : ω.IsDarbouxBasis (d.reindex (darbouxIndexEquiv n).symm) ↔ (LinearMap.BilinForm.toMatrix d) ω.toBilinForm = Matrix.J (Fin n) ℝ

A basis d indexed by Fin n ⊕ Fin n, relabelled by darbouxIndexEquiv, is a Darboux basis exactly when the matrix of ω in d is Matrix.J.

theorem TauCeti.SymplecticForm.exists_isDarbouxBasis {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) : ∃ (n : ℕ) (b : Module.Basis (Fin n × Fin 2) ℝ V), ω.IsDarbouxBasis b

Darboux bases exist: every finite-dimensional symplectic vector space has a Darboux basis.

theorem TauCeti.SymplecticForm.exists_isDarbouxBasis_of_finrank_eq {V : Type u_1} [AddCommGroup V] [Module ℝ V] {n : ℕ} [FiniteDimensional ℝ V] (ω : SymplecticForm V) (hn : Module.finrank ℝ V = n * 2) : ∃ (b : Module.Basis (Fin n × Fin 2) ℝ V), ω.IsDarbouxBasis b

A Darboux basis exists for any prescribed number n of pairs with finrank ℝ V = n * 2.

theorem TauCeti.SymplecticForm.IsDarbouxBasis.det_eq_one {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {n : ℕ} {b c : Module.Basis (Fin n × Fin 2) ℝ V} (hb : ω.IsDarbouxBasis b) (hc : ω.IsDarbouxBasis c) : b.det ⇑c = 1

Darboux bases have unit relative determinant: the change of basis between two Darboux bases of (V, ω) is a symplectic matrix, of determinant 1.

theorem TauCeti.SymplecticForm.IsDarbouxBasis.map {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {ω : SymplecticForm V} {n : ℕ} {b : Module.Basis (Fin n × Fin 2) ℝ V} {ω' : SymplecticForm W} {e : V ≃ₗ[ℝ] W} (he : ω.IsSymplectomorphism ω' e) (hb : ω.IsDarbouxBasis b) : ω'.IsDarbouxBasis (b.map e)

A linear symplectomorphism carries Darboux bases to Darboux bases.

theorem TauCeti.SymplecticForm.IsSymplectomorphism.det_eq_one {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {e : V ≃ₗ[ℝ] V} (he : ω.IsSymplectomorphism ω e) : LinearMap.det ↑e = 1

Linear symplectomorphisms have determinant one. On an infinite-dimensional space the determinant is 1 by convention.

theorem TauCeti.SymplecticForm.IsDarbouxBasis.prod {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] {ω₁ : SymplecticForm V} {ω₂ : SymplecticForm W} {m k : ℕ} {b : Module.Basis (Fin m × Fin 2) ℝ V} {c : Module.Basis (Fin k × Fin 2) ℝ W} (hb : ω₁.IsDarbouxBasis b) (hc : ω₂.IsDarbouxBasis c) : (ω₁.prod ω₂).IsDarbouxBasis ((b.prod c).reindex ((Equiv.sumProdDistrib (Fin m) (Fin k) (Fin 2)).symm.trans (finSumFinEquiv.prodCongr (Equiv.refl (Fin 2)))))

Darboux bases of a direct sum. The concatenation of a Darboux basis b of ω₁ and a Darboux basis c of ω₂, listing the pairs of b before those of c, is a Darboux basis of ω₁ ⊕ ω₂.