Base change of the special linear group

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

The proof starts from the corresponding base-change isomorphism for GLₙ. It sends the base-changed generic determinant to the generic determinant over K, and therefore carries the base change of the determinant-one Hopf ideal onto the determinant-one Hopf ideal over K. The result then follows from the general theorem that a Hopf-ideal quotient commutes with base change.

Main declarations

• TauCeti.SpecialLinear.coordinateHopfAlgebraBaseChangeIso: base change of the coordinate Hopf algebra of SLₙ.
• TauCeti.SpecialLinear.finiteTypeCoordinateHopfAlgebraBaseChangeIso: the finite-type form of the same isomorphism.
• TauCeti.SpecialLinear.finiteTypeCoordinateHopfAlgebraBaseChangeIso_hom: its underlying commutative-Hopf-algebra morphism.

References

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

This is the scalar-extension compatibility needed to assemble the SLₙ worked example in Layer 6, "Reductive and semisimple groups", of the ReductiveGroups roadmap.

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

Base change of the special-linear coordinate Hopf algebra is canonically the special-linear coordinate Hopf algebra over the new base.

Equations

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

@[simp]

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

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

theorem TauCeti.SpecialLinear.coordinateHopfAlgebraBaseChangeIso_hom_tmul_coordinateMap (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) (s : K) (x : ↑(GeneralLinear.coordinateHopfAlgebra R n)) : (CommHopfAlgCat.Hom.hom (coordinateHopfAlgebraBaseChangeIso R K n).hom) (s ⊗ₜ[R] (CommHopfAlgCat.Hom.hom (coordinateMap R n)) x) = (CommHopfAlgCat.Hom.hom (coordinateMap K n)) ((CommHopfAlgCat.Hom.hom (GeneralLinear.coordinateHopfAlgebraBaseChangeIso R K n).hom) (s ⊗ₜ[R] x))

On a pure tensor of a restricted general-linear function, the special-linear base-change isomorphism is the general-linear isomorphism followed by restriction.

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

The finite-type coordinate Hopf algebra of SLₙ commutes with base change.

Equations

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

@[simp]

theorem TauCeti.SpecialLinear.finiteTypeCoordinateHopfAlgebraBaseChangeIso_hom (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) : (finiteTypeCoordinateHopfAlgebraBaseChangeIso R K n).hom.hom = (CategoryTheory.eqToIso ⋯ ≪≫ coordinateHopfAlgebraBaseChangeIso R K n ≪≫ 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.