Documentation

Mathlib.LinearAlgebra.SymplecticGroup

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.

Instances For

@[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.

Instances For

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 { x // x ∈ Matrix.symplecticGroup l R } (Matrix (l ⊕ l) (l ⊕ l) R)

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] :

{ x // x ∈ Matrix.symplecticGroup l R }

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

Instances For

@[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 { x // x ∈ Matrix.symplecticGroup l R }

theorem SymplecticGroup.coe_inv {l : Type u_1} {R : Type u_2} [DecidableEq l] [Fintype l] [CommRing R] (A : { x // x ∈ 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 : { x // x ∈ 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 { x // x ∈ Matrix.symplecticGroup l R }