The fixed subcomodule

Let C be a coalgebra with a distinguished element 1, and let M be a right C-comodule. The vectors v with coact v = v ⊗ 1 form a submodule, and it is a subcomodule because its own coaction already lands in it. For the comodule attached to a representation of an affine group this is the submodule of vectors the group fixes. Comodule morphisms induce linear maps on these invariant vectors; these maps preserve identities, composition, and injectivity. An injective morphism also reflects invariant vectors when the coalgebra is flat.

The consequences of complete reducibility for this subcomodule are proved in TauCeti.Algebra.Coalgebra.Comodule.LinearlyReductive. They show that a linearly reductive unipotent group acts trivially. Exactness on invariant vectors for arbitrary representations is proved in TauCeti.Algebra.Coalgebra.Comodule.LinearlyReductive.Fixed.

Main declarations

• TauCeti.Comodule.fixedSubcomodule: the subcomodule of vectors with coaction v ↦ v ⊗ 1.
• TauCeti.Comodule.mem_fixedSubcomodule and TauCeti.Comodule.fixedSubcomodule_eq_top_iff: its membership and triviality characterizations.
• TauCeti.Comodule.Hom.fixedMap: the induced linear map on invariant vectors.
• TauCeti.Comodule.Hom.mem_fixedSubcomodule_iff_of_injective: reflection of invariance along injective comodule morphisms over a flat coalgebra.

References

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

def TauCeti.Comodule.fixedSubcomodule (R : Type u) (C : Type v) (M : Type w) [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [One C] [AddCommMonoid M] [Module R M] [Comodule R C M] : Subcomodule R C M

The subcomodule of vectors fixed by the coaction: those v with coact v = v ⊗ 1.

For the comodule of a representation of an affine group this is the submodule of invariants.

Equations

• TauCeti.Comodule.fixedSubcomodule R C M = { carrier := TauCeti.Comodule.coact.eqLocus ((TensorProduct.mk R M C).flip 1), coact_mem' := ⋯ }

@[simp]

theorem TauCeti.Comodule.mem_fixedSubcomodule {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [One C] [AddCommMonoid M] [Module R M] [Comodule R C M] {m : M} : m ∈ fixedSubcomodule R C M ↔ coact m = m ⊗ₜ[R] 1

Membership in the fixed subcomodule: m is fixed exactly when coact m = m ⊗ 1.

@[simp]

theorem TauCeti.Comodule.fixedSubcomodule_eq_top_iff {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [One C] [AddCommMonoid M] [Module R M] [Comodule R C M] : fixedSubcomodule R C M = ⊤ ↔ ∀ (m : M), coact m = m ⊗ₜ[R] 1

The fixed subcomodule is everything exactly when the coaction is trivial on every vector.

theorem TauCeti.Comodule.Hom.mem_fixedSubcomodule {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [One C] [AddCommMonoid M] [Module R M] [Comodule R C M] {N : Type u_1} [AddCommMonoid N] [Module R N] [Comodule R C N] (f : Hom R C M N) {m : M} (hm : m ∈ fixedSubcomodule R C M) : f m ∈ fixedSubcomodule R C N

A comodule morphism sends invariant vectors to invariant vectors.

def TauCeti.Comodule.Hom.fixedMap {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [One C] [AddCommMonoid M] [Module R M] [Comodule R C M] {N : Type u_1} [AddCommMonoid N] [Module R N] [Comodule R C N] (f : Hom R C M N) : ↥(fixedSubcomodule R C M) →ₗ[R] ↥(fixedSubcomodule R C N)

The restriction of a comodule morphism to invariant vectors.

Equations

• f.fixedMap = f.restrict ⋯

@[simp]

theorem TauCeti.Comodule.Hom.fixedMap_apply {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [One C] [AddCommMonoid M] [Module R M] [Comodule R C M] {N : Type u_1} [AddCommMonoid N] [Module R N] [Comodule R C N] (f : Hom R C M N) (m : ↥(fixedSubcomodule R C M)) : ↑(f.fixedMap m) = f ↑m

On underlying vectors, the induced map on invariants is the original morphism.

@[simp]

theorem TauCeti.Comodule.Hom.fixedMap_id {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [One C] [AddCommMonoid M] [Module R M] [Comodule R C M] : (id R C M).fixedMap = LinearMap.id

Restricting the identity morphism gives the identity on invariants.

@[simp]

theorem TauCeti.Comodule.Hom.fixedMap_comp {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [One C] [AddCommMonoid M] [Module R M] [Comodule R C M] {N : Type u_1} [AddCommMonoid N] [Module R N] [Comodule R C N] {P : Type u_2} [AddCommMonoid P] [Module R P] [Comodule R C P] (g : Hom R C N P) (f : Hom R C M N) : (g.comp f).fixedMap = g.fixedMap ∘ₗ f.fixedMap

Restriction to invariants respects composition.

theorem TauCeti.Comodule.Hom.fixedMap_injective {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [One C] [AddCommMonoid M] [Module R M] [Comodule R C M] {N : Type u_1} [AddCommMonoid N] [Module R N] [Comodule R C N] (f : Hom R C M N) (hf : Function.Injective ⇑f) : Function.Injective ⇑f.fixedMap

An injective comodule morphism induces an injective map on invariants.

theorem TauCeti.Comodule.Hom.mem_fixedSubcomodule_iff_of_injective {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [One C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] [Module.Flat R C] (f : Hom R C M N) (hf : Function.Injective ⇑f) (m : M) : f m ∈ fixedSubcomodule R C N ↔ m ∈ fixedSubcomodule R C M

An injective comodule morphism reflects invariant vectors when the coalgebra is flat.