An induced representation from a trivially meeting conjugate is never irreducible

The Mackey irreducibility criterion TauCeti.simple_indFDRep_iff asks the restrictions of A and of its conjugate {}^s A to the Mackey subgroup H ⊓ sHs⁻¹ to be disjoint for every s ∉ H. This file records the extreme case in which that condition fails as badly as possible: if the Mackey subgroup is trivial, then the two restrictions are representations of the trivial group on the same space, so the identity is an intertwiner between them, and it is nonzero unless A is a zero object; disjointness then fails outright. Consequently an induced representation fails to be irreducible as soon as some conjugate of the subgroup meets it trivially, whatever the representation being induced -- no nonzeroness need be assumed there, because an irreducible induced representation already forces the inducing representation to be irreducible, hence nonzero.

The condition is not exotic. A subgroup of prime order either equals a conjugate of itself or meets it trivially, there being nothing in between, so TauCeti.exists_notMem_mackeySubgroup_eq_bot_of_prime_card_of_not_normal turns non-normality of such a subgroup into the hypothesis above: nothing induced from a non-normal subgroup of prime order is irreducible. That is the mechanism behind the S₃ example, where the two-element subgroup generated by a transposition is not normal and nothing induced from it is irreducible; see TauCeti.RepresentationTheory.Induction.Mackey.SymmetricThree.Basic.

The dichotomy the last paragraph rests on is a statement about subgroups alone, so it lives with the rest of the Mackey subgroup theory in TauCeti.RepresentationTheory.Induction.Mackey.Subgroup; what is added here is the passage from it to representations.

The hypothesis constrains only the subgroup, so the conclusion is uniform in the representation induced. That is what distinguishes the two halves of the S₃ example: inducing from the non-normal C₂ of S₃ can never give an irreducible, whatever is induced, while inducing from the normal A₃ can.

Main statements

• TauCeti.not_mackeyDisjoint_of_mackeySubgroup_eq_bot: a trivial Mackey subgroup destroys disjointness for every representation that is not a zero object.
• TauCeti.not_simple_indFDRep_of_mackeySubgroup_eq_bot: consequently the induced representation is not irreducible.
• TauCeti.not_simple_indFDRep_of_prime_card_of_not_normal: nothing induced from a non-normal subgroup of prime order is irreducible.

References

• J.-P. Serre, Linear Representations of Finite Groups, Chapter 7.4, Proposition 23.
• I. M. Isaacs, Character Theory of Finite Groups, Chapter 5, Corollary 5.7.

theorem TauCeti.not_mackeyDisjoint_of_mackeySubgroup_eq_bot {k G : Type u} [Field k] [Group G] {H : Subgroup G} {A : FDRep k ↥H} {s : G} (hbot : mackeySubgroup s H H = ⊥) (hA : ¬CategoryTheory.Limits.IsZero A) : ¬MackeyDisjoint A s

A trivial Mackey subgroup destroys Mackey disjointness. Both restrictions appearing in TauCeti.MackeyDisjoint are then representations of the trivial group on the module underlying A, so the identity is an intertwiner between them; it is nonzero unless A is a zero object.

The only condition on A is that it not be a zero object; the rest of the hypothesis mentions only the subgroup.

theorem TauCeti.not_simple_indFDRep_of_mackeySubgroup_eq_bot {k G : Type u} [Field k] [Group G] {H : Subgroup G} [Finite G] [IsAlgClosed k] [CharZero k] {A : FDRep k ↥H} {s : G} (hs : s ∉ H) (hbot : mackeySubgroup s H H = ⊥) : ¬CategoryTheory.Simple (indFDRep A)

An induced representation is not irreducible as soon as some conjugate of the subgroup meets it trivially. Read off TauCeti.simple_indFDRep_iff at the element s, whose Mackey term TauCeti.not_mackeyDisjoint_of_mackeySubgroup_eq_bot shows cannot vanish. The criterion also returns simplicity of A, which supplies the nonzeroness that lemma needs, so this holds for every A whatsoever.

theorem TauCeti.not_simple_indFDRep_of_prime_card_of_not_normal {k G : Type u} [Field k] [Group G] [Finite G] [IsAlgClosed k] [CharZero k] {H : Subgroup G} (hp : Nat.Prime (Nat.card ↥H)) (hH : ¬H.Normal) {A : FDRep k ↥H} : ¬CategoryTheory.Simple (indFDRep A)

Nothing induced from a non-normal subgroup of prime order is irreducible. Such a subgroup meets one of its conjugates trivially (TauCeti.exists_notMem_mackeySubgroup_eq_bot_of_prime_card_of_not_normal), and that alone refutes the Mackey criterion.

Both hypotheses are needed: over a normal subgroup the Mackey subgroup is always H, and without prime order the intersection with a conjugate can be a proper nontrivial subgroup, in which case irreducibility depends on the representation.