Faithful representations and matrix coefficients

Let M be a finite free comodule over a commutative Hopf algebra H. A basis of M gives a coordinate morphism

O(GL(M)) ⟶ H.

This file identifies its range with the algebra generated by the matrix coefficients of M and their antipode images. Equivalently, it is the coefficient algebra of M × Mᵛ, where Mᵛ is the dual comodule. It follows that the associated morphism of affine group schemes is a closed immersion exactly when those coefficients generate H.

The dual coefficients are essential. For the standard one-dimensional representation of 𝔾ₘ, the original coefficient is T, whereas the dual coefficient is T⁻¹; together they generate R[T, T⁻¹]. Thus a criterion using only the original coefficient algebra would fail even for the identity representation of 𝔾ₘ.

This completes the ReductiveGroups roadmap's Layer 1 target "Faithfulness done right": faithful means that the representation morphism is a closed immersion, and this geometric condition is equivalent to generation of the coordinate ring by matrix coefficients and their duals.

Main declarations

• TauCeti.Comodule.coordinateBialgHom_range: the exact range of the coordinate morphism.
• TauCeti.Comodule.IsFaithful: the basis-independent predicate for a faithful comodule.
• TauCeti.Comodule.isFaithful_iff_matrixCoefficientSubalgebra_sup_antipode_eq_top: the matrix-coefficient criterion for faithfulness.
• TauCeti.Comodule.isFaithful_corestrict_of_surjective: corestriction along a surjective bialgebra morphism preserves faithfulness.
• TauCeti.Comodule.pointsAction_injective_of_isFaithful: a faithful comodule separates algebra-valued points.
• TauCeti.Comodule.isClosedImmersion_coordinateGroupSchemeHom_iff_of_bases: faithfulness is independent of the chosen finite basis.

References

• J. S. Milne, Algebraic Groups (2017), Remark 4.1 and Theorems 4.9 and 4.14.

theorem TauCeti.Comodule.coordinateBialgHom_range {R : Type u} {H : Type v} {M : Type w} {n : ℕ} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] (b : Module.Basis (Fin n) R M) : (↑(coordinateBialgHom b)).range = matrixCoefficientSubalgebra ⊔ Subalgebra.map (HopfAlgebra.antipodeAlgHom R H) matrixCoefficientSubalgebra

The range of a comodule's coordinate morphism is generated by its coefficients and their antipode images.

The first summand records the images of the generic matrix entries of O(GLₙ); the second records the images of the inverse-matrix entries.

theorem TauCeti.Comodule.coordinateBialgHom_surjective_iff_matrixCoefficientSubalgebra_sup_antipode_eq_top {R : Type u} {H : Type v} {M : Type w} {n : ℕ} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] (b : Module.Basis (Fin n) R M) : Function.Surjective ⇑(coordinateBialgHom b) ↔ matrixCoefficientSubalgebra ⊔ Subalgebra.map (HopfAlgebra.antipodeAlgHom R H) matrixCoefficientSubalgebra = ⊤

The coordinate morphism is surjective exactly when the matrix coefficients and their antipode images generate the coordinate Hopf algebra.

theorem TauCeti.Comodule.coordinateBialgHom_range_eq_matrixCoefficientSubalgebra_prod_dual {R : Type u} {H : Type v} {M : Type w} {n : ℕ} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] (b : Module.Basis (Fin n) R M) : (↑(coordinateBialgHom b)).range = matrixCoefficientSubalgebra

The range of a comodule's coordinate morphism is equivalently the coefficient algebra of the direct sum of the comodule and its dual.

theorem TauCeti.Comodule.coordinateBialgHom_surjective_iff_matrixCoefficientSubalgebra_prod_dual_eq_top {R : Type u} {H : Type v} {M : Type w} {n : ℕ} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] (b : Module.Basis (Fin n) R M) : Function.Surjective ⇑(coordinateBialgHom b) ↔ matrixCoefficientSubalgebra = ⊤

The coordinate morphism is surjective exactly when the coefficients of the comodule and its dual generate the coordinate Hopf algebra. This is the rigid-category form of the matrix-coefficient-and-antipode criterion above.

def TauCeti.Comodule.IsFaithful {k H V : Type u} [CommRing k] [CommRing H] [HopfAlgebra k H] [AddCommMonoid V] [Module k V] [Comodule k H V] : Prop

A comodule is faithful if its representation morphism into a general linear group is a closed immersion for some finite basis. This property is independent of the witnessing basis.

Equations

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

theorem TauCeti.Comodule.isFaithful_def {k H V : Type u} [CommRing k] [CommRing H] [HopfAlgebra k H] [AddCommMonoid V] [Module k V] [Comodule k H V] : IsFaithful ↔ ∃ (d : ℕ) (b : Module.Basis (Fin d) k V), AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (coordinateGroupSchemeHom b).hom.hom)

Faithfulness restated as the existence of a finite basis whose representation morphism is a closed immersion.

theorem TauCeti.Comodule.isClosedImmersion_coordinateGroupSchemeHom_iff_matrixCoefficientSubalgebra_sup_antipode_eq_top {k H V : Type u} {d : ℕ} [CommRing k] [CommRing H] [HopfAlgebra k H] [AddCommMonoid V] [Module k V] [Comodule k H V] (b : Module.Basis (Fin d) k V) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (coordinateGroupSchemeHom b).hom.hom) ↔ matrixCoefficientSubalgebra ⊔ Subalgebra.map (HopfAlgebra.antipodeAlgHom k H) matrixCoefficientSubalgebra = ⊤

Faithfulness is generation by matrix coefficients. The affine group-scheme morphism associated to a finite free comodule is a closed immersion if and only if the coefficients of the comodule together with their antipode images generate the coordinate Hopf algebra.

theorem TauCeti.Comodule.isClosedImmersion_coordinateGroupSchemeHom_iff_of_bases {k H V : Type u} {d : ℕ} [CommRing k] [CommRing H] [HopfAlgebra k H] [AddCommMonoid V] [Module k V] [Comodule k H V] {e : ℕ} (b : Module.Basis (Fin d) k V) (c : Module.Basis (Fin e) k V) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (coordinateGroupSchemeHom b).hom.hom) ↔ AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (coordinateGroupSchemeHom c).hom.hom)

Whether a finite free comodule defines a closed immersion into a general linear group is independent of the chosen basis. The two target general linear groups may use different finite index types; the matrix-coefficient criterion is basis-free.

theorem TauCeti.Comodule.isFaithful_iff_isClosedImmersion_coordinateGroupSchemeHom {k H V : Type u} {d : ℕ} [CommRing k] [CommRing H] [HopfAlgebra k H] [AddCommMonoid V] [Module k V] [Comodule k H V] (b : Module.Basis (Fin d) k V) : IsFaithful ↔ AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (coordinateGroupSchemeHom b).hom.hom)

A finite basis witnesses faithfulness exactly when its coordinate group-scheme morphism is a closed immersion.

theorem TauCeti.Comodule.isFaithful_corestrict_of_surjective {k H V : Type u} [CommRing k] [CommRing H] [HopfAlgebra k H] [AddCommMonoid V] [Module k V] [Comodule k H V] {K : Type u} [CommRing K] [HopfAlgebra k K] (f : H →ₐc[k] K) (hf : Function.Surjective ⇑f) (hV : IsFaithful) : IsFaithful

Corestricting a faithful finite free comodule along a surjective bialgebra morphism gives a faithful comodule over the codomain. Geometrically, restricting a faithful representation to a closed subgroup remains faithful.

theorem TauCeti.Comodule.isFaithful_iff_matrixCoefficientSubalgebra_sup_antipode_eq_top {k H V : Type u} {d : ℕ} [CommRing k] [CommRing H] [HopfAlgebra k H] [AddCommMonoid V] [Module k V] [Comodule k H V] (b : Module.Basis (Fin d) k V) : IsFaithful ↔ matrixCoefficientSubalgebra ⊔ Subalgebra.map (HopfAlgebra.antipodeAlgHom k H) matrixCoefficientSubalgebra = ⊤

A finite free comodule is faithful exactly when its matrix coefficients together with their antipode images generate the coordinate Hopf algebra.

theorem TauCeti.Comodule.pointsAction_injective_of_isFaithful {k H V : Type u} [CommRing k] [CommRing H] [HopfAlgebra k H] [AddCommMonoid V] [Module k V] [Comodule k H V] {K : Type x} [CommRing K] [Algebra k K] (hV : IsFaithful) : Function.Injective ⇑(pointsAction V)

A faithful comodule separates algebra-valued points.

theorem TauCeti.Comodule.isFaithful_iff_matrixCoefficientSubalgebra_prod_dual_eq_top {k H V : Type u} {d : ℕ} [CommRing k] [CommRing H] [HopfAlgebra k H] [AddCommMonoid V] [Module k V] [Comodule k H V] (b : Module.Basis (Fin d) k V) : IsFaithful ↔ matrixCoefficientSubalgebra = ⊤

In a finite free comodule, the faithful-representation criterion can be read as generation by the coefficients of the comodule together with its dual.