Exactness of invariants for linearly reductive coalgebras

The invariant-vector operation is exact for comodules over a linearly reductive coalgebra with a distinguished element 1. In particular, for a linearly reductive affine group, every invariant vector in a quotient rational representation lifts to an invariant vector. Neither the source nor the target representation needs to be finite dimensional.

The image statement is stronger than preservation of surjections: the image of the invariants under any comodule morphism is the intersection of its image with the target invariants. Together with preservation of injections, this gives exactness on short exact sequences. This is the representation-theoretic input to descent of invariant functions in affine homogeneous spaces.

For a completely reducible source the same lifting, image, surjectivity, and exactness results hold over a commutative ring, provided the coefficient coalgebra is flat. Over a field, local finite dimensionality reduces an arbitrary lift to this case.

References

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

theorem TauCeti.Comodule.Hom.exists_fixed_preimage_of_isCompletelyReducible {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] [One C] [Module.Flat R C] {M : Type w} [AddCommMonoid M] [Module R M] [Comodule R C M] {N : Type x} [AddCommMonoid N] [Module R N] [Comodule R C N] (f : Hom R C M N) (hM : IsCompletelyReducible R C M) {n : N} (hn : n ∈ fixedSubcomodule R C N) (hnrange : n ∈ f.range) : ∃ m ∈ fixedSubcomodule R C M, f m = n

If the source is completely reducible, every invariant vector in the image of a comodule morphism has an invariant preimage. Flatness of the coalgebra suffices over a general ring.

theorem TauCeti.Comodule.Hom.map_fixedSubcomodule_of_isCompletelyReducible {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] [One C] [Module.Flat R C] {M : Type w} [AddCommMonoid M] [Module R M] [Comodule R C M] {N : Type x} [AddCommMonoid N] [Module R N] [Comodule R C N] (f : Hom R C M N) (hM : IsCompletelyReducible R C M) : Submodule.map f.toLinearMap (fixedSubcomodule R C M).toSubmodule = f.range ⊓ (fixedSubcomodule R C N).toSubmodule

Taking invariant vectors commutes with the image of a comodule morphism whose source is completely reducible, over a commutative ring with a flat coefficient coalgebra.

theorem TauCeti.Comodule.Hom.fixedMap_surjective_of_isCompletelyReducible {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] [One C] [Module.Flat R C] {M : Type w} [AddCommMonoid M] [Module R M] [Comodule R C M] {N : Type x} [AddCommMonoid N] [Module R N] [Comodule R C N] (f : Hom R C M N) (hM : IsCompletelyReducible R C M) (hf : Function.Surjective ⇑f) : Function.Surjective ⇑f.fixedMap

A surjective comodule morphism with completely reducible source remains surjective on invariant vectors, over a commutative ring with a flat coefficient coalgebra.

theorem TauCeti.Comodule.Hom.exact_fixedMap_of_isCompletelyReducible {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] [One C] [Module.Flat R C] {M : Type w} [AddCommMonoid M] [Module R M] [Comodule R C M] {N : Type x} [AddCommMonoid N] [Module R N] [Comodule R C N] {P : Type y} [AddCommMonoid P] [Module R P] [Comodule R C P] (f : Hom R C M N) (g : Hom R C N P) (hM : IsCompletelyReducible R C M) (hfg : Function.Exact ⇑f ⇑g) : Function.Exact ⇑f.fixedMap ⇑g.fixedMap

Taking invariants preserves an exact pair of comodule morphisms when the source of the first morphism is completely reducible and the coefficient coalgebra is flat.

theorem TauCeti.Comodule.Hom.exists_fixed_preimage_of_isLinearlyReductive {k : Type u} [Field k] {C : Type v} [AddCommMonoid C] [Module k C] [Coalgebra k C] [One C] {M : Type w} [AddCommMonoid M] [Module k M] [Comodule k C M] {N : Type x} [AddCommMonoid N] [Module k N] [Comodule k C N] (f : Hom k C M N) (hC : Coalgebra.IsLinearlyReductive k C) {n : N} (hn : n ∈ fixedSubcomodule k C N) (hnrange : n ∈ f.range) : ∃ m ∈ fixedSubcomodule k C M, f m = n

In a comodule over a linearly reductive coalgebra, every invariant vector in the image of any comodule morphism has an invariant preimage, with no finiteness assumptions on the modules.

theorem TauCeti.Comodule.Hom.map_fixedSubcomodule_of_isLinearlyReductive {k : Type u} [Field k] {C : Type v} [AddCommMonoid C] [Module k C] [Coalgebra k C] [One C] {M : Type w} [AddCommMonoid M] [Module k M] [Comodule k C M] {N : Type x} [AddCommMonoid N] [Module k N] [Comodule k C N] (f : Hom k C M N) (hC : Coalgebra.IsLinearlyReductive k C) : Submodule.map f.toLinearMap (fixedSubcomodule k C M).toSubmodule = f.range ⊓ (fixedSubcomodule k C N).toSubmodule

Taking invariant vectors commutes with the image of any comodule morphism over a linearly reductive coalgebra.

theorem TauCeti.Comodule.Hom.fixedMap_surjective_of_isLinearlyReductive {k : Type u} [Field k] {C : Type v} [AddCommMonoid C] [Module k C] [Coalgebra k C] [One C] {M : Type w} [AddCommMonoid M] [Module k M] [Comodule k C M] {N : Type x} [AddCommMonoid N] [Module k N] [Comodule k C N] (f : Hom k C M N) (hC : Coalgebra.IsLinearlyReductive k C) (hf : Function.Surjective ⇑f) : Function.Surjective ⇑f.fixedMap

A surjective comodule morphism over a linearly reductive coalgebra remains surjective on invariant vectors, even for infinite-dimensional comodules.

theorem TauCeti.Comodule.Hom.exact_fixedMap_of_isLinearlyReductive {k : Type u} [Field k] {C : Type v} [AddCommMonoid C] [Module k C] [Coalgebra k C] [One C] {M : Type w} [AddCommMonoid M] [Module k M] [Comodule k C M] {N : Type x} [AddCommMonoid N] [Module k N] [Comodule k C N] {P : Type y} [AddCommMonoid P] [Module k P] [Comodule k C P] (f : Hom k C M N) (g : Hom k C N P) (hC : Coalgebra.IsLinearlyReductive k C) (hfg : Function.Exact ⇑f ⇑g) : Function.Exact ⇑f.fixedMap ⇑g.fixedMap

Taking invariants preserves exact pairs of comodule morphisms over a linearly reductive coalgebra. Combined with injectivity and surjectivity of the restricted maps, this preserves short exact sequences of arbitrary rational representations.