Matrix coefficients under base change #
Extending a finite free comodule and its coefficient coalgebra along the same scalar morphism extends every entry of its coefficient matrix. This is the coordinate calculation needed to transport faithful representations across field extensions.
Main declaration #
TauCeti.Comodule.coefficientMatrix_baseChange: the coefficient matrix in the base-changed basis is obtained by sendingcᵢⱼto1 ⊗ cᵢⱼ.
References #
- M. Sweedler, Hopf Algebras, Chapter 2.
This supplies the matrix-coefficient compatibility needed for base-change invariance of geometric unipotence in Layer 5 of the ReductiveGroups roadmap.
@[simp]
theorem
TauCeti.Comodule.coefficientMatrix_baseChange
{R : Type u}
{A : Type v}
{C : Type w}
{M : Type x}
{ι : Type u_1}
[CommSemiring R]
[CommSemiring A]
[Algebra R A]
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[AddCommMonoid M]
[Module R M]
[Comodule R C M]
(b : Module.Basis ι R M)
:
coefficientMatrix (Module.Basis.baseChange A b) = (coefficientMatrix b).map ⇑((TensorProduct.mk R A C) 1)
Base change sends every entry of a comodule's coefficient matrix to the corresponding pure tensor in the base-changed coefficient coalgebra.