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 #

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
@[simp]
theorem matrix.J_transpose (l : Type u_1) (R : Type u_2) [decidable_eq l] [comm_ring R] :
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
theorem matrix.J_inv (l : Type u_1) (R : Type u_2) [decidable_eq l] [comm_ring R] [fintype l] :
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
theorem matrix.is_unit_det_J (l : Type u_1) (R : Type u_2) [decidable_eq l] [comm_ring R] [fintype l] :
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
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} :
@[protected, instance]
def symplectic_group.coe_matrix {l : Type u_1} {R : Type u_2} [decidable_eq l] [fintype l] [comm_ring R] :
Equations

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

Equations
@[simp]
theorem symplectic_group.coe_J {l : Type u_1} {R : Type u_2} [decidable_eq l] [fintype l] [comm_ring R] :
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) :
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) :
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) :
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} :
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
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) :
@[protected, instance]
Equations