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.

Equations
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.

    Equations
    • One or more equations did not get rendered due to their size.
    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 ((Matrix.symplecticGroup l R)) (Matrix (l l) (l l) R)
      Equations
      • SymplecticGroup.coeMatrix = { coe := Subtype.val }
      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.

      Equations
      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] :
        Equations
        theorem SymplecticGroup.coe_inv {l : Type u_1} {R : Type u_2} [DecidableEq l] [Fintype l] [CommRing R] (A : (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 : (Matrix.symplecticGroup l R)) :
        A⁻¹ = (A)⁻¹