Complete reducibility descends along scalar extension

Let C be a coalgebra over a field k, let V be a C-comodule, and let A be a nonzero commutative k-algebra. If the base-changed comodule A ⊗[k] V over A ⊗[k] C is completely reducible, then so is V.

Consequently linear reductivity of a coalgebra descends from any field extension. For coordinate Hopf algebras this is the statement that an affine group over k is linearly reductive as soon as it becomes linearly reductive over some extension field; this is how linear reductivity of groups which are only diagonalizable after extension, such as non-split tori, is reached.

Main declarations

• TauCeti.Comodule.IsCompletelyReducible.of_baseChange: complete reducibility of A ⊗[k] V over A ⊗[k] C implies complete reducibility of V over C.
• TauCeti.Coalgebra.IsLinearlyReductive.of_baseChange: linear reductivity of K ⊗[k] C over a field extension K implies linear reductivity of C.

References

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

theorem TauCeti.Comodule.IsCompletelyReducible.of_baseChange {k : Type u} {C : Type v} {V : Type w} (A : Type x) [Field k] [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommMonoid V] [Module k V] [Comodule k C V] [CommRing A] [Algebra k A] [Nontrivial A] (h : IsCompletelyReducible A (TensorProduct k A C) (TensorProduct k A V)) : IsCompletelyReducible k C V

Complete reducibility descends along scalar extension. If A is a nonzero commutative algebra over the field k and the base-changed comodule A ⊗[k] V over A ⊗[k] C is completely reducible, then V is completely reducible over C.

theorem TauCeti.Coalgebra.IsLinearlyReductive.of_baseChange {k : Type u} {C : Type v} (K : Type x) [Field k] [AddCommMonoid C] [Module k C] [Coalgebra k C] [Field K] [Algebra k K] (h : IsLinearlyReductive K (TensorProduct k K C)) : IsLinearlyReductive k C

Linear reductivity descends along field extensions. If the scalar extension K ⊗[k] C of a coalgebra to an extension field K is linearly reductive, then so is C.

Linear reductivity of K ⊗[k] C is only required for carriers in the universe of K, which by TauCeti.Coalgebra.IsLinearlyReductive.isCompletelyReducible covers every universe.