The p-section indicator as a combination of characters

Fix a prime p, a finite group G, and an algebraically closed field k in which |G| is invertible. Brauer's induction theorem, which writes every character of G as an integral combination of characters induced from elementary subgroups, is proved one prime at a time: for each p one needs a function on G with natural-number values, none divisible by p, that is a combination of characters induced from p-elementary subgroups. The coefficients of that combination need not be integers; they lie in any subring A ≤ k containing the required roots of unity. The intended later specialization takes A to be a ring of cyclotomic integers, from which descent to ℤ is a separate step. This file constructs that function.

The building block is the p-section indicator of a p-regular element s (TauCeti.pSectionIndicator), a class function on the p-elementary subgroup H = TauCeti.pElementaryOfSylow s P. On the cyclic group ⟨s⟩ the indicator of s expands as |⟨s⟩|⁻¹ ∑ χ, χ(s⁻¹) χ over the linear characters χ, whose values are roots of unity of order dividing orderOf s; the section indicator is its pullback along the projection TauCeti.pFreePartHom : H →* ⟨s⟩. So orderOf s times the section indicator is an A-combination of characters of H, for every subring A of k containing those roots of unity (TauCeti.orderOf_nsmul_pSectionIndicator_mem_span_virtualCharacters), and inducing it gives an A-combination of virtual characters induced from p-elementary subgroups (TauCeti.orderOf_nsmul_indPSectionIndicator_mem_span_indVirtualCharacters).

Summing these induced functions over the conjugacy classes of p-regular elements s gives the function wanted: at y only the class of the p-free part of y contributes, with a value orderOf s times a count of cosets that is prime to p (TauCeti.exists_mem_span_indVirtualCharacters_isPElementary_not_dvd).

The scaling by orderOf s, rather than by the order of H, is what keeps the values prime to p: expanding the section indicator directly on H would clear a denominator divisible by the p-part of |H|.

Main statements

• TauCeti.pSectionIndicator_eq_comp_pFreePartHom: the p-section indicator is the pullback of the indicator of s along the p-free-part homomorphism.
• TauCeti.orderOf_nsmul_pSectionIndicator_mem_span_virtualCharacters: orderOf s times the p-section indicator is an A-combination of characters of the p-elementary subgroup.
• TauCeti.orderOf_nsmul_indPSectionIndicator_mem_span_indVirtualCharacters: its induction is an A-combination of virtual characters induced from p-elementary subgroups.
• TauCeti.exists_mem_span_indVirtualCharacters_isPElementary_not_dvd: there is a natural-number-valued function with no value divisible by p whose cast is such a combination.

References

• J.-P. Serre, Linear Representations of Finite Groups, Springer GTM 42 (1977), Part II, §10.3, whose construction this follows.
• I. M. Isaacs, Character Theory of Finite Groups, AMS Chelsea (1976), Chapter 8.

The section indicator as a pullback

theorem TauCeti.pSectionIndicator_eq_comp_pFreePartHom {k : Type u} {G : Type v} [Group G] {p : ℕ} [Fact (Nat.Prime p)] {s : G} {P : Sylow p ↥(Subgroup.centralizer {s})} [Zero k] [One k] (hs : ¬p ∣ orderOf s) : pSectionIndicator k s P = Pi.single ⟨s, ⋯⟩ 1 ∘ ⇑(pFreePartHom s P hs)

The p-section indicator is a pullback. It is the indicator of s in the cyclic group ⟨s⟩, pulled back along the p-free-part homomorphism TauCeti.pFreePartHom.

The scaled section indicator as a combination of characters

theorem TauCeti.orderOf_nsmul_pSectionIndicator_mem_span_virtualCharacters {k : Type u} {G : Type v} [Group G] {p : ℕ} [Fact (Nat.Prime p)] {s : G} {P : Sylow p ↥(Subgroup.centralizer {s})} [Field k] [Finite G] [IsAlgClosed k] [Invertible ↑(orderOf s)] (A : Subring k) (hA : ∀ (x : k), x ^ orderOf s = 1 → x ∈ A) (hs : ¬p ∣ orderOf s) : orderOf s • pSectionIndicator k s P ∈ Submodule.span ↥A ↑(virtualCharacters k ↥(pElementaryOfSylow s P))

The p-section indicator, scaled by the order of s, is an A-combination of characters of the p-elementary subgroup, for every subring A of k containing the roots of unity of order dividing orderOf s. On ⟨s⟩ the scaled indicator of s is ∑ χ, χ(s⁻¹) χ over the irreducible characters χ, whose values are such roots of unity, and the section indicator is the pullback of the indicator of s along TauCeti.pFreePartHom.

theorem TauCeti.orderOf_nsmul_indPSectionIndicator_mem_span_indVirtualCharacters {k : Type u} {G : Type v} [Group G] {p : ℕ} [Fact (Nat.Prime p)] {s : G} {P : Sylow p ↥(Subgroup.centralizer {s})} [Field k] [Finite G] [IsAlgClosed k] [Invertible ↑(orderOf s)] (A : Subring k) (hA : ∀ (x : k), x ^ orderOf s = 1 → x ∈ A) (hs : ¬p ∣ orderOf s) : orderOf s • indPSectionIndicator k s P ∈ Submodule.span ↥A ↑(ClassFunction.indVirtualCharacters k G fun (S : Subgroup G) => IsPElementary p ↥S)

The induced p-section indicator, scaled by the order of s, is an A-combination of virtual characters induced from p-elementary subgroups.

A function prime to p everywhere

theorem TauCeti.exists_mem_span_indVirtualCharacters_isPElementary_not_dvd (k : Type u) {G : Type v} [Group G] [Field k] [Finite G] [IsAlgClosed k] [Invertible ↑(Nat.card G)] (p : ℕ) [Fact (Nat.Prime p)] : ∃ (ψ : G → ℕ), (∀ (y : G), ¬p ∣ ψ y) ∧ ∀ (A : Subring k), (∀ (x : k), x ^ Nat.card G = 1 → x ∈ A) → (fun (y : G) => ↑(ψ y)) ∈ Submodule.span ↥A ↑(ClassFunction.indVirtualCharacters k G fun (S : Subgroup G) => IsPElementary p ↥S)

Brauer's local lemma. For every prime p there is a function ψ : G → ℕ, none of whose values is divisible by p, whose cast to k is an A-combination of virtual characters induced from p-elementary subgroups, for every subring A of k containing the |G|-th roots of unity. It is the sum, over the conjugacy classes of p-regular elements s, of orderOf s times the induced p-section indicator of s: at y only the class of the p-free part of y contributes, and its contribution is prime to p.