Maschke's theorem for intertwining maps

Mathlib states Maschke's theorem for modules over the group algebra: over a field in which the order of the finite group G is invertible, a k[G]-linear injection has a k[G]-linear left inverse (MonoidAlgebra.exists_leftInverse_of_injective). This file reads that statement through Mathlib's dictionary Representation.IntertwiningMap.equivLinearMapAsModule between intertwining maps and k[G]-linear maps of the attached modules, so that it applies to representations as they are usually given, without passing to Representation.asModule. It also gives a splitting of every short exact sequence in Rep k G and FDRep k G, the categorical form used to compare split and exact Grothendieck rings.

The form recorded here is the one used to compare the two meanings of "a constituent of ρ": an irreducible σ that embeds in ρ is also a quotient of ρ, because the embedding splits.

Main statements

• Representation.IntertwiningMap.exists_leftInverse_of_injective: an injective intertwining map has an intertwining left inverse.
• TauCeti.Rep.nonempty_splitting_of_shortExact: a short exact sequence in Rep splits.
• TauCeti.FDRep.nonempty_splitting_of_shortExact: a short exact sequence in FDRep splits.
• Representation.finrank_intertwiningMap_comm: intertwining-space dimension is symmetric for finite-dimensional representations.

References

• J.-P. Serre, Linear Representations of Finite Groups, Springer GTM 42 (1977), Chapter 1.

theorem Representation.IntertwiningMap.exists_leftInverse_of_injective {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Field k] [Group G] [Finite G] [NeZero ↑(Nat.card G)] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] {ρ : Representation k G V} {σ : Representation k G W} (f : ρ.IntertwiningMap σ) (hf : Function.Injective ⇑f) : ∃ (p : σ.IntertwiningMap ρ), p.comp f = id ρ

Maschke's theorem for intertwining maps. Over a field in which the order of the finite group G is invertible, an injective intertwining map f : ρ → σ has an intertwining left inverse p : σ → ρ, that is, p ∘ f = id.

theorem Representation.finrank_intertwiningMap_comm {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Field k] [Group G] [Finite G] [NeZero ↑(Nat.card G)] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] [FiniteDimensional k V] [FiniteDimensional k W] (ρ : Representation k G V) (σ : Representation k G W) : Module.finrank k (ρ.IntertwiningMap σ) = Module.finrank k (σ.IntertwiningMap ρ)

When the finite group order is invertible, the spaces of intertwining maps in the two directions between finite-dimensional representations have equal dimension.

theorem TauCeti.Rep.nonempty_splitting_of_shortExact {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [NeZero ↑(Nat.card G)] {S : CategoryTheory.ShortComplex (Rep k G)} (hS : S.ShortExact) : Nonempty S.Splitting

Every short exact sequence of representations splits when the group order is invertible in the coefficient field.

theorem TauCeti.FDRep.nonempty_splitting_of_shortExact {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [NeZero ↑(Nat.card G)] {S : CategoryTheory.ShortComplex (FDRep k G)} (hS : S.ShortExact) : Nonempty S.Splitting

Every short exact sequence of finite-dimensional representations splits when the group order is invertible in the coefficient field.