Faithful representations of closed subgroups

Let M be a finite free comodule over a commutative Hopf algebra H. Corestricting its coaction along a surjective bialgebra morphism H ⟶ K restricts the corresponding representation to the closed subgroup represented by K. Its coordinate morphism is the composite

O(GL(M)) ⟶ H ⟶ K.

Consequently a faithful representation stays faithful after restriction to a closed subgroup. If that restricted representation is trivial, faithfulness forces the subgroup itself to be the identity subgroup. The final Hopf-ideal form says that a closed subgroup acting trivially through a faithful ambient representation is cut out by the augmentation ideal.

This is the kernel-elimination input for the direct proof that GLₙ is reductive. For a connected normal smooth unipotent closed subgroup, the normal-invariants argument makes its fixed vectors an ambient subrepresentation; simplicity of the standard representation makes every vector fixed, and the result here then identifies the subgroup with the identity.

Main declarations

• TauCeti.Comodule.augmentation_eq_bot_of_isFaithful_of_coact_eq_tmul_one: a Hopf algebra with a faithful trivial representation is trivial.
• TauCeti.Comodule.eq_augmentation_of_isFaithful_of_quotient_coact_eq_tmul_one: a closed subgroup acting trivially in a faithful representation is the identity subgroup.

References

• J. S. Milne, Algebraic Groups (2017), §4.a and §5.
• T. A. Springer, Linear Algebraic Groups, §2.2.

This advances the worked-example target GLₙ is reductive in Layer 6 of the ReductiveGroups roadmap. It supplies the faithful-representation step used after normal-subgroup invariants and Kolchin's fixed-vector theorem.

theorem TauCeti.Comodule.augmentation_eq_bot_of_isFaithful_of_coact_eq_tmul_one {R H M : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] (hM : IsFaithful) (htrivial : ∀ (m : M), coact m = m ⊗ₜ[R] 1) : HopfIdeal.augmentation R H = ⊥

A commutative Hopf algebra admitting a faithful finite free comodule with trivial coaction has zero augmentation ideal. Equivalently, the represented affine group is the identity group.

theorem TauCeti.Comodule.eq_augmentation_of_isFaithful_of_quotient_coact_eq_tmul_one {R H M : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] (I : HopfIdeal R H) (hM : IsFaithful) (htrivial : ∀ (m : M), (TensorProduct.map LinearMap.id (CommHopfAlgCat.Hom.hom (CommHopfAlgCat.mkQuotient (↧H) I)).toLinearMap) (coact m) = m ⊗ₜ[R] 1) : I = HopfIdeal.augmentation R H

A closed subgroup acting trivially through a faithful finite free representation is the identity subgroup: its defining Hopf ideal is the augmentation ideal of the ambient group.