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.transpose (Matrix.J l R) = -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.det (Matrix.J l R) * Matrix.det (Matrix.J l R) = 1

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

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

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

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 * Matrix.transpose A = 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 = { val := Matrix.J l R, property := (_ : Matrix.J l R ∈ Matrix.symplecticGroup 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 (Matrix.det A)

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) : Matrix.transpose A ∈ 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} : Matrix.transpose A ∈ 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 ↔ Matrix.transpose A * 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

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

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 * Matrix.transpose ↑A * 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 * Matrix.transpose A * 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 * Matrix.transpose A * Matrix.J l R

instance SymplecticGroup.instGroupSubtypeMatrixSumMemSubmonoidToMulOneClassToMulZeroOneClassNonAssocSemiringToNonAssocSemiringToSemiringToCommSemiringInstFintypeSumInstDecidableEqSumInstMembershipInstSetLikeSubmonoidSymplecticGroup {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.