The Mackey criterion over splitting fields

For a finite group over a field whose characteristic does not divide the group order, Mackey disjointness is sufficient for induction of a simple representation to be simple. It is necessary when the induced simple object has a one-dimensional endomorphism space. Thus scalar Schur for simple representations of the ambient group gives the iff criterion, without algebraic closure or characteristic zero. No splitting hypothesis on the subgroup is required.

The necessity proof uses the natural-number intertwining formula, not its cast into the coefficient field. Consequently it also works in positive characteristic. The sufficient direction is the arbitrary-field division-algebra criterion in Mackey.Sufficient.

Algebraic closure supplies scalar Schur, yielding the corollaries TauCeti.simple_indFDRep_iff_doubleCoset, TauCeti.simple_indFDRep_iff and TauCeti.simple_indFDRep_iff_of_normal. They require only [NeZero (Nat.card G : k)], not characteristic zero, and are used by the reducibility and Clifford-theory applications.

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.

theorem FDRep.simple_indFDRep_iff_doubleCoset_of_scalarSchur {k G : Type u} [Field k] [Group G] [Finite G] {H : Subgroup G} (A : FDRep k ↥H) (hG : IsUnit ↑(Nat.card G)) (hSplitG : ∀ (W : FDRep k G), CategoryTheory.Simple W → Module.finrank k (W ⟶ W) = 1) : CategoryTheory.Simple (TauCeti.indFDRep A) ↔ CategoryTheory.Simple A ∧ ∀ (D : DoubleCoset.Quotient ↑H ↑H), D ≠ DoubleCoset.mk H H 1 → TauCeti.MackeyDisjoint A (Quotient.out D)

Mackey's iff criterion with scalar Schur imposed only on simple representations of the ambient group. It is valid over non-algebraically-closed splitting fields and in every characteristic in which the group order is invertible.

theorem FDRep.simple_indFDRep_iff_of_scalarSchur {k G : Type u} [Field k] [Group G] [Finite G] {H : Subgroup G} (A : FDRep k ↥H) (hG : IsUnit ↑(Nat.card G)) (hSplitG : ∀ (W : FDRep k G), CategoryTheory.Simple W → Module.finrank k (W ⟶ W) = 1) : CategoryTheory.Simple (TauCeti.indFDRep A) ↔ CategoryTheory.Simple A ∧ ∀ s ∉ H, TauCeti.MackeyDisjoint A s

The splitting-field Mackey criterion checked on all elements outside the subgroup, rather than on chosen double-coset representatives.

theorem FDRep.simple_indFDRep_iff_of_normal_of_scalarSchur {k G : Type u} [Field k] [Group G] [Finite G] {H : Subgroup G} [H.Normal] (A : FDRep k ↥H) (hG : IsUnit ↑(Nat.card G)) (hSplitG : ∀ (W : FDRep k G), CategoryTheory.Simple W → Module.finrank k (W ⟶ W) = 1) : CategoryTheory.Simple (TauCeti.indFDRep A) ↔ CategoryTheory.Simple A ∧ ∀ s ∉ H, IsEmpty (TauCeti.conjNormalFDRep s A ≅ A)

For a normal subgroup over a splitting field, simplicity of induction is equivalent to simplicity of the original representation and absence of isomorphic conjugates outside the subgroup. No scalar-Schur hypothesis on the subgroup is needed.

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

The Mackey irreducibility criterion. The representation induced from A is irreducible exactly when A is irreducible and every double coset HsH other than H itself, read at its chosen representative, is Mackey disjoint. Algebraic closure supplies scalar Schur.

theorem TauCeti.simple_indFDRep_iff {k G : Type u} [Field k] [Group G] [Finite G] [IsAlgClosed k] [NeZero ↑(Nat.card G)] {H : Subgroup G} (A : FDRep k ↥H) : CategoryTheory.Simple (indFDRep A) ↔ CategoryTheory.Simple A ∧ ∀ s ∉ H, MackeyDisjoint A s

The Mackey irreducibility criterion, elementwise. The disjointness condition of TauCeti.simple_indFDRep_iff_doubleCoset may equally be asked of every element s ∉ H rather than of one chosen representative of every nonidentity double coset.

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

The Mackey irreducibility criterion for a normal subgroup. If H ◁ G, then the representation induced from A is irreducible exactly when A is irreducible and none of its conjugates {}^s A, for s ∉ H, is isomorphic to A.