The representation decomposition in Clifford's theorem

Let N be a normal subgroup of a group G, and let W be an irreducible finite-dimensional representation of G over a splitting field. The isotypic components of the restriction of W to N are indexed by the inertia cosets of any one constituent V, and every component is a power of its constituent with one common positive exponent e. Combining these two statements gives the classical decomposition

Res_N W ≅ ⨁ (g : G / inertia V), e · {}^g V.

The quotient index is preferable to a chosen transversal: Quotient.out g supplies the conjugate representative, while changing that representative changes the summand only up to isomorphism.

Main definitions

• FDRep.cliffordSum: the finite sum of e copies of the conjugate of V attached to every inertia coset.

Main properties

• FDRep.finrank_cliffordSum and FDRep.character_cliffordSum: its dimension and character.

Main result

• FDRep.clifford_restrict_iso_of_isAtom: Clifford's theorem for a specified constituent.
• FDRep.clifford_restrict_iso: Clifford's theorem, representation form. It supplies a simple constituent, finiteness of its inertia quotient, a positive common multiplicity, and an isomorphism from the restriction to cliffordSum.

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.

noncomputable def FDRep.cliffordSum {k : Type u} {G : Type v} [Field k] [Group G] {N : Subgroup G} [N.Normal] (V : FDRep k ↥N) [Finite (G ⧸ TauCeti.inertia V)] (e : ℕ) : FDRep k ↥N

The finite sum of e copies of every conjugate of V indexed by the left cosets of its inertia group. A finite product of modules is their direct sum; FDRep.ofShrink only returns its possibly larger carrier to the universe in which FDRep k N lives.

@[simp]

theorem FDRep.finrank_cliffordSum {k : Type u} {G : Type v} [Field k] [Group G] {N : Subgroup G} [N.Normal] (V : FDRep k ↥N) [Finite (G ⧸ TauCeti.inertia V)] (e : ℕ) : Module.finrank k ↑(V.cliffordSum e).V = Nat.card (G ⧸ TauCeti.inertia V) * e * Module.finrank k ↑V.V

The dimension of V.cliffordSum e is the number of inertia cosets times e times the dimension of V.

@[simp]

theorem FDRep.character_cliffordSum {k : Type u} {G : Type v} [Field k] [Group G] {N : Subgroup G} [N.Normal] (V : FDRep k ↥N) [Finite (G ⧸ TauCeti.inertia V)] (e : ℕ) (x : ↥N) : (V.cliffordSum e).character x = ↑e * ∑ᶠ (q : G ⧸ TauCeti.inertia V), (TauCeti.conjNormalFDRep (Quotient.out q) V).character x

The character of V.cliffordSum e is e times the sum of the characters of its conjugate summands.

theorem FDRep.clifford_restrict_iso_of_isAtom {k : Type u} {G : Type v} [Field k] [Group G] {N : Subgroup G} [N.Normal] [IsAlgClosed k] (W : FDRep k G) [CategoryTheory.Simple W] (σ : Subrepresentation (W.ρ.comp N.subtype)) (hσ : IsAtom σ) : ∃ (hfinite : Finite (G ⧸ TauCeti.inertia (of σ.toRepresentation))), have x := hfinite; ∃ (e : ℕ), e ≠ 0 ∧ Nonempty (N.resFDRep W ≅ (of σ.toRepresentation).cliffordSum e)

Clifford's theorem for a specified constituent. Given a simple constituent σ of the restriction of an irreducible representation to a normal subgroup, the restriction is isomorphic to e copies of every conjugate of σ, with the distinct conjugates indexed by the left cosets of its inertia group.

Algebraic closure makes k a splitting field, so the Hom-space dimension in the multiplicity theorem is the actual number of copies. Finite dimensionality makes the set of isotypic components, and hence the inertia quotient indexing the sum, finite.

theorem FDRep.clifford_restrict_iso {k : Type u} {G : Type v} [Field k] [Group G] {N : Subgroup G} [N.Normal] [IsAlgClosed k] (W : FDRep k G) [CategoryTheory.Simple W] : ∃ (V : FDRep k ↥N) (_ : CategoryTheory.Simple V) (hfinite : Finite (G ⧸ TauCeti.inertia V)), have x := hfinite; ∃ (e : ℕ), e ≠ 0 ∧ Nonempty (N.resFDRep W ≅ V.cliffordSum e)

Clifford's theorem, representation form. The restriction of an irreducible representation to a normal subgroup is isomorphic to e copies of every conjugate of one simple constituent, with the distinct conjugates indexed by the left cosets of its inertia group.

Algebraic closure makes k a splitting field, so the Hom-space dimension in the multiplicity theorem is the actual number of copies. The conclusion includes the finite inertia quotient that indexes the sum.