Invariants of a representation whose elements have p-power order in characteristic p

Over a semiring k of characteristic p, a representation ρ of a finite monoid on a nonzero module, in which every ρ g has order a power of p, always has a nonzero fixed vector: Representation.exists_ne_zero_apply_eq_self_of_forall_pow_eq_one. No finiteness or dimension hypothesis on the module is needed, and k may be infinite or noncommutative. Over a commutative ring, Representation.invariants_ne_bot_of_forall_pow_eq_one states this for a group using the invariant submodule. Over a field and for a group this is the modular counterpart of Representation.IsIrreducible.invariants_eq_bot, which says that a nontrivial irreducible representation has no nonzero invariant vector; together they say that such a representation is irreducible only if it is the trivial representation on a line. Equivalently: over a field of characteristic p, the trivial module is the only irreducible module of a finite p-group. That corollary is Representation.IsIrreducible.eq_trivial_of_forall_pow_expChar_pow_eq_one in TauCeti/RepresentationTheory/Unipotent/PowerOrder.lean, stated for a finite-dimensional representation of any group; an irreducible representation of a finite group is finite-dimensional (Mathlib's instance on ρ.asModule, read back on V along ρ.asModuleEquiv).

A finite normal p-subgroup of an arbitrary group acts trivially on every irreducible representation in characteristic p: its nonzero invariant subspace is stable under the whole group and must be the entire representation. This reduces the classification of simple representations to the quotient by such a subgroup.

The fixed-vector statements assume the acting monoid is finite. For an infinite group, the analogous statement is Kolchin's theorem, which fixes a vector of a finite-dimensional vector space under a group of unipotent operators. The normal-subgroup corollary here requires finiteness only of the subgroup.

Main results

• Representation.exists_ne_zero_apply_eq_self_of_forall_pow_eq_one: a representation of a finite monoid over a semiring of characteristic p, whose elements act with p-power order, has a nonzero fixed vector, with Representation.invariants_ne_bot_of_forall_pow_eq_one its invariant-submodule form over a commutative ring.
• Representation.IsIrreducible.comp_eq_trivial_of_isPGroup: a finite normal p-subgroup acts trivially on an irreducible representation in characteristic p.

References

The statement is classical: over a field of characteristic p the group algebra of a finite p-group is a local ring, so the trivial module is its only irreducible module. Textbook accounts are in J. L. Alperin, Local Representation Theory, Cambridge University Press (1986), and P. Webb, A Course in Finite Group Representation Theory, Cambridge University Press (2016).

theorem Representation.exists_ne_zero_apply_eq_self_of_forall_pow_eq_one {k : Type u} {G : Type v} {V : Type w} [Semiring k] [Monoid G] [AddCommMonoid V] [Module k V] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] [Finite G] [Nontrivial V] (ρ : Representation k G V) (hρ : ∀ (g : G), ∃ (n : ℕ), ρ g ^ p ^ n = 1) : ∃ (v : V), v ≠ 0 ∧ ∀ (g : G), (ρ g) v = v

A representation of a finite monoid in which every element acts with p-power order, over a semiring of characteristic p, has a nonzero fixed vector. Neither finite generation nor finite dimensionality of the module is assumed, and k may be infinite or noncommutative.

theorem Representation.invariants_ne_bot_of_forall_pow_eq_one {k : Type u} {G : Type v} {V : Type w} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] [Finite G] [Nontrivial V] (ρ : Representation k G V) (hρ : ∀ (g : G), ∃ (n : ℕ), ρ g ^ p ^ n = 1) : ρ.invariants ≠ ⊥

The invariant-submodule form of Representation.exists_ne_zero_apply_eq_self_of_forall_pow_eq_one over a commutative ring: a representation of a finite group acting with p-power orders in characteristic p has a nonzero invariant vector. No finiteness hypothesis on the module is assumed.

theorem Representation.IsIrreducible.comp_eq_trivial_of_isPGroup {k : Type u} {G : Type v} {V : Type w} [Field k] [Group G] [AddCommGroup V] [Module k V] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] {ρ : Representation k G V} (hρ : ρ.IsIrreducible) (N : Subgroup G) [N.Normal] [Finite ↥N] (hN : IsPGroup p ↥N) : MonoidHom.comp ρ N.subtype = trivial k (↥N) V

A finite normal p-subgroup acts trivially on every irreducible representation in characteristic p. The ambient group and the representation need not be finite.