Normal unipotent subgroups seen through a faithful representation

Let H be a reduced finite-type commutative Hopf algebra over an algebraically closed field k and let M be a finite-dimensional H-comodule which is completely reducible and faithful. Then every normal Hopf ideal of H whose quotient is smooth unipotent is the augmentation ideal: contravariantly, every normal smooth unipotent closed subgroup of the represented affine group is trivial. Consequently the unipotent radical of H is trivial.

Smoothness of the quotient makes the subgroup coordinate ring reduced, and geometric unipotence says that all of its points act unipotently. Normality makes the fixed vectors of the subgroup an ambient subcomodule, so the normal-invariants theorem together with Kolchin's fixed-vector theorem forces the subgroup to act trivially on M, and faithfulness then identifies its defining ideal with the augmentation ideal.

Only the existence of one faithful completely reducible finite-dimensional representation is used, so the same statement serves GLₙ, SLₙ and the explicit Chevalley carriers. Neither smoothness nor connectedness of H itself is needed; reducedness of H is.

Main results

• TauCeti.HopfIdeal.eq_augmentation_of_isNormal_of_forall_isUnipotentPoint_of_isFaithful: a normal subgroup with reduced quotient and only unipotent points is trivial.
• TauCeti.HopfIdeal.eq_augmentation_of_isNormal_of_smoothUnipotent_of_isFaithful: a normal smooth unipotent closed subgroup of such an H is trivial.
• TauCeti.HopfIdeal.eq_augmentation_of_isNormal_of_smoothUnipotent_of_isFaithful_of_iso: the same conclusion after transporting the subgroup across an isomorphism.
• TauCeti.FiniteTypeCommHopfAlgCat.unipotentRadicalDefiningIdeal_eq_augmentation_of_isFaithful: the unipotent radical of such an H is trivial.

References

• J. S. Milne, Algebraic Groups (2017), §§4.a, 5 and 19.b.
• J. E. Humphreys, Linear Algebraic Groups, §§19 and 26.
• J. C. Jantzen, Representations of Algebraic Groups, I.2 and II.2.
• The argument is the one already formalized for SLₙ in TauCeti/Algebra/AlgebraicGroup/SpecialLinear/Reductive/Basic.lean.

theorem TauCeti.HopfIdeal.eq_augmentation_of_isNormal_of_forall_isUnipotentPoint_of_isFaithful (k : Type u) [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) [IsReduced ↑H.obj] (M : Type u) [AddCommGroup M] [Module k M] [Comodule k (↑H.obj) M] [FiniteDimensional k M] (hcr : Comodule.IsCompletelyReducible k (↑H.obj) M) (hM : Comodule.IsFaithful) (I : HopfIdeal k ↑H.obj) (hI : I.IsNormal) [IsReduced ↑(CommHopfAlgCat.quotient H.obj I)] (hu : ∀ (g : WithConv (↑(CommHopfAlgCat.quotient H.obj I) →ₐ[k] k)), HopfAlgebra.IsUnipotentPoint g) : I = augmentation k ↑H.obj

A normal closed subgroup is trivial when its quotient is reduced, all of its points are unipotent, and the ambient affine group has a faithful completely reducible representation.

The conclusion is stated contravariantly: the subgroup's defining Hopf ideal is the augmentation ideal.

theorem TauCeti.HopfIdeal.eq_augmentation_of_isNormal_of_smoothUnipotent_of_isFaithful (k : Type u) [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) [IsReduced ↑H.obj] (M : Type u) [AddCommGroup M] [Module k M] [Comodule k (↑H.obj) M] [FiniteDimensional k M] (hcr : Comodule.IsCompletelyReducible k (↑H.obj) M) (hM : Comodule.IsFaithful) (I : HopfIdeal k ↑H.obj) (hI : I.IsNormal) (hU : smoothUnipotentCommHopfAlgProperty k (H.quotient I)) : I = augmentation k ↑H.obj

A normal smooth unipotent closed subgroup is trivial as soon as the ambient reduced finite-type affine group has a faithful completely reducible finite-dimensional representation.

The conclusion is stated contravariantly: the subgroup's defining Hopf ideal is the augmentation ideal. Neither smoothness nor connectedness of the ambient group is needed.

theorem TauCeti.HopfIdeal.eq_augmentation_of_isNormal_of_smoothUnipotent_of_isFaithful_of_iso (k : Type u) [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) [IsReduced ↑H.obj] (M : Type u) [AddCommGroup M] [Module k M] [Comodule k (↑H.obj) M] [FiniteDimensional k M] (H' : FiniteTypeCommHopfAlgCat k) (e : H.obj ≅ H'.obj) (hcr : Comodule.IsCompletelyReducible k (↑H.obj) M) (hM : Comodule.IsFaithful) (I : HopfIdeal k ↑H'.obj) (hI : I.IsNormal) (hU : smoothUnipotentCommHopfAlgProperty k (H'.quotient I)) : I = augmentation k ↑H'.obj

A normal smooth unipotent closed subgroup is trivial when an isomorphic presentation of the ambient group has a faithful completely reducible representation.

This packages the transport of the subgroup ideal, quotient, and augmentation ideal across the chosen isomorphism.

theorem TauCeti.FiniteTypeCommHopfAlgCat.unipotentRadicalDefiningIdeal_eq_augmentation_of_isFaithful (k : Type u) [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) [IsReduced ↑H.obj] (M : Type u) [AddCommGroup M] [Module k M] [Comodule k (↑H.obj) M] [FiniteDimensional k M] (hcr : Comodule.IsCompletelyReducible k (↑H.obj) M) (hM : Comodule.IsFaithful) : H.unipotentRadicalDefiningIdeal = HopfIdeal.augmentation k ↑H.obj

The unipotent radical is trivial as soon as the reduced finite-type affine group has a faithful completely reducible finite-dimensional representation.