Inducing a linear character from a normal subgroup

Let N be a normal subgroup of a finite group G and let χ : N →* kˣ be a linear character, carried by the one-dimensional representation FDRep.ofLinearCharacter χ. The Mackey irreducibility criterion for a normal subgroup, TauCeti.simple_indFDRep_iff_of_normal, asks that the representation be irreducible -- automatic here, a line having no proper nonzero subrepresentation -- and that no conjugate {}^s (χ) for s ∉ N be isomorphic to χ. On a line that second condition is an identity in N →* kˣ, because a one-dimensional representation is determined by the scalar it acts by: FDRep.nonempty_iso_ofLinearCharacter_iff. The criterion therefore becomes elementary group theory: Ind_N^G χ is irreducible exactly when no element outside N stabilizes χ, that is, when for every s ∉ N there is an x ∈ N with χ (s x s⁻¹) ≠ χ x.

A subgroup of index two inverted by conjugation -- the rotation subgroup of a dihedral or of a generalized quaternion group -- makes the condition uniform in s: conjugation sends χ to χ⁻¹ for every s ∉ N, so the criterion collapses to χ ≠ χ⁻¹, that some value of χ fails to square to 1. This is TauCeti.simple_indFDRep_ofLinearCharacter_iff_of_conj_eq_inv, and the inversion need only be checked on a single element outside N.

When χ is moreover faithful the condition loses all reference to χ: χ (s x s⁻¹) ≠ χ x becomes s x s⁻¹ ≠ x, so the induced representation is irreducible exactly when the centralizer of N in G is contained in N. This is the form the classical examples are checked in -- A₃ ◁ S₃ in TauCeti.RepresentationTheory.Induction.Mackey.SymmetricThree.Basic, and the rotation subgroup of a dihedral group -- where the ambient group is visibly nonabelian on N.

The whole file is the normal-subgroup half of the roadmap's dichotomy: nothing induced from the non-normal point stabilizer of S₃ is irreducible (TauCeti.not_simple_indFDRep_stabilizer_perm_fin_three), while a faithful character of the normal subgroup A₃ does induce irreducibly.

Main statements

• TauCeti.conjNormalFDRep_ofLinearCharacter: conjugating a one-dimensional representation conjugates its linear character, as an equality of objects.
• TauCeti.simple_indFDRep_ofLinearCharacter_iff: the Mackey criterion for an induced linear character -- Ind_N^G χ is irreducible exactly when no element outside N stabilizes χ.
• TauCeti.simple_indFDRep_ofLinearCharacter_iff_of_conj_eq_inv: for an inverted subgroup of index two, exactly when some value of χ is not a square root of 1.
• TauCeti.simple_indFDRep_ofLinearCharacter_iff_centralizer_le: for a faithful χ, exactly when C_G(N) ≤ N.

References

The Layer 4 "normal-subgroup corollary" of the induction and restriction roadmap, read on a linear character, as its "Mackey on a small group" and "D₄ dihedral induction" worked examples require.

• J.-P. Serre, Linear Representations of Finite Groups, Chapter 7.4, Proposition 23 and its corollary for a normal subgroup.

@[simp]

theorem TauCeti.conjNormalFDRep_ofLinearCharacter {k G : Type u} [CommRing k] [Group G] {N : Subgroup G} [N.Normal] (g : G) (χ : ↥N →* kˣ) : conjNormalFDRep g (FDRep.ofLinearCharacter χ) = FDRep.ofLinearCharacter (χ.comp (MulEquiv.toMonoidHom (MulAut.conjNormal g⁻¹)))

Conjugating a one-dimensional representation conjugates its linear character. Both sides are the line k with x : N acting by the scalar χ (g⁻¹ x g), so this is an equality of objects of FDRep k N, not merely an isomorphism.

theorem TauCeti.nonempty_iso_conjNormalFDRep_ofLinearCharacter_iff {k G : Type u} [CommRing k] [Group G] {N : Subgroup G} [N.Normal] (g : G) (χ : ↥N →* kˣ) : Nonempty (conjNormalFDRep g (FDRep.ofLinearCharacter χ) ≅ FDRep.ofLinearCharacter χ) ↔ ∀ (x : ↥N), χ ((MulAut.conjNormal g⁻¹) x) = χ x

A conjugate of a one-dimensional representation is isomorphic to it exactly when the conjugated linear character is the same one. There is no room for anything but an equality of scalars: a line is determined by the character it carries.

Not a simp lemma: with conjNormalFDRep_ofLinearCharacter tagged, simp already rewrites this left-hand side to χ.comp ↑(MulAut.conjNormal g)⁻¹ = χ through FDRep.nonempty_iso_ofLinearCharacter_iff, so tagging it too is a simpNF violation. This is the pointwise spelling of that same condition.

theorem TauCeti.simple_indFDRep_ofLinearCharacter_iff {k G : Type u} [Field k] [Group G] {N : Subgroup G} [N.Normal] [Finite G] [IsAlgClosed k] [NeZero ↑(Nat.card G)] (χ : ↥N →* kˣ) : CategoryTheory.Simple (indFDRep (FDRep.ofLinearCharacter χ)) ↔ ∀ s ∉ N, ∃ (x : ↥N), χ ((MulAut.conjNormal s) x) ≠ χ x

The Mackey irreducibility criterion for an induced linear character. For a normal subgroup N ◁ G and a linear character χ : N →* kˣ, the induced representation Ind_N^G χ is irreducible exactly when no element of G outside N stabilizes χ: for every s ∉ N some x ∈ N has χ (s x s⁻¹) ≠ χ x.

The irreducibility of χ itself, which the general criterion also asks for, is automatic: a line has no proper nonzero subrepresentation.

theorem TauCeti.simple_indFDRep_ofLinearCharacter_iff_of_conj_eq_inv {k G : Type u} [Field k] [Group G] {N : Subgroup G} [Finite G] [IsAlgClosed k] [NeZero ↑(Nat.card G)] (hindex : N.index = 2) {s : G} (hs : s ∉ N) (hinv : ∀ x ∈ N, s * x * s⁻¹ = x⁻¹) (χ : ↥N →* kˣ) : CategoryTheory.Simple (indFDRep (FDRep.ofLinearCharacter χ)) ↔ ∃ (x : ↥N), χ x ^ 2 ≠ 1

The Mackey criterion for a linear character of an inverted subgroup of index two: the induced representation is irreducible exactly when some value of χ is not a square root of 1. Conjugation by any element outside N inverts it, by TauCeti.conj_eq_inv_of_notMem_of_index_two, so {}^s χ = χ⁻¹ for every such s and the criterion becomes the single condition χ ≠ χ⁻¹. The inversion hypothesis is asked of the one outside element s only.

theorem TauCeti.simple_indFDRep_ofLinearCharacter_iff_centralizer_le {k G : Type u} [Field k] [Group G] {N : Subgroup G} [N.Normal] [Finite G] [IsAlgClosed k] [NeZero ↑(Nat.card G)] {χ : ↥N →* kˣ} (hχ : Function.Injective ⇑χ) : CategoryTheory.Simple (indFDRep (FDRep.ofLinearCharacter χ)) ↔ Subgroup.centralizer ↑N ≤ N

A faithful linear character of a normal subgroup induces irreducibly exactly when the centralizer of that subgroup is no bigger than the subgroup. Faithfulness turns the Mackey condition χ (s x s⁻¹) ≠ χ x into s x s⁻¹ ≠ x, so all reference to χ disappears and only the position of N inside G is left.