Applications of Maschke's theorem

This proves some properties of representations that follow from Maschke's theorem.

We prove that, if G is a finite group whose order is invertible in a field k, then every object of Rep k G (resp. FDRep k G) is injective and projective.

We also give two simpleness criteria for an object V of FDRep k G, when k is an algebraically closed field in which the order of G is invertible:

• FDRep.simple_iff_end_is_rank_one: V is simple if and only V ⟶ V is a k-vector space of dimension 1.
• FDRep.simple_iff_char_is_norm_one: when k is characteristic zero, V is simple if and only if ∑ g : G, V.character g * V.character g⁻¹ = Fintype.card G.

instance Rep.instInjective {k : Type u} [Field k] {G : Type u} [Finite G] [Group G] [NeZero ↑(Nat.card G)] (V : Rep k G) : CategoryTheory.Injective V

If G is finite and its order is nonzero in the field k, then every object of Rep k G is injective.

instance Rep.instProjective {k : Type u} [Field k] {G : Type u} [Finite G] [Group G] [NeZero ↑(Nat.card G)] (V : Rep k G) : CategoryTheory.Projective V

If G is finite and its order is nonzero in the field k, then every object of Rep k G is projective.

instance FDRep.instInjectiveOfNeZeroCastCard {k : Type u} [Field k] {G : Type u} [Finite G] [Group G] [NeZero ↑(Nat.card G)] (V : FDRep k G) : CategoryTheory.Injective V

If G is finite and its order is nonzero in the field k, then every object of FDRep k G is injective.

instance FDRep.instProjectiveOfNeZeroCastCard {k : Type u} [Field k] {G : Type u} [Finite G] [Group G] [NeZero ↑(Nat.card G)] (V : FDRep k G) : CategoryTheory.Projective V

If G is finite and its order is nonzero in the field k, then every object of FDRep k G is projective.

theorem FDRep.simple_iff_end_is_rank_one {k : Type u} [Field k] {G : Type u} [Finite G] [Group G] [IsAlgClosed k] [NeZero ↑(Nat.card G)] (V : FDRep k G) : CategoryTheory.Simple V ↔ Module.finrank k (V ⟶ V) = 1

If G is finite and its order is nonzero in an algebraically closed field k, then an object of FDRep k G is simple if and only if its space of endomorphisms is a k-vector space of dimension 1.

theorem FDRep.simple_iff_char_is_norm_one {k : Type u} [Field k] {G : Type u} [Group G] [IsAlgClosed k] [CharZero k] [Fintype G] (V : FDRep k G) : CategoryTheory.Simple V ↔ ∑ g : G, V.character g * V.character g⁻¹ = ↑(Nat.card G)

If G is finite and k an algebraically closed field of characteristic 0, then an object of FDRep k G is simple if and only if its character has norm 1.