Base change of the symplectic group

For a morphism of commutative rings R → K, scalar extension of the coordinate Hopf algebra of Sp₂ₘ is canonically the coordinate Hopf algebra constructed directly over K.

The proof transports the entries of the matrix relation X Jₘ Xᵀ - Jₘ across the existing base-change isomorphism for GL (m + m). It therefore identifies the base change of the symplectic defining Hopf ideal with the symplectic defining ideal over K, after which the general base-change theorem for Hopf-ideal quotients gives the result.

Main declarations

• TauCeti.Symplectic.coordinateHopfAlgebraBaseChangeIso: base change of the coordinate Hopf algebra of Sp₂ₘ.
• TauCeti.Symplectic.baseChangeMap_coordinateMap_comp_coordinateHopfAlgebraBaseChangeIso_hom: compatibility with the quotient coordinate morphisms from O(GL (m + m)).
• TauCeti.Symplectic.finiteTypeCoordinateHopfAlgebraBaseChangeIso: the finite-type form of the same isomorphism.

References

• J. S. Milne, Basic Theory of Affine Group Schemes, Chapter IV, §1.8.
• The Stacks Project, Tags 01JO and 022W.

The quotient-transport construction follows TauCeti.SpecialLinear.coordinateHopfAlgebraBaseChangeIso, replacing its determinant relation by the symplectic matrix relations.

This is the scalar-extension compatibility needed before the Sp₂ₘ worked example can be proved reductive in Layer 6, "Reductive and semisimple groups", of the ReductiveGroups roadmap.

@[instance_reducible]

noncomputable def TauCeti.Symplectic.instAlgebraXCoordinateHopfAlgebraHAddNat (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (m : ℕ) : Algebra R ↑(GeneralLinear.coordinateHopfAlgebra K (m + m))

The R-algebra structure obtained by restricting the coordinate algebra over K.

Equations

• TauCeti.Symplectic.instAlgebraXCoordinateHopfAlgebraHAddNat R K m = Algebra.compHom (↑(TauCeti.GeneralLinear.coordinateHopfAlgebra K (m + m))) (algebraMap R K)

theorem TauCeti.Symplectic.instIsScalarTowerXCoordinateHopfAlgebraHAddNat (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (m : ℕ) : IsScalarTower R K ↑(GeneralLinear.coordinateHopfAlgebra K (m + m))

The coordinate algebra over K is a scalar tower over R → K.

theorem TauCeti.Symplectic.coordinateHopfAlgebraBaseChangeIso_hom_relationMatrix (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (m : ℕ) (i j : Fin (m + m)) : (CommHopfAlgCat.Hom.hom (GeneralLinear.coordinateHopfAlgebraBaseChangeIso R K (m + m)).hom) (1 ⊗ₜ[R] relationMatrix R m i j) = relationMatrix K m i j

The general-linear base-change isomorphism carries each scalar-extended symplectic relation to the corresponding relation over the new base.

noncomputable def TauCeti.Symplectic.coordinateHopfAlgebraBaseChangeIso (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (m : ℕ) : CommHopfAlgCat.baseChange (coordinateHopfAlgebra R m) ≅ coordinateHopfAlgebra K m

Base change of the symplectic coordinate Hopf algebra is canonically the symplectic coordinate Hopf algebra over the new base.

Equations

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

@[simp]

theorem TauCeti.Symplectic.baseChangeMap_coordinateMap_comp_coordinateHopfAlgebraBaseChangeIso_hom (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (m : ℕ) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.baseChangeMap (coordinateMap R m)) (coordinateHopfAlgebraBaseChangeIso R K m).hom = CategoryTheory.CategoryStruct.comp (GeneralLinear.coordinateHopfAlgebraBaseChangeIso R K (m + m)).hom (coordinateMap K m)

The symplectic base-change isomorphism is compatible with the quotient coordinate morphisms from the corresponding general-linear coordinate Hopf algebras.

noncomputable def TauCeti.Symplectic.finiteTypeCoordinateHopfAlgebraBaseChangeIso (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (m : ℕ) : (finiteTypeCoordinateHopfAlgebra R m).baseChange ≅ finiteTypeCoordinateHopfAlgebra K m

The finite-type coordinate Hopf algebra of Sp₂ₘ commutes with base change.

Equations

• TauCeti.Symplectic.finiteTypeCoordinateHopfAlgebraBaseChangeIso R K m = TauCeti.FiniteTypeCommHopfAlgCat.baseChangeIsoOfObjIso ⋯ ⋯ (TauCeti.Symplectic.coordinateHopfAlgebraBaseChangeIso R K m)

@[simp]

theorem TauCeti.Symplectic.finiteTypeCoordinateHopfAlgebraBaseChangeIso_hom (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (m : ℕ) : (finiteTypeCoordinateHopfAlgebraBaseChangeIso R K m).hom.hom = (CategoryTheory.eqToIso ⋯ ≪≫ coordinateHopfAlgebraBaseChangeIso R K m ≪≫ CategoryTheory.eqToIso ⋯).hom

The underlying commutative-Hopf-algebra morphism of the finite-type base-change isomorphism is the coordinate-Hopf-algebra base-change isomorphism, with the object equalities made explicit.