The class function induced from a p-elementary subgroup

Fix a prime p, an element s of a finite group G whose order is prime to p, and a Sylow p-subgroup P of the centraliser C_G(s). The subgroup H = TauCeti.pElementaryOfSylow s P generated by s and P is p-elementary, and the p-section of s in H is the set of elements of H whose p-free part is s. Because H centralises s, that set is stable under conjugation in H, so its indicator TauCeti.pSectionIndicator is a class function of H.

This file computes the class function of G induced from that indicator. Its value is the number TauCeti.pSectionCosetCard of left cosets of H that conjugate the argument into the p-section, and that count is

• zero unless the p-free part of the argument is conjugate to s;
• the relative index [C_G(s) : H], which is prime to p, at s itself; and
• congruent to that relative index modulo p at every element whose p-free part is s, because the contributing cosets are the fixed points of the p-element s⁻¹x acting on the cosets of H in C_G(s).

So TauCeti.pSectionCosetCard is prime to p on the whole p-section of s, and the induced class function's value there is the cast of this count into the coefficient semiring. It vanishes off the conjugates of that section. This is the local computation behind Brauer's induction theorem, which writes every character as an integral combination of characters induced from elementary subgroups: one such class function is attached to each p-regular class, and their values modulo p are what an integral combination is assembled from.

Main definitions

• TauCeti.pSectionIndicator: the indicator of the p-section of s in H.
• TauCeti.indPSectionIndicator: the class function of G induced from it.
• TauCeti.pSectionCosetCard: the number of cosets of H contributing to that induced value.

Main statements

• TauCeti.pSectionIndicator_mem_classFunction and TauCeti.indPSectionIndicator_mem_classFunction: both functions are class functions.
• TauCeti.conj_mem_pElementaryOfSylow_and_pFreePart_eq_iff: a conjugate of x lies in the p-section of s exactly when the two factors of x are carried to s and into H.
• TauCeti.indPSectionIndicator_eq_pSectionCosetCard: the induced class function is the coset count, read in the coefficient ring.
• TauCeti.pSectionCosetCard_eq_zero_of_not_isConj and TauCeti.indPSectionIndicator_eq_zero_of_not_isConj: the count vanishes off the conjugates of the p-section.
• TauCeti.pSectionCosetCard_self and TauCeti.indPSectionIndicator_self: at s the count is the relative index of H in C_G(s).
• TauCeti.pSectionCosetCard_modEq: on the p-section of s the count is that relative index modulo p.
• TauCeti.not_dvd_pSectionCosetCard: hence the count is prime to p on the whole p-section, and by conjugation invariance (TauCeti.pSectionCosetCard_conj) on every conjugate of it, TauCeti.not_dvd_pSectionCosetCard_of_isConj.

References

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

The indicator of a p-section and the class function it induces

noncomputable def TauCeti.pSectionIndicator {G : Type v} [Group G] {p : ℕ} (k : Type u) [Zero k] [One k] (s : G) (P : Sylow p ↥(Subgroup.centralizer {s})) : ↥(pElementaryOfSylow s P) → k

The indicator of the p-section of s inside the p-elementary subgroup attached to s and a Sylow p-subgroup P of the centraliser of s: it is 1 on the elements whose p-free part is s, and 0 elsewhere.

@[simp]

theorem TauCeti.pSectionIndicator_apply {k : Type u} {G : Type v} [Group G] {p : ℕ} {s : G} {P : Sylow p ↥(Subgroup.centralizer {s})} [Zero k] [One k] (x : ↥(pElementaryOfSylow s P)) : pSectionIndicator k s P x = if pFreePart p ↑x = s then 1 else 0

The defining case split of TauCeti.pSectionIndicator.

theorem TauCeti.pSectionIndicator_mem_classFunction {k : Type u} {G : Type v} [Group G] {p : ℕ} {s : G} {P : Sylow p ↥(Subgroup.centralizer {s})} [Semiring k] : pSectionIndicator k s P ∈ ClassFunction k ↥(pElementaryOfSylow s P)

The p-section indicator is a class function. Conjugation transports the p-free part, and the p-elementary subgroup centralises s, so conjugating inside it does not move the condition pFreePart p x = s.

noncomputable def TauCeti.indPSectionIndicator {G : Type v} [Group G] {p : ℕ} (k : Type u) [Semiring k] [Finite G] (s : G) (P : Sylow p ↥(Subgroup.centralizer {s})) : G → k

The class function of G induced from the p-section indicator. Its values are computed by TauCeti.indPSectionIndicator_eq_pSectionCosetCard.

theorem TauCeti.nsmul_indPSectionIndicator {k : Type u} {G : Type v} [Group G] {p : ℕ} {s : G} {P : Sylow p ↥(Subgroup.centralizer {s})} [Semiring k] [Finite G] (n : ℕ) : n • indPSectionIndicator k s P = (pElementaryOfSylow s P).indClassFun (n • pSectionIndicator k s P)

Scaling the induced p-section indicator is the induction of the scaled section indicator.

theorem TauCeti.indPSectionIndicator_mem_classFunction {k : Type u} {G : Type v} [Group G] {p : ℕ} {s : G} {P : Sylow p ↥(Subgroup.centralizer {s})} [Semiring k] [Finite G] : indPSectionIndicator k s P ∈ ClassFunction k G

The induced p-section indicator is a class function of G.

The contributing cosets

noncomputable def TauCeti.pSectionCosetCard {G : Type v} [Group G] {p : ℕ} (s : G) (P : Sylow p ↥(Subgroup.centralizer {s})) (x : G) : ℕ

The number of cosets contributing to the induced p-section indicator: those left cosets of the p-elementary subgroup whose representatives conjugate the p-free part of x to s and the p-part of x into the subgroup. By TauCeti.conj_mem_pElementaryOfSylow_and_pFreePart_eq_iff this says exactly that the conjugate of x lies in the p-section of s.

theorem TauCeti.conj_mem_pElementaryOfSylow_and_pFreePart_eq_iff {G : Type v} [Group G] {p : ℕ} {s : G} {P : Sylow p ↥(Subgroup.centralizer {s})} [Fact (Nat.Prime p)] (hs : ¬p ∣ orderOf s) (x g : G) : g⁻¹ * x * g ∈ pElementaryOfSylow s P ∧ pFreePart p (g⁻¹ * x * g) = s ↔ g⁻¹ * pFreePart p x * g = s ∧ g⁻¹ * pPart p x * g ∈ pElementaryOfSylow s P

A conjugate of x lies in the p-section of s exactly when the conjugating element carries the p-free part of x to s and the p-part of x into the subgroup. The two factorisations x = pFreePart · pPart and y = s · pPart y correspond term by term.

theorem TauCeti.indPSectionIndicator_eq_pSectionCosetCard {k : Type u} {G : Type v} [Group G] {p : ℕ} {s : G} {P : Sylow p ↥(Subgroup.centralizer {s})} [Semiring k] [Finite G] [Fact (Nat.Prime p)] (hs : ¬p ∣ orderOf s) (x : G) : indPSectionIndicator k s P x = ↑(pSectionCosetCard s P x)

The induced p-section indicator counts cosets.

Vanishing off the conjugates of the p-section

theorem TauCeti.pSectionCosetCard_eq_zero_of_not_isConj {G : Type v} [Group G] {p : ℕ} {s : G} {P : Sylow p ↥(Subgroup.centralizer {s})} {x : G} (hx : ¬IsConj (pFreePart p x) s) : pSectionCosetCard s P x = 0

The count vanishes unless the p-free part of x is conjugate to s.

theorem TauCeti.indPSectionIndicator_eq_zero_of_not_isConj {k : Type u} {G : Type v} [Group G] {p : ℕ} {s : G} {P : Sylow p ↥(Subgroup.centralizer {s})} [Semiring k] [Finite G] [Fact (Nat.Prime p)] (hs : ¬p ∣ orderOf s) {x : G} (hx : ¬IsConj (pFreePart p x) s) : indPSectionIndicator k s P x = 0

The induced p-section indicator vanishes off the conjugates of the p-section.

The count on the p-section of s

@[simp]

theorem TauCeti.pSectionCosetCard_self {G : Type v} [Group G] {p : ℕ} {s : G} {P : Sylow p ↥(Subgroup.centralizer {s})} [Fact (Nat.Prime p)] (hs : ¬p ∣ orderOf s) : pSectionCosetCard s P s = (pElementaryOfSylow s P).relIndex (Subgroup.centralizer {s})

At s itself the count is the relative index of the p-elementary subgroup in the centraliser of s, which is prime to p by TauCeti.not_dvd_relIndex_pElementaryOfSylow: the p-part of s is trivial, so every coset of the subgroup in the centraliser contributes.

theorem TauCeti.pSectionCosetCard_modEq {G : Type v} [Group G] {p : ℕ} {s : G} {P : Sylow p ↥(Subgroup.centralizer {s})} [Finite G] [Fact (Nat.Prime p)] {x : G} (hx : pFreePart p x = s) : pSectionCosetCard s P x ≡ pSectionCosetCard s P s [MOD p]

The count is constant modulo p along the p-section of s. The contributing cosets are the fixed points of the p-element pPart p x acting by translation on the cosets of the p-elementary subgroup in the centraliser of s, and a p-group has as many fixed points as points modulo p.

theorem TauCeti.not_dvd_pSectionCosetCard {G : Type v} [Group G] {p : ℕ} {s : G} {P : Sylow p ↥(Subgroup.centralizer {s})} [Finite G] [Fact (Nat.Prime p)] {x : G} (hx : pFreePart p x = s) : ¬p ∣ pSectionCosetCard s P x

The count is prime to p everywhere on the p-section of s.

@[simp]

theorem TauCeti.pSectionCosetCard_conj {G : Type v} [Group G] {p : ℕ} {s : G} {P : Sylow p ↥(Subgroup.centralizer {s})} (c x : G) : pSectionCosetCard s P (c * x * c⁻¹) = pSectionCosetCard s P x

The count is a class function of x: left multiplication by the conjugating element gives a bijection between the corresponding sets of contributing cosets.

theorem TauCeti.not_dvd_pSectionCosetCard_of_isConj {G : Type v} [Group G] {p : ℕ} {s : G} {P : Sylow p ↥(Subgroup.centralizer {s})} [Finite G] [Fact (Nat.Prime p)] {x : G} (hx : IsConj (pFreePart p x) s) : ¬p ∣ pSectionCosetCard s P x

The count is prime to p on every conjugate of the p-section of s: the class-function form of TauCeti.not_dvd_pSectionCosetCard.

@[simp]

theorem TauCeti.indPSectionIndicator_self {k : Type u} {G : Type v} [Group G] {p : ℕ} {s : G} {P : Sylow p ↥(Subgroup.centralizer {s})} [Semiring k] [Finite G] [Fact (Nat.Prime p)] (hs : ¬p ∣ orderOf s) : indPSectionIndicator k s P s = ↑((pElementaryOfSylow s P).relIndex (Subgroup.centralizer {s}))

The value of the induced p-section indicator at s.