Documentation

Mathlib.LinearAlgebra.SymplecticGroup

The Symplectic Group #

This file defines the symplectic group and proves elementary properties.

Main Definitions #

TODO #

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] :
    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] :
    theorem Matrix.isUnit_det_J (l : Type u_1) (R : Type u_2) [DecidableEq l] [CommRing R] [Fintype l] :
    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} :
      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)
      def SymplecticGroup.symJ (l : Type u_1) (R : Type u_2) [DecidableEq l] [Fintype l] [CommRing 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] :
        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) :
        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) :
        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} :
        instance SymplecticGroup.hasInv {l : Type u_1} {R : Type u_2} [DecidableEq l] [Fintype l] [CommRing 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 }) :
        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) :
        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)⁻¹