Morphisms from connected affine groups to finite constant groups

Let H be the coordinate Hopf algebra of a connected affine group over a field k, and let G be a finite group. Every group-scheme morphism from Spec H to the constant group scheme attached to G is trivial. Contravariantly, every bialgebra morphism

  k^G ⟶ H

is the composite of the counit of k^G and the unit of H.

The proof uses the characteristic functions of the elements of G. Their images are idempotents in H, hence are zero or one because Spec H is connected. Compatibility with the counit determines which alternative occurs: the characteristic function of the identity maps to one, and all the others map to zero. The same computation shows that the induced map on points has constant value the identity.

This is the connectedness input in the Lie--Kolchin induction. The derived subgroup first produces finitely many weight spaces permuted by the ambient group; the result here makes the resulting morphism to that finite permutation group trivial. In that application geometric connectedness supplies connectedness of the coordinate ring after extension to an algebraic closure.

Main declarations

• TauCeti.ConstantGroup.bialgHom_eq_unit_comp_counit_of_connected: a morphism from a connected affine group to a finite constant group is trivial in Hopf coordinates.
• TauCeti.ConstantGroup.point_comp_eq_one_of_connected: the induced map on algebra-valued points is constantly the identity.

References

• J. S. Milne, Algebraic Groups (2017), Proposition 1.34 and Chapter 2.
• T. A. Springer, Linear Algebraic Groups, Theorem 6.3.1.

This advances the "Lie--Kolchin; solvable groups" milestone in Layer 5 of the ReductiveGroups roadmap.

theorem TauCeti.ConstantGroup.bialgHom_eq_unit_comp_counit_of_connected {k : Type u} [Field k] {H : Type v} [CommRing H] [Bialgebra k H] (G : Type w) [Group G] [Finite G] (hconnected : ConnectedSpace (PrimeSpectrum H)) (f : coordinateRing k G →ₐc[k] H) : f = (Bialgebra.unitBialgHom k H).comp (Bialgebra.counitBialgHom k (coordinateRing k G))

Every morphism from a connected affine group to a finite constant group is trivial.

In coordinate Hopf algebras, a morphism to the constant group attached to G is a bialgebra homomorphism from its function algebra to H. It is necessarily the counit followed by the unit.

theorem TauCeti.ConstantGroup.point_comp_eq_one_of_connected {k : Type u} [Field k] {H : Type v} [CommRing H] [Bialgebra k H] (G : Type w) [Group G] [Finite G] (hconnected : ConnectedSpace (PrimeSpectrum H)) (f : coordinateRing k G →ₐc[k] H) {A : Type u_1} [CommRing A] [Algebra k A] (p : H →ₐ[k] A) : WithConv.toConv (p.comp ↑f) = 1

A connected affine group's map to a finite constant group sends every algebra-valued point to the identity.