The dimension form of 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 an algebraically closed field. Clifford's theorem describes the restriction of W to N as e copies of each of the [G : inertia V] distinct conjugates of one irreducible constituent V. Counting dimensions turns that description into the identity

dim W = e * [G : inertia V] * dim V,

so in particular the index of the inertia group divides dim W, and so does the dimension of the constituent. That index divides [G : N] as well, because N ≤ inertia V, so the number of distinct conjugates occurring is constrained from two sides at once: by the degree of W and by the index of N, neither constraint mentioning the multiplicity e.

Two special cases follow from that arithmetic. Whenever dim W and [G : N] are coprime the index is 1: the inertia group is everything, there is a single constituent, and the character of W on N is e times that of V. A subgroup of index two and an irreducible of odd dimension are coprime in that sense, which is the case arising for alternatingGroup α ◁ Equiv.Perm α, complementary to the linear-character computation of TauCeti/RepresentationTheory/Induction/Clifford/Alternating/Basic.lean, where the inertia group is as small as Clifford theory allows. And when dim W = 1 the right-hand side of the dimension identity is a product of natural numbers equal to 1, so every factor is 1: a linear character of G restricts to a linear character of N that the whole group fixes.

Main statements

• FDRep.clifford_restrict_finrank: Clifford's theorem, dimension form, packaging the constituent together with its decomposition of Res_N W, the multiplicity and the identity dim W = e * [G : inertia V] * dim V as natural numbers.
• FDRep.clifford_restrict_dvd_finrank: the divisibilities that identity contains, [G : inertia V] ∣ dim W and dim V ∣ dim W, together with [G : inertia V] ∣ [G : N] and the count [G : inertia V] ∣ dim W / (e * dim V) with the multiplicity divided out, stated for a constituent V supplied with its decomposition of Res_N W.
• FDRep.clifford_restrict_inertia_eq_top_of_coprime: when the dimension of W is coprime to [G : N], the restriction of W to N is isomorphic to e copies of a single constituent V whose inertia group is all of G, the character of W on N being e times that of V and dim W = e * dim V.
• FDRep.clifford_restrict_inertia_eq_top_of_finrank_eq_one: a one-dimensional representation of G restricts to a one-dimensional representation of N whose inertia group is all of G, the restriction being a single copy of it.

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 FDRep.clifford_restrict_finrank {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) ∧ Module.finrank k ↑W.V = e * (TauCeti.inertia V).index * Module.finrank k ↑V.V

Clifford's theorem, dimension form. The dimension of an irreducible representation of G is the common multiplicity e of the constituents of its restriction to N, times the number [G : inertia V] of those constituents, times the dimension of one of them.

The decomposition Res_N W ≅ V.cliffordSum e that FDRep.clifford_restrict_iso supplies is returned alongside the identity, so that V is exhibited as a constituent of the restriction and not merely named by it.

In particular the index of the inertia group of a constituent divides the dimension of W; that is the arithmetic that FDRep.clifford_restrict_dvd_finrank reads off and that FDRep.clifford_restrict_inertia_eq_top_of_coprime exploits.

theorem FDRep.clifford_restrict_dvd_finrank {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) ∧ (TauCeti.inertia V).index ∣ Module.finrank k ↑W.V ∧ Module.finrank k ↑V.V ∣ Module.finrank k ↑W.V ∧ (TauCeti.inertia V).index ∣ N.index ∧ (TauCeti.inertia V).index ∣ Module.finrank k ↑W.V / (e * Module.finrank k ↑V.V)

The divisibilities in Clifford's theorem. For an irreducible constituent V of the restriction of an irreducible W to a normal subgroup, both the index of the inertia group of V and the dimension of V divide the dimension of W; the index divides [G : N], and it divides the quotient dim W / (e * dim V) that the dimension identity leaves.

The decomposition Res_N W ≅ V.cliffordSum e is carried along from FDRep.clifford_restrict_finrank, so that V is exhibited as a constituent of the restriction and the divisibilities are read as statements about that constituent rather than about some unrelated irreducible representation of N.

This is the form in which the dimension identity of FDRep.clifford_restrict_finrank is used. The number of distinct conjugates occurring in the restriction is [G : inertia V], and it is constrained from two sides at once: by the degree of W, through the dimension identity, and by the index of N, through TauCeti.le_inertia. Neither constraint mentions the multiplicity e, which the last divisibility divides out instead: dim W / (e * dim V) counts the distinct conjugates.

theorem FDRep.clifford_restrict_inertia_eq_top_of_coprime {k : Type u} {G : Type v} [Field k] [Group G] {N : Subgroup G} [N.Normal] [IsAlgClosed k] (W : FDRep k G) [CategoryTheory.Simple W] (hcop : (Module.finrank k ↑W.V).Coprime N.index) : ∃ (V : FDRep k ↥N) (_ : CategoryTheory.Simple V) (hfinite : Finite (G ⧸ TauCeti.inertia V)), have x := hfinite; ∃ (e : ℕ), e ≠ 0 ∧ TauCeti.inertia V = ⊤ ∧ Nonempty (N.resFDRep W ≅ V.cliffordSum e) ∧ Module.finrank k ↑W.V = e * Module.finrank k ↑V.V ∧ ∀ (n : ↥N), W.character ↑n = ↑e * V.character n

Clifford theory when the dimension is coprime to the index. If the dimension of an irreducible W : FDRep k G is coprime to [G : N], then Res_N W is isomorphic to e copies of a single irreducible constituent V whose inertia group is all of G; consequently the character of W on N is e times that of V, and dim W = e * dim V.

The number of constituents is the index [G : inertia V], which divides [G : N] because N ≤ inertia V, and divides dim W by the dimension identity that FDRep.clifford_restrict_finrank records. Coprimality leaves it no value but 1, so inertia V = ⊤ and V.cliffordSum e has a single conjugate summand.

An irreducible of odd dimension over a subgroup of index two is the instance of this that arises for alternatingGroup α ◁ Equiv.Perm α, complementary to TauCeti.inertia_ofLinearCharacter_alternatingGroup, where a linear character of the alternating group has the smallest inertia group instead.

theorem FDRep.clifford_restrict_inertia_eq_top_of_finrank_eq_one {k : Type u} {G : Type v} [Field k] [Group G] {N : Subgroup G} [N.Normal] [IsAlgClosed k] (W : FDRep k G) [CategoryTheory.Simple W] (hW : Module.finrank k ↑W.V = 1) : ∃ (V : FDRep k ↥N) (_ : CategoryTheory.Simple V) (hfinite : Finite (G ⧸ TauCeti.inertia V)), have x := hfinite; Nonempty (N.resFDRep W ≅ V.cliffordSum 1) ∧ TauCeti.inertia V = ⊤ ∧ Module.finrank k ↑V.V = 1

A linear character restricts to an invariant linear character. If W is one-dimensional, then an irreducible constituent of its restriction to a normal subgroup is one-dimensional and is fixed by the conjugation action of the whole group, its inertia group being all of G.

The right-hand side of the dimension identity of FDRep.clifford_restrict_finrank is a product of natural numbers, so its being 1 forces each of the three factors to be 1. The multiplicity is therefore 1 too, and the decomposition Res_N W ≅ V.cliffordSum 1 exhibiting V as the constituent is returned alongside.