Linear reductivity of diagonalizable group schemes

Every finite-type diagonalizable group scheme over a field is linearly reductive. On the canonical object D(G) = Spec k[G], this follows from complete reducibility of comodules over a monoid-algebra coalgebra. Isomorphism invariance then extends the result to the full diagonalizable-group-scheme property.

Main declarations

• TauCeti.DiagonalizableGroup.linearlyReductiveAffineGroupSchemeProperty_groupScheme: the canonical diagonalizable group scheme D(G) is linearly reductive.
• linearlyReductiveAffineGroupSchemeProperty_of_diagonalizableGroupSchemeProperty: every affine group scheme satisfying the diagonalizable property is linearly reductive.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, Section 3.2.
• J. S. Milne, Algebraic Groups (2017), Theorem 12.12.

This is the diagonalizable-group example for the complete-reducibility characterization in Layer 6 of the ReductiveGroups roadmap.

theorem TauCeti.DiagonalizableGroup.linearlyReductiveAffineGroupSchemeProperty_groupScheme (k : Type u) [Field k] (G : FGCommGrpCat) : linearlyReductiveAffineGroupSchemeProperty k { obj := groupScheme k G, property := ⋯ }

The canonical finite-type diagonalizable group scheme D(G) is linearly reductive.

theorem TauCeti.DiagonalizableGroup.linearlyReductiveAffineGroupSchemeProperty_of_diagonalizableGroupSchemeProperty (k : Type u) [Field k] (G : AffineGroupSchemeCat ↧k) (hG : diagonalizableGroupSchemeProperty k G.obj) : linearlyReductiveAffineGroupSchemeProperty k G

Every affine group scheme satisfying the finite-type diagonalizable-group property is linearly reductive.