Torsion in groups of group-like elements

Group-like elements of a Hopf algebra over a field are linearly independent, so evaluation embeds their group algebra into the Hopf algebra. Consequently, reducedness and connectedness of the Hopf algebra pass to this group algebra and force its group of group-like elements to be torsion-free.

Contravariantly, a bialgebra homomorphism from a group algebra into such a Hopf algebra kills every torsion element of the indexing group. If the indexing group is torsion, the homomorphism factors through the counit.

Main declarations

• TauCeti.isMulTorsionFree_groupLike_of_isReduced_of_connectedSpace: group-like elements of a reduced Hopf algebra with connected spectrum form a torsion-free group.
• IsGroupLikeElem.eq_one_of_pow_eq_one: the elementwise form.
• BialgHom.monoidAlgebra_single_eq_one: a bialgebra homomorphism kills torsion basis elements.
• BialgHom.monoidAlgebra_eq_algebraMap_counit: a bialgebra homomorphism from the group algebra of a torsion group factors through the counit.

References

• J. S. Milne, Algebraic Groups (2017), Definitions 12.14 and 12.17.
• W. C. Waterhouse, Introduction to Affine Group Schemes, Chapter 2.

theorem TauCeti.isMulTorsionFree_groupLike_of_isReduced_of_connectedSpace (k : Type u) [Field k] (H : Type v) [CommRing H] [HopfAlgebra k H] [IsReduced H] [ConnectedSpace (PrimeSpectrum H)] : IsMulTorsionFree (GroupLike k H)

The group-like elements of a reduced Hopf algebra with connected spectrum form a torsion-free group.

theorem IsGroupLikeElem.eq_one_of_pow_eq_one {k : Type u} [Field k] {H : Type v} [CommRing H] [HopfAlgebra k H] [IsReduced H] [ConnectedSpace (PrimeSpectrum H)] {a : H} (ha : IsGroupLikeElem k a) {n : ℕ} (hn : n ≠ 0) (hpow : a ^ n = 1) : a = 1

A group-like element of finite order in a reduced Hopf algebra with connected spectrum is trivial.

@[simp]

theorem BialgHom.monoidAlgebra_single_eq_one {k : Type u} [Field k] {H : Type v} [CommRing H] [HopfAlgebra k H] [IsReduced H] [ConnectedSpace (PrimeSpectrum H)] {M : Type w} [Monoid M] (f : MonoidAlgebra k M →ₐc[k] H) {m : M} (hm : IsOfFinOrder m) : f (MonoidAlgebra.single m 1) = 1

A bialgebra homomorphism into a reduced Hopf algebra with connected spectrum kills every torsion basis element of a group algebra.

theorem BialgHom.monoidAlgebra_eq_algebraMap_counit {k : Type u} [Field k] {H : Type v} [CommRing H] [HopfAlgebra k H] [IsReduced H] [ConnectedSpace (PrimeSpectrum H)] {M : Type w} [Monoid M] (f : MonoidAlgebra k M →ₐc[k] H) (hM : IsMulTorsion M) : ↑f = (Algebra.ofId k H).comp (Bialgebra.counitAlgHom k (MonoidAlgebra k M))

A bialgebra homomorphism from the group algebra of a torsion group into a reduced Hopf algebra with connected spectrum factors through the counit.