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) [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.J_transpose (l : Type u_1) (R : Type u_2) [DecidableEq l] [CommRing R] : (Matrix.J l R).transpose = -Matrix.J l R

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

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

theorem Matrix.J_det_mul_J_det (l : Type u_1) (R : Type u_2) [DecidableEq l] [CommRing R] [Fintype l] : (Matrix.J l R).det * (Matrix.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 (Matrix.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

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] : ↑(SymplecticGroup.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.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

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

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

Equations

• SymplecticGroup.instGroupSubtypeMatrixSumMemSubmonoidSymplecticGroup = let __src := SymplecticGroup.hasInv; let __src_1 := (Matrix.symplecticGroup l R).toMonoid; Group.mk ⋯