Mackey sufficiency over arbitrary fields

Let H be a subgroup of a finite group G whose order is invertible in a field k. If A is a simple representation of H and its nonidentity Mackey intertwining spaces vanish, then its induction to G is simple. No splitting-field hypothesis is needed: the endomorphism algebra of A may be a division algebra larger than k.

The algebra comparison FDRep.indEndAlgEquiv transports Schur's division algebra to the induced object, and Maschke's theorem supplies the converse to Schur's lemma. We give the criterion both on double-coset representatives and on all elements outside the subgroup. For a normal subgroup, the latter condition says that no such element fixes the isomorphism class of A under conjugation.

References

• J.-P. Serre, Linear Representations of Finite Groups, §7.4, Proposition 23.
• I. M. Isaacs, Character Theory of Finite Groups, Chapter 5, Theorem 5.6.
• The algebra comparison FDRep.indEndAlgEquiv and the converse to Schur's lemma CategoryTheory.simple_iff_nontrivial_end_and_isUnit supply the two main steps.

theorem FDRep.simple_indFDRep_of_mackeyDisjoint_doubleCoset {k G : Type u} [Field k] [Group G] [Finite G] {H : Subgroup G} (A : FDRep k ↥H) [CategoryTheory.Simple A] (hG : IsUnit ↑(Nat.card G)) (h : ∀ (D : DoubleCoset.Quotient ↑H ↑H), D ≠ DoubleCoset.mk H H 1 → TauCeti.MackeyDisjoint A (Quotient.out D)) : CategoryTheory.Simple (TauCeti.indFDRep A)

Mackey's sufficient criterion over any field satisfying Maschke's hypothesis: induction of a simple representation is simple if the nonidentity double-coset intertwining spaces vanish.

theorem FDRep.simple_indFDRep_of_forall_mackeyDisjoint {k G : Type u} [Field k] [Group G] [Finite G] {H : Subgroup G} (A : FDRep k ↥H) [CategoryTheory.Simple A] (hG : IsUnit ↑(Nat.card G)) (h : ∀ s ∉ H, TauCeti.MackeyDisjoint A s) : CategoryTheory.Simple (TauCeti.indFDRep A)

Elementwise Mackey sufficiency over an arbitrary field: it is enough to check disjointness at each group element outside the inducing subgroup.

theorem FDRep.simple_indFDRep_of_isEmpty_conjNormalFDRep_iso {k G : Type u} [Field k] [Group G] [Finite G] {H : Subgroup G} [H.Normal] (A : FDRep k ↥H) [CategoryTheory.Simple A] (hG : IsUnit ↑(Nat.card G)) (h : ∀ s ∉ H, IsEmpty (TauCeti.conjNormalFDRep s A ≅ A)) : CategoryTheory.Simple (TauCeti.indFDRep A)

For a normal subgroup, a simple representation with no isomorphic conjugate outside that subgroup induces to a simple representation over any Maschke field.