A symmetric matrix pivot for Gaussian elimination

Let A and C be two square matrices over a field. If their kernels meet trivially and Aᵀ C = Cᵀ A, then some symmetric matrix X makes A + X C invertible. Applied to the left blocks of a symplectic matrix, this says that multiplication by an upper symplectic unipotent can make the upper-left block invertible. This is the pivot step in the Gaussian decomposition of the symplectic group.

Main result

• TauCeti.exists_isSymm_isUnit_add_mul_of_ker_inter_eq_bot_of_transpose_mul_comm constructs the symmetric pivot.

References

• J. Dieudonné, La géométrie des groupes classiques, Chapter II, §1.

The proof is adapted from Mathlib's private lemma Matrix.SymplecticGroup.exists_symmetric_X_invertible_add_mul_of_ker_inter_eq_bot in Mathlib.LinearAlgebra.SymplecticGroup (Apache-2.0). It is made public here because symplectic Gaussian generation needs the constructed symmetric pivot, while Mathlib uses it only internally to prove that symplectic matrices have determinant one.

theorem TauCeti.exists_isSymm_isUnit_add_mul_of_ker_inter_eq_bot_of_transpose_mul_comm {K : Type u} [Field K] {l : Type u_1} [Fintype l] [DecidableEq l] {A C : Matrix l l K} (hker : ∀ (x : l → K), A • x = 0 → C • x = 0 → x = 0) (hcomm : A.transpose * C = C.transpose * A) : ∃ (X : Matrix l l K), X.IsSymm ∧ IsUnit (A + X * C)

Given square matrices A and C over a field, if the only vector annihilated by both is zero and Aᵀ C = Cᵀ A, then a symmetric left multiplier makes A + X C invertible.