mathlib3 documentation

linear_algebra.symplectic_group

The Symplectic Group #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the symplectic group and proves elementary properties.

Main Definitions #

matrix.J: the canonical 2n × 2n skew-symmetric matrix symplectic_group: the group of symplectic matrices

TODO #

source
def matrix.J (l : Type u_1) (R : Type u_2) [decidable_eq l] [comm_ring R] :
matrix (l ⊕ l) (l ⊕ l) R

The matrix defining the canonical skew-symmetric bilinear form.

Equations
source
@[simp]
theorem matrix.J_transpose (l : Type u_1) (R : Type u_2) [decidable_eq l] [comm_ring R] :
(matrix.J l R).transpose = -matrix.J l R
source
theorem matrix.J_squared (l : Type u_1) (R : Type u_2) [decidable_eq l] [comm_ring R] [fintype l] :
(matrix.J l R).mul (matrix.J l R) = -1
source
theorem matrix.J_inv (l : Type u_1) (R : Type u_2) [decidable_eq l] [comm_ring R] [fintype l] :
(matrix.J l R)⁻¹ = -matrix.J l R
source
theorem matrix.J_det_mul_J_det (l : Type u_1) (R : Type u_2) [decidable_eq l] [comm_ring R] [fintype l] :
(matrix.J l R).det * (matrix.J l R).det = 1
source
theorem matrix.is_unit_det_J (l : Type u_1) (R : Type u_2) [decidable_eq l] [comm_ring R] [fintype l] :
is_unit (matrix.J l R).det
source
def matrix.symplectic_group (l : Type u_1) (R : Type u_2) [decidable_eq l] [comm_ring R] [fintype l] :
submonoid (matrix (l ⊕ l) (l ⊕ l) R)

The group of symplectic matrices over a ring R.

Equations
Instances for ↥matrix.symplectic_group
source
theorem symplectic_group.mem_iff {l : Type u_1} {R : Type u_2} [decidable_eq l] [fintype l] [comm_ring R] {A : matrix (l ⊕ l) (l ⊕ l) R} :
A ∈ matrix.symplectic_group l R ↔ (A.mul (matrix.J l R)).mul A.transpose = matrix.J l R
source
@[protected, instance]
def symplectic_group.coe_matrix {l : Type u_1} {R : Type u_2} [decidable_eq l] [fintype l] [comm_ring R] :
has_coe ↥(matrix.symplectic_group l R) (matrix (l ⊕ l) (l ⊕ l) R)
Equations
source
theorem symplectic_group.J_mem (l : Type u_1) (R : Type u_2) [decidable_eq l] [fintype l] [comm_ring R] :
matrix.J l R ∈ matrix.symplectic_group l R
source
def symplectic_group.sym_J (l : Type u_1) (R : Type u_2) [decidable_eq l] [fintype l] [comm_ring R] :
↥(matrix.symplectic_group l R)

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

Equations
source
@[simp]
theorem symplectic_group.coe_J {l : Type u_1} {R : Type u_2} [decidable_eq l] [fintype l] [comm_ring R] :
↑(symplectic_group.sym_J l R) = matrix.J l R
source
theorem symplectic_group.neg_mem {l : Type u_1} {R : Type u_2} [decidable_eq l] [fintype l] [comm_ring R] {A : matrix (l ⊕ l) (l ⊕ l) R} (h : A ∈ matrix.symplectic_group l R) :
-A ∈ matrix.symplectic_group l R
source
theorem symplectic_group.symplectic_det {l : Type u_1} {R : Type u_2} [decidable_eq l] [fintype l] [comm_ring R] {A : matrix (l ⊕ l) (l ⊕ l) R} (hA : A ∈ matrix.symplectic_group l R) :
is_unit A.det
source
theorem symplectic_group.transpose_mem {l : Type u_1} {R : Type u_2} [decidable_eq l] [fintype l] [comm_ring R] {A : matrix (l ⊕ l) (l ⊕ l) R} (hA : A ∈ matrix.symplectic_group l R) :
A.transpose ∈ matrix.symplectic_group l R
source
@[simp]
theorem symplectic_group.transpose_mem_iff {l : Type u_1} {R : Type u_2} [decidable_eq l] [fintype l] [comm_ring R] {A : matrix (l ⊕ l) (l ⊕ l) R} :
A.transpose ∈ matrix.symplectic_group l R ↔ A ∈ matrix.symplectic_group l R
source
theorem symplectic_group.mem_iff' {l : Type u_1} {R : Type u_2} [decidable_eq l] [fintype l] [comm_ring R] {A : matrix (l ⊕ l) (l ⊕ l) R} :
A ∈ matrix.symplectic_group l R ↔ (A.transpose.mul (matrix.J l R)).mul A = matrix.J l R
source
@[protected, instance]
def symplectic_group.matrix.symplectic_group.has_inv {l : Type u_1} {R : Type u_2} [decidable_eq l] [fintype l] [comm_ring R] :
has_inv ↥(matrix.symplectic_group l R)
Equations
source
theorem symplectic_group.coe_inv {l : Type u_1} {R : Type u_2} [decidable_eq l] [fintype l] [comm_ring R] (A : ↥(matrix.symplectic_group l R)) :
↑A⁻¹ = ((-matrix.J l R).mul ↑A.transpose).mul (matrix.J l R)
source
theorem symplectic_group.inv_left_mul_aux {l : Type u_1} {R : Type u_2} [decidable_eq l] [fintype l] [comm_ring R] {A : matrix (l ⊕ l) (l ⊕ l) R} (hA : A ∈ matrix.symplectic_group l R) :
-(((matrix.J l R).mul A.transpose).mul (matrix.J l R)).mul A = 1
source
theorem symplectic_group.coe_inv' {l : Type u_1} {R : Type u_2} [decidable_eq l] [fintype l] [comm_ring R] (A : ↥(matrix.symplectic_group l R)) :
↑A⁻¹ = (↑A)⁻¹
source
theorem symplectic_group.inv_eq_symplectic_inv {l : Type u_1} {R : Type u_2} [decidable_eq l] [fintype l] [comm_ring R] (A : matrix (l ⊕ l) (l ⊕ l) R) (hA : A ∈ matrix.symplectic_group l R) :
A⁻¹ = ((-matrix.J l R).mul A.transpose).mul (matrix.J l R)
source
@[protected, instance]
def symplectic_group.matrix.symplectic_group.group {l : Type u_1} {R : Type u_2} [decidable_eq l] [fintype l] [comm_ring R] :
group ↥(matrix.symplectic_group l R)
Equations