The standard representation of the symplectic group

This file restricts the standard representation of the general linear group to the symplectic group. It defines the standard alternating form from Matrix.J, proves that the standard action preserves it, and packages the resulting equivariant self-duality.

Main definitions

• TauCeti.symplecticGroupToGL is the canonical inclusion into the general linear group.
• TauCeti.stdSymplecticRep is the standard representation of Matrix.symplecticGroup.
• TauCeti.stdSymplecticBilinForm is the nondegenerate invariant alternating form.
• TauCeti.stdSymplecticRepEquivDual is the induced equivariant self-duality.

References

• Classical groups roadmap, Layer 0.
• The equivariance, self-duality, and character constructions follow the formal template in TauCeti.RepresentationTheory.ClassicalGroups.Orthogonal.

def TauCeti.symplecticGroupToGL (k : Type u) (n : ℕ) [CommRing k] : ↥(Matrix.symplecticGroup (Fin n) k) →* GL (Fin n ⊕ Fin n) k

The canonical inclusion of the symplectic group into the general linear group.

Equations

• TauCeti.symplecticGroupToGL k n = { toFun := fun (g : ↥(Matrix.symplecticGroup (Fin n) k)) => Matrix.SpecialLinearGroup.toGL ⟨↑g, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.symplecticGroupToGL_coe (k : Type u) (n : ℕ) [CommRing k] (g : ↥(Matrix.symplecticGroup (Fin n) k)) : ↑((symplecticGroupToGL k n) g) = ↑g

The symplectic-to-general-linear inclusion has the original matrix as underlying matrix.

theorem TauCeti.symplecticGroupToGL_injective (k : Type u) (n : ℕ) [CommRing k] : Function.Injective ⇑(symplecticGroupToGL k n)

The canonical inclusion of the symplectic group into the general linear group is injective.

def TauCeti.stdSymplecticRep (k : Type u) (n : ℕ) [CommRing k] : Representation k (↥(Matrix.symplecticGroup (Fin n) k)) (Fin n ⊕ Fin n → k)

The standard representation of the symplectic group on column vectors.

Equations

• TauCeti.stdSymplecticRep k n = (Units.coeHom ((Fin n ⊕ Fin n → k) →ₗ[k] Fin n ⊕ Fin n → k)).comp (Matrix.GeneralLinearGroup.toLin.toMonoidHom.comp (TauCeti.symplecticGroupToGL k n))

@[simp]

theorem TauCeti.stdSymplecticRep_apply (k : Type u) (n : ℕ) [CommRing k] (g : ↥(Matrix.symplecticGroup (Fin n) k)) : (stdSymplecticRep k n) g = (↑g).mulVecLin

The standard symplectic action is multiplication by the underlying matrix.

theorem TauCeti.stdSymplecticRep_apply_apply (k : Type u) (n : ℕ) [CommRing k] (g : ↥(Matrix.symplecticGroup (Fin n) k)) (v : Fin n ⊕ Fin n → k) : ((stdSymplecticRep k n) g) v = (↑g).mulVec v

Evaluation of the standard symplectic action is matrix-vector multiplication.

theorem TauCeti.stdSymplecticRep_injective (k : Type u) (n : ℕ) [CommRing k] : Function.Injective ⇑(stdSymplecticRep k n)

The standard representation of the symplectic group is faithful.

@[reducible, inline]

noncomputable abbrev TauCeti.stdSymplecticFDRep (k : Type u) (n : ℕ) [CommRing k] : FDRep k ↥(Matrix.symplecticGroup (Fin n) k)

The standard representation of the symplectic group, bundled as an object of FDRep.

Equations

• TauCeti.stdSymplecticFDRep k n = FDRep.of (TauCeti.stdSymplecticRep k n)

def TauCeti.stdSymplecticBilinForm (k : Type u) (n : ℕ) [CommRing k] : LinearMap.BilinForm k (Fin n ⊕ Fin n → k)

The standard alternating bilinear form represented by Matrix.J.

Equations

• TauCeti.stdSymplecticBilinForm k n = Matrix.toBilin' (Matrix.J (Fin n) k)

@[simp]

theorem TauCeti.stdSymplecticBilinForm_apply (k : Type u) (n : ℕ) [CommRing k] (v w : Fin n ⊕ Fin n → k) : ((stdSymplecticBilinForm k n) v) w = v ⬝ᵥ (Matrix.J (Fin n) k).mulVec w

The standard symplectic form is vᵀ J w.

theorem TauCeti.isAlt_stdSymplecticBilinForm (k : Type u) (n : ℕ) [CommRing k] : (stdSymplecticBilinForm k n).IsAlt

The standard symplectic form is alternating.

theorem TauCeti.stdSymplecticBilinForm_nondegenerate (k : Type u) (n : ℕ) [CommRing k] : (stdSymplecticBilinForm k n).Nondegenerate

The standard symplectic form is nondegenerate.

@[simp]

theorem TauCeti.stdSymplecticBilinForm_comp_stdSymplecticRep (k : Type u) (n : ℕ) [CommRing k] (g : ↥(Matrix.symplecticGroup (Fin n) k)) : (stdSymplecticBilinForm k n).comp (↑g).mulVecLin (↑g).mulVecLin = stdSymplecticBilinForm k n

The standard symplectic action preserves the standard alternating form.

@[simp]

theorem TauCeti.stdSymplecticBilinForm_stdSymplecticRep (k : Type u) (n : ℕ) [CommRing k] (g : ↥(Matrix.symplecticGroup (Fin n) k)) (v w : Fin n ⊕ Fin n → k) : (↑g).mulVec v ⬝ᵥ (Matrix.J (Fin n) k * ↑g).mulVec w = ((stdSymplecticBilinForm k n) v) w

The standard symplectic pairing is invariant under the standard action.

noncomputable def TauCeti.stdSymplecticRepToDual (k : Type u) (n : ℕ) [CommRing k] : (Fin n ⊕ Fin n → k) ≃ₗ[k] Module.Dual k (Fin n ⊕ Fin n → k)

The standard symplectic form identifies the standard module with its dual.

Equations

• TauCeti.stdSymplecticRepToDual k n = (Matrix.toLinearEquiv (Pi.basisFun k (Fin n ⊕ Fin n)) (Matrix.J (Fin n) k).transpose ⋯).trans (Pi.basisFun k (Fin n ⊕ Fin n)).toDualEquiv

@[simp]

theorem TauCeti.stdSymplecticRepToDual_apply (k : Type u) (n : ℕ) [CommRing k] (v w : Fin n ⊕ Fin n → k) : ((stdSymplecticRepToDual k n) v) w = ((stdSymplecticBilinForm k n) v) w

The standard symplectic self-duality evaluates as the standard alternating form.

noncomputable def TauCeti.stdSymplecticDualRep (k : Type u) (n : ℕ) [CommRing k] : Representation k (↥(Matrix.symplecticGroup (Fin n) k)) (Module.Dual k (Fin n ⊕ Fin n → k))

The dual, or contragredient, of the standard representation of the symplectic group.

Equations

• TauCeti.stdSymplecticDualRep k n = (TauCeti.stdSymplecticRep k n).dual

@[simp]

theorem TauCeti.stdSymplecticDualRep_apply (k : Type u) (n : ℕ) [CommRing k] (g : ↥(Matrix.symplecticGroup (Fin n) k)) : (stdSymplecticDualRep k n) g = Module.Dual.transpose (↑g⁻¹).mulVecLin

The dual standard symplectic action is the transpose of the inverse matrix action.

theorem TauCeti.stdSymplecticRepToDual_equivariant (k : Type u) (n : ℕ) [CommRing k] (g : ↥(Matrix.symplecticGroup (Fin n) k)) : ↑(stdSymplecticRepToDual k n) ∘ₗ (stdSymplecticRep k n) g = (stdSymplecticDualRep k n) g ∘ₗ ↑(stdSymplecticRepToDual k n)

The standard-form identification intertwines the standard and dual actions.

noncomputable def TauCeti.stdSymplecticRepEquivDual (k : Type u) (n : ℕ) [CommRing k] : (stdSymplecticRep k n).Equiv (stdSymplecticDualRep k n)

The standard representation of the symplectic group is equivariantly self-dual.

Equations

• TauCeti.stdSymplecticRepEquivDual k n = Representation.Equiv.mk (TauCeti.stdSymplecticRepToDual k n) ⋯

@[simp]

theorem TauCeti.stdSymplecticRepEquivDual_apply (k : Type u) (n : ℕ) [CommRing k] (v w : Fin n ⊕ Fin n → k) : ((stdSymplecticRepEquivDual k n) v) w = ((stdSymplecticBilinForm k n) v) w

The symplectic self-duality equivalence evaluates as the standard alternating form.

@[reducible, inline]

noncomputable abbrev TauCeti.stdSymplecticDualFDRep (k : Type u) (n : ℕ) [CommRing k] : FDRep k ↥(Matrix.symplecticGroup (Fin n) k)

The dual standard symplectic representation, bundled as an object of FDRep.

Equations

• TauCeti.stdSymplecticDualFDRep k n = FDRep.of (TauCeti.stdSymplecticDualRep k n)

@[simp]

theorem TauCeti.char_stdSymplecticRep (k : Type u) (n : ℕ) [Field k] (g : ↥(Matrix.symplecticGroup (Fin n) k)) : (stdSymplecticRep k n).character g = (↑g).trace

The character of the standard symplectic representation is the matrix trace.

@[simp]

theorem TauCeti.char_stdSymplecticFDRep (k : Type u) (n : ℕ) [Field k] (g : ↥(Matrix.symplecticGroup (Fin n) k)) : (stdSymplecticFDRep k n).character g = (↑g).trace

The bundled standard symplectic character is the matrix trace.

@[simp]

theorem TauCeti.char_stdSymplecticDualRep (k : Type u) (n : ℕ) [Field k] (g : ↥(Matrix.symplecticGroup (Fin n) k)) : (stdSymplecticDualRep k n).character g = (↑g⁻¹).trace

The dual standard symplectic character is the inverse matrix trace.

@[simp]

theorem TauCeti.char_stdSymplecticDualFDRep (k : Type u) (n : ℕ) [Field k] (g : ↥(Matrix.symplecticGroup (Fin n) k)) : (stdSymplecticDualFDRep k n).character g = (↑g⁻¹).trace

The bundled dual standard symplectic character is the inverse matrix trace.