Membership in the symplectic Lie algebra

The symplectic Lie algebra LieAlgebra.Symplectic.sp l R is cut out by a condition relating a matrix to its transpose through the canonical skew-symmetric matrix Matrix.J l R. This file spells that condition out as Aᵀ * J = -(J * A), the symplectic counterpart of Mathlib's LieAlgebra.Orthogonal.mem_so, and rewrites it as a conjugation by J, Aᵀ = J * (-A) * J⁻¹, which is the form the matrix exponential consumes.

Since J * J = -1, all of this is available over an arbitrary commutative ring with no invertibility side conditions; Matrix.eq_J_conj_iff_mul_J_eq is the cancellation that moves a matrix past J.

Main results

• LieAlgebra.Symplectic.mem_sp: membership in the symplectic Lie algebra, spelled out as Aᵀ * J = -(J * A).
• LieAlgebra.Symplectic.mem_sp_iff_transpose_eq_J_conj_neg: the same condition as a conjugation, Aᵀ = J * (-A) * J⁻¹.
• LieAlgebra.Symplectic.mul_J_add_J_mul_transpose_eq_zero: the additive form A * J + J * Aᵀ = 0.
• Matrix.mem_symplecticLieAlgebra_iff: the entrywise block criterion, with symmetric off-diagonal blocks and opposite transposed diagonal blocks.

@[simp]

theorem LieAlgebra.Symplectic.mem_sp {l : Type u_1} [DecidableEq l] [Fintype l] {R : Type u_2} [CommRing R] (A : Matrix (l ⊕ l) (l ⊕ l) R) : A ∈ sp l R ↔ A.transpose * Matrix.J l R = -(Matrix.J l R * A)

Membership in the symplectic Lie algebra: A is skew-adjoint for the canonical skew-symmetric form exactly when Aᵀ * J = -(J * A). The symplectic counterpart of Mathlib's LieAlgebra.Orthogonal.mem_so, whose J = 1 makes the two multiplications disappear.

theorem LieAlgebra.Symplectic.mem_sp_iff_transpose_eq_J_conj_neg {l : Type u_1} [DecidableEq l] [Fintype l] {R : Type u_2} [CommRing R] (A : Matrix (l ⊕ l) (l ⊕ l) R) : A ∈ sp l R ↔ A.transpose = Matrix.J l R * -A * (Matrix.J l R)⁻¹

Membership in the symplectic Lie algebra, as a conjugation: Aᵀ = J * (-A) * J⁻¹. This is the shape NormedSpace.exp transports, by Matrix.exp_conj.

theorem LieAlgebra.Symplectic.mul_J_add_J_mul_transpose_eq_zero {l : Type u_1} [DecidableEq l] [Fintype l] {R : Type u_2} [CommRing R] {A : Matrix (l ⊕ l) (l ⊕ l) R} (hA : A ∈ sp l R) : A * Matrix.J l R + Matrix.J l R * A.transpose = 0

Membership in the symplectic Lie algebra, in additive form: A * J + J * Aᵀ = 0. This is the shape a congruence computation X ↦ X * J * Xᵀ differentiates to.

theorem LieAlgebra.Symplectic.mem_sp_iff_mul_J_add_J_mul_transpose_eq_zero {l : Type u_1} [DecidableEq l] [Fintype l] {R : Type u_2} [CommRing R] (A : Matrix (l ⊕ l) (l ⊕ l) R) : A ∈ sp l R ↔ A * Matrix.J l R + Matrix.J l R * A.transpose = 0

Membership in the symplectic Lie algebra is equivalent to the linearized symplectic-group equation, also in characteristic two.

theorem Matrix.mem_symplecticLieAlgebra_iff {l : Type u_1} [DecidableEq l] [Fintype l] {R : Type u_2} [CommRing R] (A : Matrix (l ⊕ l) (l ⊕ l) R) : A ∈ LieAlgebra.Symplectic.sp l R ↔ (∀ (i j : l), A (Sum.inl i) (Sum.inr j) = A (Sum.inl j) (Sum.inr i)) ∧ (∀ (i j : l), A (Sum.inr i) (Sum.inl j) = A (Sum.inr j) (Sum.inl i)) ∧ ∀ (i j : l), A (Sum.inr i) (Sum.inr j) = -A (Sum.inl j) (Sum.inl i)

A symplectic Lie matrix has symmetric off-diagonal blocks and diagonal blocks which are negatives of each other's transposes. This criterion includes characteristic two.