Involutions of a matrix algebra

A K-linear involution φ of the matrix algebra Mₙ(K) reversing products is the adjoint involution of a nondegenerate bilinear form: φ X = C⁻¹ Xᵀ C for an invertible matrix C, which is either symmetric or skew-symmetric. Composing φ with the transpose gives an algebra automorphism, which is inner by the Skolem–Noether theorem for matrix algebras; involutivity then forces Cᵀ = ±C.

When 2 ≠ 0, the two cases are told apart by the dimension of the skew elements: when C is symmetric (an orthogonal involution), the matrices on which φ acts as -1, Mathlib's skewAdjointMatricesSubmodule C, form a space of dimension at most n(n - 1) / 2. When C is skew-symmetric (a symplectic involution), a symplectic basis of the alternating form of C conjugates φ into the standard symplectic adjoint X ↦ J⁻¹ Xᵀ J = -(J Xᵀ J), whose unitary group is Mathlib's Matrix.symplecticGroup.

Main results

• Matrix.exists_forall_eq_inv_mul_transpose_mul: an involutive anti-automorphism of Mₙ(K) is X ↦ C⁻¹ Xᵀ C with Cᵀ = C or Cᵀ = -C.
• Matrix.finrank_skewAdjointMatricesSubmodule_le_choose_two: for invertible symmetric C and 2 ≠ 0, the matrices on which X ↦ C⁻¹ Xᵀ C is -1 form a space of dimension at most n.choose 2.
• Matrix.exists_algEquiv_inv_mul_transpose_mul_eq_neg_J_mul_transpose_mul_J: for invertible skew-symmetric C and 2 ≠ 0, an algebra isomorphism Mₙ(K) ≃ M_{2m}(K) carries X ↦ C⁻¹ Xᵀ C to X ↦ -(J Xᵀ J).

References

• M.-A. Knus, A. Merkurjev, M. Rost and J.-P. Tignol, The Book of Involutions (1998), Proposition 2.7 and §2.A.

theorem Matrix.exists_forall_eq_inv_mul_transpose_mul {n : Type u_1} {K : Type u_2} [Fintype n] [DecidableEq n] [Field K] (φ : Matrix n n K →ₗ[K] Matrix n n K) (hmul : ∀ (X Y : Matrix n n K), φ (X * Y) = φ Y * φ X) (hφ : Function.Involutive ⇑φ) : ∃ (C : GL n K), ((↑C).transpose = ↑C ∨ (↑C).transpose = -↑C) ∧ ∀ (X : Matrix n n K), φ X = ↑C⁻¹ * X.transpose * ↑C

Involutions of a matrix algebra are adjoint involutions. A K-linear map of Mₙ(K) that reverses products and is its own inverse is X ↦ C⁻¹ Xᵀ C for an invertible matrix C that is either symmetric or skew-symmetric.

theorem Matrix.finrank_skewAdjointMatricesSubmodule_le_choose_two {n : Type u_1} {K : Type u_2} [Fintype n] [DecidableEq n] [Field K] [NeZero 2] {C : Matrix n n K} (hC : C.transpose = C) (hCu : IsUnit C) : Module.finrank K ↥(skewAdjointMatricesSubmodule C) ≤ (Fintype.card n).choose 2

Skew elements of an orthogonal involution. For an invertible symmetric matrix C over a field with 2 ≠ 0, the matrices that are skew-adjoint for C, that is Xᵀ C = -C X, or equivalently C⁻¹ Xᵀ C = -X, form a space of dimension at most n(n - 1) / 2: left multiplication by C embeds them into the skew-symmetric matrices, which are determined by their entries above the diagonal.

theorem Matrix.exists_algEquiv_inv_mul_transpose_mul_eq_neg_J_mul_transpose_mul_J {n : Type u_1} {K : Type u_2} [Fintype n] [DecidableEq n] [Field K] [NeZero 2] {C : GL n K} (hC : (↑C).transpose = -↑C) : ∃ (m : ℕ) (ψ : Matrix n n K ≃ₐ[K] Matrix (Fin m ⊕ Fin m) (Fin m ⊕ Fin m) K), m + m = Fintype.card n ∧ ∀ (X : Matrix n n K), ψ (↑C⁻¹ * X.transpose * ↑C) = -(J (Fin m) K * (ψ X).transpose * J (Fin m) K)

Symplectic involutions of a matrix algebra are standard. For a skew-symmetric invertible matrix C over a field with 2 ≠ 0, a symplectic basis of the alternating form of C gives an algebra isomorphism Mₙ(K) ≃ M_{2m}(K) carrying the adjoint involution X ↦ C⁻¹ Xᵀ C to the standard symplectic adjoint X ↦ J⁻¹ Xᵀ J = -(J Xᵀ J).