The character form of Clifford's theorem

Let N be a normal subgroup of a finite group G, and let W be an irreducible finite-dimensional representation of G over a splitting field. The restriction of W to N has irreducible constituents in one G-orbit, indexed by the left cosets of the inertia group of any constituent V, and every constituent occurs with one common positive multiplicity e. Consequently

W.character n = e * ∑ g in reps, (conjNormalFDRep g V).character n

for a left transversal reps of inertia V.

The orbit, its inertia-coset indexing and the common Hom-space dimension are already provided by TauCeti/RepresentationTheory/Induction/Clifford/Orbit/Basic.lean, TauCeti/RepresentationTheory/Induction/Clifford/Orbit/Index.lean and TauCeti/RepresentationTheory/Induction/Clifford/Multiplicity.lean. This file assembles them using the irreducible-character basis: pairing either side with an irreducible character counts the same constituent, and a transversal contains exactly one representative when it occurs, so the two sides agree by TauCeti.ClassFunction.eq_of_forall_characterPairing_ofCharacter_eq.

Main result

• TauCeti.clifford_restrict_character: Clifford's theorem, character form. It supplies a simple constituent, its positive common multiplicity, a genuine inertia-group transversal, and the restriction-character formula indexed by that transversal.

References

• I. M. Isaacs, Character Theory of Finite Groups, Chapter 6.
• C. W. Curtis and I. Reiner, Representation Theory of Finite Groups and Associative Algebras, §49.

theorem TauCeti.clifford_restrict_character {k : Type u} {G : Type v} [Field k] [Group G] {N : Subgroup G} [N.Normal] [Finite G] [IsAlgClosed k] (hG : IsUnit ↑(Nat.card G)) (W : FDRep k G) [CategoryTheory.Simple W] : ∃ (V : FDRep k ↥N) (_ : CategoryTheory.Simple V) (e : ℕ) (reps : Finset G), e ≠ 0 ∧ (∀ (g : G), ∃! r : G, r ∈ reps ∧ g⁻¹ * r ∈ inertia V) ∧ ∀ (n : ↥N), W.character ↑n = ↑e * ∑ g ∈ reps, (conjNormalFDRep g V).character n

Clifford's theorem, character form. The character of the restriction of an irreducible representation to a normal subgroup is a positive common multiple of the sum of the distinct conjugates of a fixed irreducible constituent, indexed by representatives of the left cosets of its inertia group. The finite set reps is a genuine left transversal for the inertia group: for every g, it contains a unique r with g⁻¹ * r ∈ inertia V.

The hypothesis on Nat.card G is Maschke's condition. Algebraic closure makes k a splitting field, so irreducible characters form an orthonormal basis and their pairings compute multiplicities.