The tangent Lie algebra of the symplectic group scheme

The closed immersion Sp₂ₘ → GL₂ₘ identifies counit-valued tangent derivations with matrices satisfying X J + J Xᵀ = 0. Reindexing these matrices in Fin m ⊕ Fin m coordinates identifies the convolution Lie bracket with the commutator bracket in Mathlib's LieAlgebra.Symplectic.sp.

The equivalence works over every commutative base ring and every commutative coefficient algebra. In particular it includes characteristic two, nilpotents, and rank zero. It supplies matrix coordinates for root-subgroup differentials and adjoint root spaces of the symplectic group.

The construction follows SpecialLinear.tangentLieEquivSl, using ConstantForm.mem_lieSubalgebra_definingHopfIdeal_iff and the existing GeneralLinear.tangentLieEquivMatrix and HopfIdeal.quotientLieEquiv.

References

• J. S. Milne, Algebraic Groups (2017), §§10.a and 24.6.

theorem TauCeti.Symplectic.mem_lieSubalgebra_definingHopfIdeal_iff {R : Type u} [CommRing R] {B : Type v} [CommRing B] [Algebra R B] (m : ℕ) (d : Derivation R (↑(GeneralLinear.coordinateHopfAlgebra R (m + m))) (Bialgebra.CounitAlgebra R (↑(GeneralLinear.coordinateHopfAlgebra R (m + m))) B)) : d ∈ (definingHopfIdeal R m).lieSubalgebra ↔ ((GeneralLinear.tangentMatrix (m + m)) d).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv ∈ LieAlgebra.Symplectic.sp (Fin m) B

An ambient tangent derivation lies in the symplectic subgroup's Lie algebra exactly when its matrix, in paired coordinates, lies in the classical symplectic Lie algebra.

noncomputable def TauCeti.Symplectic.tangentMatrix {R : Type u} [CommRing R] {B : Type v} [CommRing B] [Algebra R B] (m : ℕ) : Derivation R (↑(coordinateHopfAlgebra R m)) (Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R m)) B) →ₗ[B] ↥(LieAlgebra.Symplectic.sp (Fin m) B)

The symplectic tangent matrix, written in paired coordinates and restricted to the classical symplectic Lie algebra.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Symplectic.tangentMatrix_apply_coe {R : Type u} [CommRing R] {B : Type v} [CommRing B] [Algebra R B] (m : ℕ) (d : Derivation R (↑(coordinateHopfAlgebra R m)) (Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R m)) B)) : ↑((tangentMatrix m) d) = ((GeneralLinear.tangentMatrix (m + m)) ((definingHopfIdeal R m).quotientLieHom d)).submatrix ⇑finSumFinEquiv ⇑finSumFinEquiv

Forgetting the symplectic condition recovers the ambient tangent matrix, reindexed along the canonical equivalence between paired and unpaired coordinates.

@[simp]

theorem TauCeti.Symplectic.tangentMatrix_lie {R : Type u} [CommRing R] {B : Type v} [CommRing B] [Algebra R B] (m : ℕ) (d e : Derivation R (↑(coordinateHopfAlgebra R m)) (Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R m)) B)) : (tangentMatrix m) ⁅d, e⁆ = ⁅(tangentMatrix m) d, (tangentMatrix m) e⁆

The symplectic tangent-matrix map preserves the convolution Lie bracket.

noncomputable def TauCeti.Symplectic.tangentLieEquivSp {R : Type u} [CommRing R] {B : Type v} [CommRing B] [Algebra R B] (m : ℕ) : Derivation R (↑(coordinateHopfAlgebra R m)) (Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R m)) B) ≃ₗ⁅B⁆ ↥(LieAlgebra.Symplectic.sp (Fin m) B)

The tangent Lie algebra of Sp₂ₘ is the classical symplectic Lie algebra, over any commutative coefficient algebra, including in characteristic two.

Equations

• TauCeti.Symplectic.tangentLieEquivSp m = LieEquiv.ofBijective (let __src := TauCeti.Symplectic.tangentMatrix m; { toLinearMap := __src, map_lie' := ⋯ }) ⋯

@[simp]

theorem TauCeti.Symplectic.tangentLieEquivSp_apply {R : Type u} [CommRing R] {B : Type v} [CommRing B] [Algebra R B] (m : ℕ) (d : Derivation R (↑(coordinateHopfAlgebra R m)) (Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R m)) B)) : (tangentLieEquivSp m) d = (tangentMatrix m) d

The Lie equivalence computes by the symplectic tangent-matrix map.