Linear reductivity and injective coalgebra morphisms

Over a field, corestriction along an injective coalgebra morphism does not change the invariant subspaces of a comodule. A linear retraction of the coalgebra morphism recovers the original coaction from its corestriction. Consequently complete reducibility is unchanged by corestriction, and linear reductivity passes from a coalgebra to its subcoalgebras.

For coordinate Hopf algebras, this applies to the injective coordinate morphism of a quotient-group projection. It is the complete-reducibility input for passing linear reductivity to quotients in the characteristic-zero reductive-group comparison.

References

• J. S. Milne, Algebraic Groups (2017), §12.
• M. Sweedler, Hopf Algebras, Chapter 2.

theorem TauCeti.Comodule.isCompletelyReducible_corestrict_iff_of_split {k : Type u} [CommSemiring k] {C : Type v} {D : Type w} [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommMonoid D] [Module k D] [Coalgebra k D] {V : Type x} [AddCommMonoid V] [Module k V] [Comodule k C V] (f : C →ₗc[k] D) (r : D →ₗ[k] C) (hr : r ∘ₗ f.toLinearMap = LinearMap.id) : IsCompletelyReducible k D V ↔ IsCompletelyReducible k C V

Complete reducibility is unchanged by corestriction along a coalgebra morphism with a linear retraction.

theorem TauCeti.Comodule.isCompletelyReducible_corestrict_iff_of_injective {k : Type u} [Field k] {C : Type v} {D : Type w} [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommMonoid D] [Module k D] [Coalgebra k D] {V : Type x} [AddCommMonoid V] [Module k V] [Comodule k C V] (f : C →ₗc[k] D) (hf : Function.Injective ⇑f) : IsCompletelyReducible k D V ↔ IsCompletelyReducible k C V

Complete reducibility is unchanged by corestriction along an injective coalgebra morphism over a field.

theorem TauCeti.Coalgebra.IsLinearlyReductive.of_injective {k : Type u} [Field k] {C : Type v} {D : Type w} [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommMonoid D] [Module k D] [Coalgebra k D] (f : C →ₗc[k] D) (hf : Function.Injective ⇑f) (hD : IsLinearlyReductive k D) : IsLinearlyReductive k C

A subcoalgebra of a linearly reductive coalgebra is linearly reductive.