The standard representation of the symplectic group

The standard representation of the symplectic group scheme Sp₂ₘ is obtained by corestricting the standard O(GL₂ₘ)-comodule along the quotient coordinate morphism

O(GL₂ₘ) ⟶ O(Sp₂ₘ).

The representation is faithful in every rank. Over a field it is simple whenever m is positive. Its functor-of-points action is multiplication by the corresponding symplectic matrix, so every subcomodule is stable under symplectic matrices.

Main declarations

• TauCeti.Symplectic.standardComodule: the standard O(Sp₂ₘ)-comodule on R^(2m).
• TauCeti.Symplectic.isFaithful_standardComodule: the standard comodule is faithful.
• TauCeti.Symplectic.mulVec_mem: a standard subcomodule is stable under every symplectic matrix.
• TauCeti.Symplectic.instIsSimpleOrderSubcomodule: over a field and in positive rank, the standard comodule is simple.

References

• J. S. Milne, Algebraic Groups (2017), §§2.3 and 24.6.
• J. C. Jantzen, Representations of Algebraic Groups, I.2.
• TauCeti.Algebra.AlgebraicGroup.SpecialLinear.StandardComodule, for the parallel corestriction, faithfulness, point-action, and subcomodule-stability arguments.

@[instance_reducible]

noncomputable def TauCeti.Symplectic.standardComodule (R : Type u) [CommRing R] (m : ℕ) : Comodule R (↑(coordinateHopfAlgebra R m)) (Fin (m + m) → R)

The standard right comodule of the symplectic coordinate Hopf algebra, obtained by corestricting the standard GL₂ₘ-comodule along the symplectic quotient map.

Equations

• TauCeti.Symplectic.standardComodule R m = TauCeti.Comodule.Corestrict (CommHopfAlgCat.Hom.hom (TauCeti.Symplectic.coordinateMap R m)).toCoalgHom

@[simp]

theorem TauCeti.Symplectic.standardComodule_coact (R : Type u) [CommRing R] (m : ℕ) : have x := GeneralLinear.standardComodule R (m + m); Comodule.corestrictCoact (CommHopfAlgCat.Hom.hom (coordinateMap R m)).toCoalgHom = TensorProduct.map LinearMap.id (Bialgebra.Quotient.mkBialgHom (definingHopfIdeal R m).toIdeal).toLinearMap ∘ₗ GeneralLinear.standardCoact R (m + m)

The standard symplectic coaction is the standard general-linear coaction followed by the quotient map on the coordinate factor.

theorem TauCeti.Symplectic.isFaithful_standardComodule (R : Type u) [CommRing R] (m : ℕ) : Comodule.IsFaithful

The standard comodule of Sp₂ₘ is faithful.

theorem TauCeti.Symplectic.piScalarRight_comp_endOfPoint (R : Type u) [CommRing R] (m : ℕ) {A : Type u_1} [CommRing A] [Algebra R A] (g : WithConv (↑(coordinateHopfAlgebra R m) →ₐ[R] A)) : ↑(TensorProduct.piScalarRight R A A (Fin (m + m))) ∘ₗ Comodule.endOfPoint (Fin (m + m) → R) g.ofConv = ↑(Matrix.GeneralLinearGroup.toLin ↑((pointsMulEquiv R m) g)) ∘ₗ ↑(TensorProduct.piScalarRight R A A (Fin (m + m)))

Under the canonical scalar-extension identification A ⊗[R] R^(2m) ≃ A^(2m), a point of Sp₂ₘ acts on the standard comodule by multiplication with its symplectic matrix.

theorem TauCeti.Symplectic.mulVec_mem (R : Type u) [CommRing R] (m : ℕ) (N : Subcomodule R (↑(coordinateHopfAlgebra R m)) (Fin (m + m) → R)) (g : ↥(GLSymplecticFin m R)) {w : Fin (m + m) → R} (hw : w ∈ N) : (↑↑g).mulVec w ∈ N

A subcomodule of the standard symplectic comodule is stable under every symplectic matrix.

instance TauCeti.Symplectic.instIsSimpleOrderSubcomodule (k : Type u) [Field k] (m : ℕ) [NeZero m] : IsSimpleOrder (Subcomodule k (↑(coordinateHopfAlgebra k m)) (Fin (m + m) → k))

The standard comodule of Sp₂ₘ over a field is simple when m is positive.