Diagonalizing symplectic matrices by symplectic matrices

Let k be a field and Q a commutative k-algebra. Suppose a symplectic matrix M over Q is diagonalized by an invertible matrix P₀ over k, with unit eigenvalues: M P₀ = P₀ diag(t). Then M is already diagonalized by a symplectic matrix P over k, and the eigenvalues can be taken paired, M P = P diag(u₁, …, uₘ, u₁⁻¹, …, uₘ⁻¹): a conjugate of M by a rational symplectic matrix lies in the paired diagonal torus.

This diagonalization supplies the linear algebra for conjugating a diagonalizable subgroup of Sp₂ₘ into the paired diagonal torus, with Q the coordinate ring of the subgroup.

Main declarations

• Matrix.exists_mem_symplecticGroup_mul_map_eq_map_mul_diagonal: the statement in Mathlib's Fin m ⊕ Fin m coordinates.
• TauCeti.GLSymplecticFin.exists_mul_map_eq_map_mul_diagonal: the statement for TauCeti.GLSymplecticFin, with the paired diagonal matrix TauCeti.GLSymplecticFin.diagonal.

References

• E. Artin, Geometric Algebra (1957), Theorem 3.7, for symplectic bases; the graded form used here is LinearMap.BilinForm.IsAlt.exists_basis_toMatrix_eq_J_of_iSup_eq_top.

theorem Matrix.exists_mem_symplecticGroup_mul_map_eq_map_mul_diagonal {k : Type u_1} {Q : Type u_2} [Field k] [CommRing Q] [Algebra k Q] {m : ℕ} {M : Matrix (Fin m ⊕ Fin m) (Fin m ⊕ Fin m) Q} (hM : M ∈ symplecticGroup (Fin m) Q) {P₀ : Matrix (Fin m ⊕ Fin m) (Fin m ⊕ Fin m) k} (hP₀ : IsUnit P₀) {t : Fin m ⊕ Fin m → Qˣ} (h : M * P₀.map ⇑(algebraMap k Q) = P₀.map ⇑(algebraMap k Q) * diagonal fun (i : Fin m ⊕ Fin m) => ↑(t i)) : ∃ P ∈ symplecticGroup (Fin m) k, ∃ (u : Fin m → Qˣ), M * P.map ⇑(algebraMap k Q) = P.map ⇑(algebraMap k Q) * diagonal fun (x : Fin m ⊕ Fin m) => ↑(Sum.elim u (fun (i : Fin m) => (u i)⁻¹) x)

A symplectic matrix diagonalized by a rational matrix is diagonalized by a rational symplectic matrix, in Mathlib's Fin m ⊕ Fin m coordinates.

If M ∈ Sp₂ₘ(Q) satisfies M P₀ = P₀ diag(t) for an invertible P₀ over k and units t of Q, then M P = P diag(u, u⁻¹) for some symplectic P over k and units u of Q.

theorem TauCeti.GLSymplecticFin.exists_mul_map_eq_map_mul_diagonal {k : Type u_1} {Q : Type u_2} [Field k] [CommRing Q] [Algebra k Q] {m : ℕ} (M : ↥(GLSymplecticFin m Q)) {P₀ : GL (Fin (m + m)) k} {t : Fin (m + m) → Qˣ} (h : ↑M * (Matrix.GeneralLinearGroup.map (algebraMap k Q)) P₀ = (Matrix.GeneralLinearGroup.map (algebraMap k Q)) P₀ * diagGL t) : ∃ (P : ↥(GLSymplecticFin m k)) (u : Fin m → Qˣ), M * (map m k (algebraMap k Q)) P = (map m k (algebraMap k Q)) P * diagonal u

A symplectic matrix diagonalized by a rational matrix is diagonalized by a rational symplectic matrix.

If M ∈ Sp₂ₘ(Q) satisfies M P₀ = P₀ diag(t) for some P₀ ∈ GL₂ₘ(k) and units t of Q, then some rational symplectic matrix P conjugates M into the paired diagonal torus: M P = P diag(u₁, …, uₘ, u₁⁻¹, …, uₘ⁻¹).