The symplectic subgroup scheme of GL₂ₘ

For a commutative ring R and m : ℕ, the symplectic subgroup scheme Sp₂ₘ of GL (m + m) is the subgroup scheme preserving the standard alternating form Jₘ: the specialization of TauCeti.ConstantForm at C = Jₘ, cut out of GL (m + m) by the entries of

X Jₘ Xᵀ - Jₘ

for X the localized generic matrix and Jₘ the standard alternating form in Fin (m + m) coordinates. On every commutative R-algebra A, its points are the existing subgroup TauCeti.GLSymplecticFin m A, equivalently TauCeti.GLSymplectic (Fin m) A, and that identification is what this file adds to the general construction.

Together with TauCeti.GLSymplectic, this completes the Sp₂ₘ worked example of the ReductiveGroups roadmap at the same boundary as the Borel example (TauCeti.GeneralLinear.Borel): construction and points identification, with no smoothness or reductivity claim.

The Hopf-ideal closure conditions, the quotient, the group scheme with its closed immersion into GL (m + m), and the ambient membership criterion M C Mᵀ = C all come from TauCeti.ConstantForm, which proves them for an arbitrary constant matrix C (local finite type is the generic instance for Hopf-ideal quotients of the ambient coordinate algebra); no invertibility or nondegeneracy of Jₘ is used anywhere. The construction includes m = 0 and the zero ring.

Main declarations

• TauCeti.Symplectic.relationMatrix: the matrix of defining relations X Jₘ Xᵀ - Jₘ.
• TauCeti.Symplectic.definingHopfIdeal: the Hopf ideal its entries generate.
• TauCeti.Symplectic.coordinateHopfAlgebra and TauCeti.Symplectic.coordinateMap: the symplectic coordinate Hopf algebra, the quotient by the defining Hopf ideal, and the quotient morphism onto it.
• TauCeti.Symplectic.groupScheme and TauCeti.Symplectic.inclusion: the symplectic subgroup scheme and its closed immersion into the general linear group scheme.
• TauCeti.Symplectic.pointsMulEquiv: the group of algebra-valued points of the symplectic coordinate Hopf algebra is TauCeti.GLSymplecticFin, and TauCeti.Symplectic.pointsMulEquivGLSymplectic reads it in Fin m ⊕ Fin m coordinates.

References

• J. S. Milne, Algebraic Groups (2017), §2.3 and §24.6: Sp₂ₙ as the subgroup of GL₂ₙ preserving a nondegenerate alternating form, cut out by the entries of the form relation.
• The Stacks Project, Tag 022W, for the ambient general linear group scheme.

The closure computations this file relies on, and the framing identities behind them, are proved for an arbitrary constant form in TauCeti.ConstantForm.

The symplectic specialization of the constant-form construction

@[reducible, inline]

noncomputable abbrev TauCeti.Symplectic.relationMatrix (R : Type u) [CommRing R] (m : ℕ) : Matrix (Fin (m + m)) (Fin (m + m)) ↑(GeneralLinear.coordinateHopfAlgebra R (m + m))

The matrix of defining relations of the symplectic subgroup scheme: X Jₘ Xᵀ - Jₘ over the coordinate Hopf algebra of GL (m + m), the constant-form relation matrix at C = Jₘ.

Equations

• TauCeti.Symplectic.relationMatrix R m = TauCeti.ConstantForm.relationMatrix R (m + m) (TauCeti.JFin m R)

theorem TauCeti.Symplectic.relationMatrix_def (R : Type u) [CommRing R] (m : ℕ) : relationMatrix R m = GeneralLinear.genericMatrix R (m + m) * JFin m ↑(GeneralLinear.coordinateHopfAlgebra R (m + m)) * (GeneralLinear.genericMatrix R (m + m)).transpose - JFin m ↑(GeneralLinear.coordinateHopfAlgebra R (m + m))

The relation matrix is the standard alternating form transported by the generic matrix, minus the form: X Jₘ Xᵀ - Jₘ.

@[reducible, inline]

abbrev TauCeti.Symplectic.relationSet (R : Type u) [CommRing R] (m : ℕ) : Set ↑(GeneralLinear.coordinateHopfAlgebra R (m + m))

The set of defining relations: the entries of the relation matrix.

Equations

• TauCeti.Symplectic.relationSet R m = TauCeti.ConstantForm.relationSet R (m + m) (TauCeti.JFin m R)

@[reducible, inline]

noncomputable abbrev TauCeti.Symplectic.definingHopfIdeal (R : Type u) [CommRing R] (m : ℕ) : HopfIdeal R ↑(GeneralLinear.coordinateHopfAlgebra R (m + m))

The symplectic Hopf ideal: the ideal of the coordinate Hopf algebra of GL (m + m) generated by the entries of X Jₘ Xᵀ - Jₘ.

Equations

• TauCeti.Symplectic.definingHopfIdeal R m = TauCeti.ConstantForm.definingHopfIdeal R (m + m) (TauCeti.JFin m R)

@[reducible, inline]

noncomputable abbrev TauCeti.Symplectic.coordinateHopfAlgebra (R : Type u) [CommRing R] (m : ℕ) : CommHopfAlgCat R

The coordinate Hopf algebra of the symplectic subgroup scheme of GL (m + m).

Equations

• TauCeti.Symplectic.coordinateHopfAlgebra R m = TauCeti.ConstantForm.coordinateHopfAlgebra R (m + m) (TauCeti.JFin m R)

@[reducible, inline]

noncomputable abbrev TauCeti.Symplectic.coordinateMap (R : Type u) [CommRing R] (m : ℕ) : GeneralLinear.coordinateHopfAlgebra R (m + m) ⟶ coordinateHopfAlgebra R m

The quotient coordinate morphism from O(GL (m + m)) to the symplectic coordinate Hopf algebra.

Equations

• TauCeti.Symplectic.coordinateMap R m = TauCeti.ConstantForm.coordinateMap R (m + m) (TauCeti.JFin m R)

theorem TauCeti.Symplectic.coordinateMap_def (R : Type u) [CommRing R] (m : ℕ) : coordinateMap R m = CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra R (m + m)) (definingHopfIdeal R m)

The symplectic coordinate map is the canonical quotient morphism by the defining Hopf ideal.

@[reducible, inline]

noncomputable abbrev TauCeti.Symplectic.groupScheme (R : Type u) [CommRing R] (m : ℕ) : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))

The symplectic subgroup scheme of GL (m + m).

Equations

• TauCeti.Symplectic.groupScheme R m = TauCeti.ConstantForm.groupScheme R (m + m) (TauCeti.JFin m R)

theorem TauCeti.Symplectic.groupScheme_def (R : Type u) [CommRing R] (m : ℕ) : groupScheme R m = CommHopfAlgCat.quotientSpec (GeneralLinear.coordinateHopfAlgebra R (m + m)) (definingHopfIdeal R m)

The symplectic group scheme is the quotient spectrum of its coordinate Hopf algebra.

@[reducible, inline]

noncomputable abbrev TauCeti.Symplectic.finiteTypeCoordinateHopfAlgebra (R : Type u) [CommRing R] (m : ℕ) : FiniteTypeCommHopfAlgCat R

The symplectic coordinate Hopf algebra, bundled with its finite-type property.

Equations

• TauCeti.Symplectic.finiteTypeCoordinateHopfAlgebra R m = TauCeti.ConstantForm.finiteTypeCoordinateHopfAlgebra R (m + m) (TauCeti.JFin m R)

theorem TauCeti.Symplectic.finiteTypeCoordinateHopfAlgebra_obj (R : Type u) [CommRing R] (m : ℕ) : (finiteTypeCoordinateHopfAlgebra R m).obj = coordinateHopfAlgebra R m

The finite-type package has the symplectic coordinate Hopf algebra as its underlying object.

@[reducible, inline]

noncomputable abbrev TauCeti.Symplectic.inclusion (R : Type u) [CommRing R] (m : ℕ) : groupScheme R m ⟶ GeneralLinear.groupScheme R (m + m)

The closed-subgroup inclusion from the symplectic subgroup scheme into the named general linear group scheme.

Equations

• TauCeti.Symplectic.inclusion R m = TauCeti.ConstantForm.inclusion R (m + m) (TauCeti.JFin m R)

theorem TauCeti.Symplectic.inclusion_eq_constantForm (R : Type u) [CommRing R] (m : ℕ) : inclusion R m = ConstantForm.inclusion R (m + m) (JFin m R)

The symplectic inclusion is the specialization of the constant-form inclusion at the standard alternating form.

theorem TauCeti.Symplectic.inclusion_def (R : Type u) [CommRing R] (m : ℕ) : inclusion R m = GeneralLinear.hopfIdealInclusion R (m + m) (definingHopfIdeal R m)

The symplectic inclusion is the generic Hopf-ideal closed immersion at the defining Hopf ideal.

Algebra-valued points

noncomputable def TauCeti.Symplectic.pointsMulEquiv (R : Type u) [CommRing R] (m : ℕ) {A : Type w} [CommRing A] [Algebra R A] : ↑(HopfAlgebra.points ↧A) ≃* ↥(GLSymplecticFin m A)

The points identification: the group of algebra-valued points of the symplectic coordinate Hopf algebra is the symplectic subgroup of the general linear group.

Equations

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

theorem TauCeti.Symplectic.pointsMulEquiv_coe (R : Type u) [CommRing R] (m : ℕ) {A : Type w} [CommRing A] [Algebra R A] (f : ↑(HopfAlgebra.points ↧A)) : (GeneralLinear.pointsMulEquiv (m + m)) ((CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra R (m + m)) (definingHopfIdeal R m) ↧A)) f) = ↑((pointsMulEquiv R m) f)

Under the symplectic and general-linear point equivalences, the quotient-point inclusion is the ordinary inclusion of symplectic matrices into GL (m + m).

@[simp]

theorem TauCeti.Symplectic.quotientPointsHom_pointsMulEquiv_symm (R : Type u) [CommRing R] (m : ℕ) {A : Type w} [CommRing A] [Algebra R A] (g : ↥(GLSymplecticFin m A)) : (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra R (m + m)) (definingHopfIdeal R m) ↧A)) ((pointsMulEquiv R m).symm g) = (GeneralLinear.pointsMulEquiv (m + m)).symm ↑g

The ambient point attached to a symplectic matrix is the general-linear point attached to its ordinary inclusion.

theorem TauCeti.Symplectic.pointsMulEquiv_mapValue (R : Type u) [CommRing R] (m : ℕ) {A : Type w} [CommRing A] [Algebra R A] {B : Type v} [CommRing B] [Algebra R B] (phi : A →ₐ[R] B) (f : ↑(HopfAlgebra.points ↧A)) : (pointsMulEquiv R m) ((AlgHom.mapValue phi) f) = (GLSymplecticFin.map m A ↑phi) ((pointsMulEquiv R m) f)

The symplectic point equivalence is natural in the value algebra: postcomposition of Hopf points agrees with entrywise mapping of symplectic matrices.

noncomputable def TauCeti.Symplectic.pointsMulEquivGLSymplectic (R : Type u) [CommRing R] (m : ℕ) {A : Type w} [CommRing A] [Algebra R A] : ↑(HopfAlgebra.points ↧A) ≃* ↥(GLSymplectic (Fin m) A)

The points identification, read in Fin m ⊕ Fin m coordinates: the points of the symplectic coordinate Hopf algebra are TauCeti.GLSymplectic (Fin m) A.

Equations

• TauCeti.Symplectic.pointsMulEquivGLSymplectic R m = (TauCeti.Symplectic.pointsMulEquiv R m).trans (TauCeti.GLSymplecticFin.mulEquivGLSymplectic m A)

@[simp]

theorem TauCeti.Symplectic.coe_pointsMulEquivGLSymplectic (R : Type u) [CommRing R] (m : ℕ) {A : Type w} [CommRing A] [Algebra R A] (f : ↑(HopfAlgebra.points ↧A)) : ↑((pointsMulEquivGLSymplectic R m) f) = (finSumFinEquiv.symm.reindexGL A) ↑((pointsMulEquiv R m) f)

On underlying general-linear elements, the Fin m ⊕ Fin m reading of a point is the reindexing of its Fin (m + m) reading.