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

Implementation Notes

• SymplecticGroup.det_eq_one: Symplectic matrices have determinant 1. The proof strategy comes in two steps:

1. Consider a symplectic matrix M over a local ring, we can construct a matrix of the form fromBlocks 1 X 0 1 s.t. the upper-left block of (fromBlocks 1 X 0 1) * M is invertible. From this we can calculate the determinant.

2. For a symplectic matrix M over general commutative ring R, we note that by step 1, M.det - 1 = 0 in any localization at a maximal ideal in R. Therefore M.det = 1 in R.

Developing the proof in two steps is helpful, since the local ring hypothesis allows us to construct the desired X in step 1 at the residue field level, and lift back to the ring while keeping the upper-left block invertible.

TODO

• For n = 1 the symplectic group coincides with the special linear group.

def Matrix.J (l : Type u_1) (R : Type u_2) [DecidableEq l] [CommRing R] : Matrix (l ⊕ l) (l ⊕ l) R

The matrix defining the canonical skew-symmetric bilinear form.

Equations

• Matrix.J l R = Matrix.fromBlocks 0 (-1) 1 0

@[simp]

theorem Matrix.map_J (l : Type u_1) {R : Type u_2} [DecidableEq l] [CommRing R] {F : Type u_3} {S : Type u_4} [CommRing S] [FunLike F R S] [AddMonoidHomClass F R S] [OneHomClass F R S] (f : F) : (J l R).map ⇑f = J l S

@[simp]

theorem Matrix.J_transpose (l : Type u_1) (R : Type u_2) [DecidableEq l] [CommRing R] : (J l R).transpose = -J l R

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

theorem Matrix.J_inv (l : Type u_1) (R : Type u_2) [DecidableEq l] [CommRing R] [Fintype l] : (J l R)⁻¹ = -J l R

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

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

def Matrix.symplecticGroup (l : Type u_1) (R : Type u_2) [DecidableEq l] [CommRing R] [Fintype l] : Submonoid (Matrix (l ⊕ l) (l ⊕ l) R)

The group of symplectic matrices over a ring R.

Equations

• Matrix.symplecticGroup l R = { carrier := {A : Matrix (l ⊕ l) (l ⊕ l) R | A * Matrix.J l R * A.transpose = Matrix.J l R}, mul_mem' := ⋯, one_mem' := ⋯ }

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

@[implicit_reducible]

instance SymplecticGroup.coeMatrix {l : Type u_1} {R : Type u_2} [DecidableEq l] [Fintype l] [CommRing R] : Coe (↥(Matrix.symplecticGroup l R)) (Matrix (l ⊕ l) (l ⊕ l) R)

Equations

• SymplecticGroup.coeMatrix = { coe := Subtype.val }

theorem SymplecticGroup.J_mem (l : Type u_1) (R : Type u_2) [DecidableEq l] [Fintype l] [CommRing R] : Matrix.J l R ∈ Matrix.symplecticGroup l R

def SymplecticGroup.symJ (l : Type u_1) (R : Type u_2) [DecidableEq l] [Fintype l] [CommRing R] : ↥(Matrix.symplecticGroup l R)

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

Equations

• SymplecticGroup.symJ l R = ⟨Matrix.J l R, ⋯⟩

@[simp]

theorem SymplecticGroup.coe_J {l : Type u_1} {R : Type u_2} [DecidableEq l] [Fintype l] [CommRing R] : ↑(symJ l R) = Matrix.J l R

theorem SymplecticGroup.neg_mem {l : Type u_1} {R : Type u_2} [DecidableEq l] [Fintype l] [CommRing R] {A : Matrix (l ⊕ l) (l ⊕ l) R} (h : A ∈ Matrix.symplecticGroup l R) : -A ∈ Matrix.symplecticGroup l R

theorem SymplecticGroup.symplectic_det {l : Type u_1} {R : Type u_2} [DecidableEq l] [Fintype l] [CommRing R] {A : Matrix (l ⊕ l) (l ⊕ l) R} (hA : A ∈ Matrix.symplecticGroup l R) : IsUnit A.det

theorem SymplecticGroup.map_mem {l : Type u_1} {R : Type u_2} [DecidableEq l] [Fintype l] [CommRing R] {A : Matrix (l ⊕ l) (l ⊕ l) R} {F : Type u_3} {S : Type u_4} [CommRing S] [FunLike F R S] [RingHomClass F R S] (hA : A ∈ Matrix.symplecticGroup l R) (f : F) : A.map ⇑f ∈ Matrix.symplecticGroup l S

theorem SymplecticGroup.transpose_mem {l : Type u_1} {R : Type u_2} [DecidableEq l] [Fintype l] [CommRing R] {A : Matrix (l ⊕ l) (l ⊕ l) R} (hA : A ∈ Matrix.symplecticGroup l R) : A.transpose ∈ Matrix.symplecticGroup l R

@[simp]

theorem SymplecticGroup.transpose_mem_iff {l : Type u_1} {R : Type u_2} [DecidableEq l] [Fintype l] [CommRing R] {A : Matrix (l ⊕ l) (l ⊕ l) R} : A.transpose ∈ Matrix.symplecticGroup l R ↔ A ∈ Matrix.symplecticGroup l R

theorem SymplecticGroup.mem_iff' {l : Type u_1} {R : Type u_2} [DecidableEq l] [Fintype l] [CommRing R] {A : Matrix (l ⊕ l) (l ⊕ l) R} : A ∈ Matrix.symplecticGroup l R ↔ A.transpose * Matrix.J l R * A = Matrix.J l R

@[implicit_reducible]

instance SymplecticGroup.hasInv {l : Type u_1} {R : Type u_2} [DecidableEq l] [Fintype l] [CommRing R] : Inv ↥(Matrix.symplecticGroup l R)

Equations

• SymplecticGroup.hasInv = { inv := fun (A : ↥(Matrix.symplecticGroup l R)) => ⟨-Matrix.J l R * (↑A).transpose * Matrix.J l R, ⋯⟩ }

theorem SymplecticGroup.coe_inv {l : Type u_1} {R : Type u_2} [DecidableEq l] [Fintype l] [CommRing R] (A : ↥(Matrix.symplecticGroup l R)) : ↑A⁻¹ = -Matrix.J l R * (↑A).transpose * Matrix.J l R

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

theorem SymplecticGroup.coe_inv' {l : Type u_1} {R : Type u_2} [DecidableEq l] [Fintype l] [CommRing R] (A : ↥(Matrix.symplecticGroup l R)) : ↑A⁻¹ = (↑A)⁻¹

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

@[implicit_reducible]

instance SymplecticGroup.instGroupSubtypeMatrixSumMemSubmonoidSymplecticGroup {l : Type u_1} {R : Type u_2} [DecidableEq l] [Fintype l] [CommRing R] : Group ↥(Matrix.symplecticGroup l R)

Equations

• One or more equations did not get rendered due to their size.

theorem SymplecticGroup.fromBlocks_mem_iff {l : Type u_1} {R : Type u_2} [DecidableEq l] [Fintype l] [CommRing R] {A B C D : Matrix l l R} : Matrix.fromBlocks A B C D ∈ Matrix.symplecticGroup l R ↔ A.transpose * C = C.transpose * A ∧ B.transpose * D = D.transpose * B ∧ A.transpose * D - C.transpose * B = 1

theorem SymplecticGroup.det_eq_one {l : Type u_1} {R : Type u_2} [DecidableEq l] [Fintype l] [CommRing R] {M : Matrix (l ⊕ l) (l ⊕ l) R} (hM : M ∈ Matrix.symplecticGroup l R) : M.det = 1

Symplectic matrices have determinant 1.

The proof strategy comes in two steps:

1. Consider a symplectic matrix M over a local ring, we can construct a matrix of the form fromBlocks 1 X 0 1 s.t. the upper-left block of (fromBlocks 1 X 0 1) * M is invertible. From this we can calculate the determinant.

2. For a symplectic matrix M over general commutative ring R, we note that by step 1, M.det - 1 = 0 in any localization at a maximal ideal in R. Therefore M.det = 1 in R.