Documentation

TauCeti.Algebra.AlgebraicGroup.Representation.Faithful.BaseChange

Base change of faithful comodules #

Let M be a finite free comodule over a commutative Hopf algebra H. After extending both the coefficient Hopf algebra and M along a morphism of commutative rings, the coordinate morphism of the extended comodule is the scalar extension of the original coordinate morphism, transported through the canonical base-change isomorphism for O(GLₙ).

Consequently, scalar extension preserves faithful comodules: surjectivity of the coordinate morphism survives base change.

Main declarations #

References #

This transports the faithful representation used to prove base-change invariance of geometric unipotence, the next scalar-extension step for the unipotent radical in Layer 5 of the ReductiveGroups roadmap.

source
theorem TauCeti.Comodule.coordinateBialgHom_baseChange {k H M : Type u} {K : Type (max u v)} [CommRing k] [CommRing K] [Algebra k K] [CommRing H] [HopfAlgebra k H] [AddCommMonoid M] [Module k M] [Comodule k H M] {d : ℕ} (b : Module.Basis (Fin d) k M) :
coordinateBialgHom (Module.Basis.baseChange K b) = CommHopfAlgCat.Hom.hom (CategoryTheory.CategoryStruct.comp (GeneralLinear.coordinateHopfAlgebraBaseChangeIso k K d).inv (CommHopfAlgCat.baseChangeMap (CommHopfAlgCat.ofHom (coordinateBialgHom b))))

The coordinate morphism of a base-changed comodule is the scalar extension of its original coordinate morphism, after identifying the scalar extension of O(GLₙ) with O(GLₙ) over the new base.

source
theorem TauCeti.Comodule.IsFaithful.baseChange {k H M : Type u} {K : Type (max u v)} [CommRing k] [CommRing K] [Algebra k K] [CommRing H] [HopfAlgebra k H] [AddCommMonoid M] [Module k M] [Comodule k H M] (hM : IsFaithful) :
IsFaithful

Scalar extension of the coefficient Hopf algebra and underlying module preserves a faithful finite free comodule.