The Symplectic Group #

This file defines the symplectic group and proves elementary properties.

Main Definitions #

• Matrix.J: the canonical 2n × 2n skew-symmetric matrix
• symplecticGroup: 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) [] [] :
Matrix (l l) (l l) R

The matrix defining the canonical skew-symmetric bilinear form.

Equations
Instances For
@[simp]
theorem Matrix.J_transpose (l : Type u_1) (R : Type u_2) [] [] :
theorem Matrix.J_squared (l : Type u_1) (R : Type u_2) [] [] [] :
Matrix.J l R * Matrix.J l R = -1
theorem Matrix.J_inv (l : Type u_1) (R : Type u_2) [] [] [] :
theorem Matrix.J_det_mul_J_det (l : Type u_1) (R : Type u_2) [] [] [] :
theorem Matrix.isUnit_det_J (l : Type u_1) (R : Type u_2) [] [] [] :
def Matrix.symplecticGroup (l : Type u_1) (R : Type u_2) [] [] [] :
Submonoid (Matrix (l l) (l l) R)

The group of symplectic matrices over a ring R.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem SymplecticGroup.mem_iff {l : Type u_1} {R : Type u_2} [] [] [] {A : Matrix (l l) (l l) R} :
A * Matrix.J l R * = Matrix.J l R
instance SymplecticGroup.coeMatrix {l : Type u_1} {R : Type u_2} [] [] [] :
Coe (()) (Matrix (l l) (l l) R)
Equations
• SymplecticGroup.coeMatrix = { coe := Subtype.val }
theorem SymplecticGroup.J_mem (l : Type u_1) (R : Type u_2) [] [] [] :
def SymplecticGroup.symJ (l : Type u_1) (R : Type u_2) [] [] [] :
()

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

Equations
Instances For
@[simp]
theorem SymplecticGroup.coe_J {l : Type u_1} {R : Type u_2} [] [] [] :
() = Matrix.J l R
theorem SymplecticGroup.neg_mem {l : Type u_1} {R : Type u_2} [] [] [] {A : Matrix (l l) (l l) R} (h : ) :
theorem SymplecticGroup.symplectic_det {l : Type u_1} {R : Type u_2} [] [] [] {A : Matrix (l l) (l l) R} (hA : ) :
theorem SymplecticGroup.transpose_mem {l : Type u_1} {R : Type u_2} [] [] [] {A : Matrix (l l) (l l) R} (hA : ) :
@[simp]
theorem SymplecticGroup.transpose_mem_iff {l : Type u_1} {R : Type u_2} [] [] [] {A : Matrix (l l) (l l) R} :
theorem SymplecticGroup.mem_iff' {l : Type u_1} {R : Type u_2} [] [] [] {A : Matrix (l l) (l l) R} :
* A = Matrix.J l R
instance SymplecticGroup.hasInv {l : Type u_1} {R : Type u_2} [] [] [] :
Inv ()
Equations
• One or more equations did not get rendered due to their size.
theorem SymplecticGroup.coe_inv {l : Type u_1} {R : Type u_2} [] [] [] (A : ()) :
A⁻¹ = -Matrix.J l R * * Matrix.J l R
theorem SymplecticGroup.inv_left_mul_aux {l : Type u_1} {R : Type u_2} [] [] [] {A : Matrix (l l) (l l) R} (hA : ) :
-( * Matrix.J l R * A) = 1
theorem SymplecticGroup.coe_inv' {l : Type u_1} {R : Type u_2} [] [] [] (A : ()) :
A⁻¹ = (A)⁻¹
theorem SymplecticGroup.inv_eq_symplectic_inv {l : Type u_1} {R : Type u_2} [] [] [] (A : Matrix (l l) (l l) R) (hA : ) :
Equations
• One or more equations did not get rendered due to their size.