Brauer's induction theorem

For a finite group G over an algebraically closed field of characteristic zero, every virtual character is an integral combination of characters induced from elementary subgroups. In the canonical lattice API this says

indVirtualCharacters k G (fun E ↦ IsElementary E) = virtualCharacters k G.

The local input is TauCeti.exists_mem_span_indVirtualCharacters_isPElementary_not_dvd. For a prime p it supplies a natural-number-valued function ψ, none of whose values is divisible by p, in the cyclotomic span of the characters induced from p-elementary subgroups. If S is the finite set of values of ψ, then

∏ n in S, (n - ψ) = 0.

The induced-character span is closed under multiplication. Expanding the product therefore puts the constant ∏ n in S, n in that span, and this constant is prime to p. The prime-by-prime criterion from TauCeti.RepresentationTheory.Induction.Ideal then gives the integral theorem.

Main results

• TauCeti.ClassFunction.indVirtualCharacters_eq_virtualCharacters_isElementary: Brauer's induction theorem, in virtual-character lattice form.
• TauCeti.ClassFunction.character_mem_indCharacterSpanInt_isElementary: Brauer's induction theorem, in character-level form.
• TauCeti.ClassFunction.indVirtualCharacterDirectSumAddHom_isElementary_surjective: the direct sum of induction maps from elementary subgroups is surjective.

References

• J.-P. Serre, Linear Representations of Finite Groups, Springer GTM 42 (1977), Part II, Section 10.3, Theorem 18.
• I. M. Isaacs, Character Theory of Finite Groups, AMS Chelsea (1976), Chapter 8.

theorem TauCeti.ClassFunction.indVirtualCharacters_eq_virtualCharacters_isElementary {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [CharZero k] [IsAlgClosed k] : (indVirtualCharacters k G fun (E : Subgroup G) => IsElementary ↥E) = virtualCharacters k G

Brauer's induction theorem. Over an algebraically closed field of characteristic zero, every virtual character of a finite group is an integral combination of virtual characters induced from elementary subgroups.

theorem TauCeti.ClassFunction.character_mem_indCharacterSpanInt_isElementary {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [CharZero k] [IsAlgClosed k] (V : FDRep k G) : V.character ∈ indCharacterSpanInt k G fun (E : Subgroup G) => IsElementary ↥E

Brauer's induction theorem, character form. Every character is an integral combination of characters induced from irreducible characters of elementary subgroups.

theorem TauCeti.ClassFunction.indVirtualCharacterDirectSumAddHom_isElementary_surjective {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [CharZero k] [IsAlgClosed k] : Function.Surjective ⇑(indVirtualCharacterDirectSumAddHom k G fun (E : Subgroup G) => IsElementary ↥E)

The direct sum of induction maps from elementary subgroups is surjective. This is the direct-sum formulation of TauCeti.ClassFunction.indVirtualCharacters_eq_virtualCharacters_isElementary.