The canonical skew-symmetric matrix as a unit, and block matrices in the symplectic group

Mathlib's Matrix.J satisfies J * J = -1, so it is a unit with inverse -J. This file records that unit and the conjugation cancellation it supports — X = J * Y * J⁻¹ iff X * J = J * Y — and solves the symplectic inverse formula SymplecticGroup.inv_eq_symplectic_inv for the transpose, Aᵀ = J * A⁻¹ * J⁻¹. Conjugation by J is the shape the matrix exponential consumes: the exponential does not interact with Aᵀ * J = J * (-A), but it does turn Aᵀ = J * (-A) * J⁻¹ into (exp A)ᵀ = J * (exp A)⁻¹ * J⁻¹.

It also records membership in Matrix.symplecticGroup of three families of block matrices, each a specialisation of SymplecticGroup.fromBlocks_mem_iff.

Main results

• Matrix.J_mul_neg_J, Matrix.neg_J_mul_J and Matrix.isUnit_J: the canonical skew-symmetric matrix is a unit, with inverse -J.
• Matrix.eq_J_conj_iff_mul_J_eq: cancelling a conjugation by J.
• SymplecticGroup.transpose_eq_J_conj_inv: the transpose of a symplectic matrix is the J-conjugate of its inverse.
• SymplecticGroup.fromBlocks_upper_mem: fromBlocks 1 B 0 1 for symmetric B;
• SymplecticGroup.fromBlocks_lower_mem: fromBlocks 1 0 C 1 for symmetric C;
• SymplecticGroup.fromBlocks_diagonal_mem: fromBlocks A 0 0 D when Aᵀ * D = 1.

theorem Matrix.J_mul_neg_J (l : Type u_1) [DecidableEq l] [Fintype l] (R : Type u_2) [CommRing R] : J l R * -J l R = 1

J * (-J) = 1: the companion of Matrix.J_squared in the form the conjugation arguments below use.

theorem Matrix.neg_J_mul_J (l : Type u_1) [DecidableEq l] [Fintype l] (R : Type u_2) [CommRing R] : -J l R * J l R = 1

(-J) * J = 1, the other one-sided inverse identity for Matrix.J.

theorem Matrix.isUnit_J (l : Type u_1) [DecidableEq l] [Fintype l] (R : Type u_2) [CommRing R] : IsUnit (J l R)

The canonical skew-symmetric matrix is a unit, with inverse -J, because J * J = -1.

theorem Matrix.eq_J_conj_iff_mul_J_eq {l : Type u_1} [DecidableEq l] [Fintype l] {R : Type u_2} [CommRing R] (X Y : Matrix (l ⊕ l) (l ⊕ l) R) : X = J l R * Y * (J l R)⁻¹ ↔ X * J l R = J l R * Y

Cancelling a conjugation by J: since J is a unit, X is the J-conjugate of Y exactly when X * J = J * Y. This is Mathlib's Matrix.mul_inv_eq_iff_eq_mul_of_invertible with the invertibility of J supplied; every identity below that moves a matrix past J is an instance of it.

theorem SymplecticGroup.transpose_eq_J_conj_inv {l : Type u_1} [DecidableEq l] [Fintype l] {R : Type u_2} [CommRing R] {A : Matrix (l ⊕ l) (l ⊕ l) R} (hA : A ∈ Matrix.symplecticGroup l R) : A.transpose = Matrix.J l R * A⁻¹ * (Matrix.J l R)⁻¹

The transpose of a symplectic matrix is the J-conjugate of its inverse. Mathlib's SymplecticGroup.inv_eq_symplectic_inv computes the inverse as -J * Aᵀ * J; cancelling the conjugation by J solves that identity for Aᵀ instead.

theorem SymplecticGroup.fromBlocks_upper_mem {l : Type u_1} [DecidableEq l] [Fintype l] {R : Type u_2} [CommRing R] {B : Matrix l l R} (hB : B.transpose = B) : Matrix.fromBlocks 1 B 0 1 ∈ Matrix.symplecticGroup l R

An upper unitriangular block matrix is symplectic when its upper-right block is symmetric.

theorem SymplecticGroup.fromBlocks_lower_mem {l : Type u_1} [DecidableEq l] [Fintype l] {R : Type u_2} [CommRing R] {C : Matrix l l R} (hC : C.transpose = C) : Matrix.fromBlocks 1 0 C 1 ∈ Matrix.symplecticGroup l R

A lower unitriangular block matrix is symplectic when its lower-left block is symmetric.

theorem SymplecticGroup.fromBlocks_diagonal_mem {l : Type u_1} [DecidableEq l] [Fintype l] {R : Type u_2} [CommRing R] {A D : Matrix l l R} (hAD : A.transpose * D = 1) : Matrix.fromBlocks A 0 0 D ∈ Matrix.symplecticGroup l R

A block-diagonal matrix is symplectic when its diagonal blocks satisfy the defining inverse transpose relation.