Grothendieck classes of representations with p-power-order image

Over a field of characteristic p, a representation of a finite group in which every element acts with p-power order has only trivial composition factors. Its class in the exact Grothendieck group is therefore its dimension times the class of the trivial line. The group itself need not be a p-group, and the representation need not split into trivial lines.

The module statement expresses the power-order hypothesis using the group-algebra basis vectors, so it passes directly to submodules and quotients. The representation statement TauCeti.exactK0_asModule_eq_finrank_nsmul_of_forall_pow_eq_one uses powers of the representing endomorphisms instead. These results apply, for example, to permutation representations of quotients of p-power order and allow their induced classes to be computed additively.

The simple-module argument uses the trivial-line theorem for irreducible representations in TauCeti/RepresentationTheory/Unipotent/PowerOrder.lean; finite-length induction supplies the exact-sequence relations for arbitrary modules.

References

• J.-P. Serre, Linear Representations of Finite Groups, Part III, §14.

theorem TauCeti.nonempty_linearEquiv_trivial_of_forall_pow_eq_one {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] (M : Type u_1) [AddCommGroup M] [Module k M] [Module (MonoidAlgebra k G) M] [IsScalarTower k (MonoidAlgebra k G) M] [IsSimpleModule (MonoidAlgebra k G) M] (hM : ∀ (g : G), ∃ (n : ℕ), ∀ (x : M), MonoidAlgebra.single (g ^ p ^ n) 1 • x = x) : Nonempty (M ≃ₗ[MonoidAlgebra k G] (Representation.trivial k G k).asModule)

A simple group-algebra module on which every group element acts with p-power order in characteristic p is isomorphic to the trivial line.

theorem TauCeti.exactK0_of_eq_finrank_smul_of_forall_pow_eq_one {k : Type u} [Field k] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] {G : Type u} [Group G] [Finite G] (M : FGModuleCat (MonoidAlgebra k G)) (hM : ∀ (g : G), ∃ (n : ℕ), ∀ (x : ↑M), MonoidAlgebra.single (g ^ p ^ n) 1 • x = x) : ExactK0.of M = ↑(Module.finrank k ↑M.obj) • ExactK0.of ↧(Representation.trivial k G k).asModule

A finitely generated group-algebra module with p-power-order image in characteristic p has Grothendieck class equal to its dimension times the trivial class. The exponent may depend on the group element; no semisimplicity is assumed.

theorem TauCeti.exactK0_asModule_eq_finrank_nsmul_of_forall_pow_eq_one {k : Type u} [Field k] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] {G : Type u} [Group G] [Finite G] {V : Type u} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρ : Representation k G V) (hρ : ∀ (g : G), ∃ (n : ℕ), ρ g ^ p ^ n = 1) : ExactK0.of ↧ρ.asModule = Module.finrank k V • ExactK0.of ↧(Representation.trivial k G k).asModule

The class of a finite-dimensional representation with p-power-order image in characteristic p is its dimension times the class of the trivial line, including when its trivial composition factors do not split.