Documentation

TauCeti.Algebra.HopfAlgebra.GroupLike.FiniteGeneration

Finite generation of group-like elements #

If a finite-type Hopf algebra over a nontrivial commutative ring is spanned by linearly independent group-like elements, then its group of group-like elements is finitely generated. Indeed, evaluation identifies the group algebra on the group-like elements with the original Hopf algebra. Finite type transports across this equivalence, and a group algebra over a nontrivial commutative ring is of finite type exactly when its indexing group is finitely generated.

The result does not require the Hopf algebra to be commutative. Over a domain, linear independence is automatic when the carrier is torsion-free.

Main declarations #

References #

See Milne, Algebraic Groups, Proposition 4.23 and Theorems 12.8--12.9.

source
theorem TauCeti.GroupLike.fg_of_finiteType_of_linearIndependent_of_groupLikeSetSpan_eq_top (R : Type u) (H : Type v) [CommRing R] [Nontrivial R] [Semiring H] [HopfAlgebra R H] (hfinite : Algebra.FiniteType R H) (hlinear : LinearIndependent R GroupLike.val) (hspan : Subcoalgebra.groupLikeSetSpan Set.univ = ⊤) :
Group.FG (GroupLike R H)

The linearly independent group-like elements spanning a finite-type Hopf algebra over a nontrivial commutative ring form a finitely generated group.

The spanning hypothesis is expressed intrinsically through the subcoalgebra spanned by all group-like elements.

source
theorem TauCeti.GroupLike.fg_of_finiteType_of_groupLikeSetSpan_eq_top (R : Type u) (H : Type v) [CommRing R] [IsDomain R] [Ring H] [HopfAlgebra R H] [Module.IsTorsionFree R H] (hfinite : Algebra.FiniteType R H) (hspan : Subcoalgebra.groupLikeSetSpan Set.univ = ⊤) :
Group.FG (GroupLike R H)

The group-like elements spanning a finite-type Hopf algebra over a domain form a finitely generated group, provided the carrier is torsion-free over the base.