Linear reductivity and split exact sequences

A finite-dimensional comodule is completely reducible if and only if every monomorphism into it splits. Consequently a coalgebra is linearly reductive if and only if every short exact sequence of finite-dimensional comodules splits. For coordinate Hopf algebras, this identifies the invariant-complement definition of linear reductivity with its categorical formulation in the rational representation category.

No Hopf algebra structure or finite-dimensionality of the coalgebra is required. The monomorphism criterion and the middle-term splitting theorem hold more generally for finite comodules over a flat coalgebra over a Noetherian commutative ring.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, Section 3.2.

theorem TauCeti.FGComoduleCat.isCompletelyReducible_iff_forall_isSplitMono {k : Type u} [CommRing k] {C : Type v} [AddCommMonoid C] [Module k C] [Coalgebra k C] [IsNoetherianRing k] [Module.Flat k C] (M : FGComoduleCat k C) : Comodule.IsCompletelyReducible k C ↑M ↔ ∀ (N : FGComoduleCat k C) (f : N ⟶ M), CategoryTheory.Mono f → CategoryTheory.IsSplitMono f

A finite comodule over a flat coalgebra over a Noetherian ring is completely reducible exactly when every monomorphism into it admits a retraction.

theorem CategoryTheory.ShortComplex.nonempty_splitting_of_isCompletelyReducible {k : Type u} [CommRing k] {C : Type v} [AddCommMonoid C] [Module k C] [Coalgebra k C] [IsNoetherianRing k] [Module.Flat k C] (S : ShortComplex (TauCeti.FGComoduleCat k C)) (hS : S.ShortExact) (hM : TauCeti.Comodule.IsCompletelyReducible k C ↑S.X₂) : Nonempty S.Splitting

A short exact sequence with completely reducible middle comodule splits.

theorem TauCeti.Coalgebra.isLinearlyReductive_iff_forall_nonempty_splitting {k : Type u} [Field k] {C : Type v} [AddCommMonoid C] [Module k C] [Coalgebra k C] : IsLinearlyReductive k C ↔ ∀ (S : CategoryTheory.ShortComplex (FGComoduleCat k C)), S.ShortExact → Nonempty S.Splitting

Linear reductivity is equivalent to splitting every short exact sequence of finite-dimensional comodules. It suffices to test comodules in the base field’s universe.