The additive group is not linearly reductive

Over any field the additive group 𝔾ₐ is unipotent in the strong sense that every nonzero comodule over its coordinate algebra k[x] contains a nonzero fixed vector (TauCeti.AdditiveGroup.exists_ne_zero_coact_eq_tmul_one, Kolchin's theorem for 𝔾ₐ, which needs neither algebraic closedness nor finite-dimensionality). That supply of fixed vectors is exactly what TauCeti.HopfAlgebra.comul_eq_tmul_one_of_isLinearlyReductive_of_forall_exists_fixed asks for, so a linearly reductive 𝔾ₐ would have Δ h = h ⊗ 1, hence h = ε(h) · 1, for every h. The coordinate algebra is a polynomial algebra and its coordinate x has counit 0, so 𝔾ₐ is not linearly reductive over any field.

This is the worked example that gives the triviality theorem content: unipotent groups other than the trivial one exist, so complete reducibility genuinely fails for them.

Main results

• TauCeti.AdditiveGroup.not_isLinearlyReductive: the coordinate algebra of 𝔾ₐ over a field is not linearly reductive.
• TauCeti.AdditiveGroup.not_linearlyReductiveCommHopfAlgProperty_coordinateHopfAlgebra: the same statement for the object property.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, §3.2 and §8.3.
• J. C. Jantzen, Representations of Algebraic Groups, I.2.

theorem TauCeti.AdditiveGroup.not_isLinearlyReductive (k : Type u) [Field k] : ¬Coalgebra.IsLinearlyReductive k (SymmetricAlgebra k k)

The additive group is not linearly reductive, over any field: its coordinate algebra k[x] admits a finite-dimensional representation that is not completely reducible, since otherwise every element of k[x] would be a scalar.

theorem TauCeti.AdditiveGroup.not_linearlyReductiveCommHopfAlgProperty_coordinateHopfAlgebra (k : Type u) [Field k] : ¬linearlyReductiveCommHopfAlgProperty k (coordinateHopfAlgebra k)

The object-property form of TauCeti.AdditiveGroup.not_isLinearlyReductive.