Theorems · Theorem · group theory

SymplecticGroup.det_eq_one

∀ {l : Type u_1} {R : Type u_2} [inst : DecidableEq l] [inst_1 : Fintype l] [inst_2 : CommRing R]
  {M : Matrix (l ⊕ l) (l ⊕ l) R}, M ∈ Matrix.symplecticGroup l R → M.det = 1

Symplectic matrices have determinant 1. The proof strategy comes in two steps: 1. Consider a symplectic matrix M over a local ring, we can construct a matrix of the form fromBlocks 1 X 0 1 s.t. the upper-left block of (fromBlocks 1 X 0 1) * M is invertible. From this we can calculate the determinant. 2. For a symplectic matrix M over general commutative ring R, we note that by step 1, M.det - 1 = 0 in any localization at a maximal ideal in R. Therefore M.det = 1 in R.

Defined in

Mathlib.LinearAlgebra.SymplecticGroup

Cited by

0 results in Mathlib

Foundations

Depth 126 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqFintypeCommRing