# mathlib3documentation

linear_algebra.symplectic_group

# The Symplectic Group #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the symplectic group and proves elementary properties.

## Main Definitions #

matrix.J: the canonical 2n × 2n skew-symmetric matrix symplectic_group: the group of symplectic matrices

## TODO #

• Every symplectic matrix has determinant 1.
• For n = 1 the symplectic group coincides with the special linear group.
def matrix.J (l : Type u_1) (R : Type u_2) [decidable_eq l] [comm_ring R] :
matrix (l l) (l l) R

The matrix defining the canonical skew-symmetric bilinear form.

Equations
• R = (-1) 1 0
@[simp]
theorem matrix.J_transpose (l : Type u_1) (R : Type u_2) [decidable_eq l] [comm_ring R] :
theorem matrix.J_squared (l : Type u_1) (R : Type u_2) [decidable_eq l] [comm_ring R] [fintype l] :
(matrix.J l R).mul (matrix.J l R) = -1
theorem matrix.J_inv (l : Type u_1) (R : Type u_2) [decidable_eq l] [comm_ring R] [fintype l] :
(matrix.J l R)⁻¹ = - R
theorem matrix.J_det_mul_J_det (l : Type u_1) (R : Type u_2) [decidable_eq l] [comm_ring R] [fintype l] :
(matrix.J l R).det * (matrix.J l R).det = 1
theorem matrix.is_unit_det_J (l : Type u_1) (R : Type u_2) [decidable_eq l] [comm_ring R] [fintype l] :
def matrix.symplectic_group (l : Type u_1) (R : Type u_2) [decidable_eq l] [comm_ring R] [fintype l] :
submonoid (matrix (l l) (l l) R)

The group of symplectic matrices over a ring R.

Equations
Instances for ↥matrix.symplectic_group
theorem symplectic_group.mem_iff {l : Type u_1} {R : Type u_2} [decidable_eq l] [fintype l] [comm_ring R] {A : matrix (l l) (l l) R} :
(A.mul (matrix.J l R)).mul A.transpose = R
@[protected, instance]
def symplectic_group.coe_matrix {l : Type u_1} {R : Type u_2} [decidable_eq l] [fintype l] [comm_ring R] :
(matrix (l l) (l l) R)
Equations
theorem symplectic_group.J_mem (l : Type u_1) (R : Type u_2) [decidable_eq l] [fintype l] [comm_ring R] :
R
def symplectic_group.sym_J (l : Type u_1) (R : Type u_2) [decidable_eq l] [fintype l] [comm_ring R] :

The canonical skew-symmetric matrix as an element in the symplectic group.

Equations
• = R _inst_3, _⟩
@[simp]
theorem symplectic_group.coe_J {l : Type u_1} {R : Type u_2} [decidable_eq l] [fintype l] [comm_ring R] :
= R
theorem symplectic_group.neg_mem {l : Type u_1} {R : Type u_2} [decidable_eq l] [fintype l] [comm_ring R] {A : matrix (l l) (l l) R} (h : A ) :
theorem symplectic_group.symplectic_det {l : Type u_1} {R : Type u_2} [decidable_eq l] [fintype l] [comm_ring R] {A : matrix (l l) (l l) R} (hA : A ) :
theorem symplectic_group.transpose_mem {l : Type u_1} {R : Type u_2} [decidable_eq l] [fintype l] [comm_ring R] {A : matrix (l l) (l l) R} (hA : A ) :
@[simp]
theorem symplectic_group.transpose_mem_iff {l : Type u_1} {R : Type u_2} [decidable_eq l] [fintype l] [comm_ring R] {A : matrix (l l) (l l) R} :
theorem symplectic_group.mem_iff' {l : Type u_1} {R : Type u_2} [decidable_eq l] [fintype l] [comm_ring R] {A : matrix (l l) (l l) R} :
(A.transpose.mul (matrix.J l R)).mul A = R
@[protected, instance]
Equations
theorem symplectic_group.coe_inv {l : Type u_1} {R : Type u_2} [decidable_eq l] [fintype l] [comm_ring R] (A : ) :
theorem symplectic_group.inv_left_mul_aux {l : Type u_1} {R : Type u_2} [decidable_eq l] [fintype l] [comm_ring R] {A : matrix (l l) (l l) R} (hA : A ) :
-(((matrix.J l R).mul A.transpose).mul (matrix.J l R)).mul A = 1
theorem symplectic_group.coe_inv' {l : Type u_1} {R : Type u_2} [decidable_eq l] [fintype l] [comm_ring R] (A : ) :
theorem symplectic_group.inv_eq_symplectic_inv {l : Type u_1} {R : Type u_2} [decidable_eq l] [fintype l] [comm_ring R] (A : matrix (l l) (l l) R) (hA : A ) :
A⁻¹ = ((- R).mul A.transpose).mul (matrix.J l R)
@[protected, instance]
Equations