Documentation

TauCeti.RepresentationTheory.Induction.ExceptionalCharacter

The exceptional character attached to a trivial-intersection subgroup #

Let H be a trivial-intersection subgroup of a finite group G (TauCeti.IsTISubgroup): one meeting each of its distinct conjugates trivially, as a Frobenius complement does. Induction from such an H is an isometry on the class functions that vanish at the identity (TauCeti.characterPairing_ind_ind, whose support form is TauCeti.isometry_ind_of_isTISet), but it does not send characters to characters: Ind_H^G φ has degree |G : H| · φ(1), not φ(1). The classical repair is to induce not φ but φ corrected by a multiple of the trivial character, and to add that multiple back on G:

φ* = Ind_H^G (φ - φ(1) · 1_H) + φ(1) · 1_G.

This file builds that class function, TauCeti.ClassFunction.indExtend H φ, as a k-linear map in φ, and proves what makes it useful. It has the same degree (TauCeti.ClassFunction.indExtend_apply_one) and restricts back to φ (TauCeti.ClassFunction.comap_subtype_indExtend); and the assignment φ ↦ φ* preserves the character pairing (TauCeti.ClassFunction.characterPairing_indExtend_indExtend), so it carries a norm-1 virtual character of H to a norm-1 virtual character of G. Over an algebraically closed field of characteristic zero in which |G| is invertible, a norm-1 virtual character is ± an irreducible character, and the degree pins down the sign: φ* is an irreducible character of G (TauCeti.ClassFunction.indExtend_mem_irreducibleCharacters). Restriction inverts the assignment, so φ ↦ φ* is injective (TauCeti.ClassFunction.indExtend_injective), and Irr(H) embeds into Irr(G) with Res_H φ* = φ.

That embedding is the exceptional-character correspondence, the step at which the character-theoretic proof of Frobenius's theorem produces the irreducible characters of G whose common kernel is the Frobenius kernel. Nothing here asserts that the kernel is a subgroup; that uses the family of these characters and is a separate target.

Why the correction term is needed #

Two properties of φ* are in tension, and the correction is exactly what reconciles them. The pairing is preserved only for class functions vanishing at the identity — Ind is an isometry there, and Ind 1_H has norm #(H \ G / H), not 1 — while a character of G must take the value φ(1) at the identity, and Ind φ takes |G : H| · φ(1). Subtracting φ(1) · 1_H before inducing buys the first, and adding φ(1) · 1_G afterwards buys the second, without disturbing the first: the trivial character of G is itself the extension of the trivial character of H, and the cross terms cancel. This is why TauCeti.ClassFunction.characterPairing_indExtend_indExtend is an identity of pairings on the nose, with no error term.

Main definitions #

Main results #

Implementation notes #

TauCeti.ClassFunction.indExtend is bundled as a k-linear map, matching Subgroup.indClassFunction: the value at the identity is a linear functional of φ, so the correction is linear in φ too, and the pairing identity then says exactly that the map is an isometry for TauCeti.ClassFunction.characterPairing. Because the definition is not exposed, TauCeti.ClassFunction.indExtend_def records the defining formula for consumers.

The trivial character is spelled TauCeti.ClassFunction.ofCharacter (Representation.trivial k _ k), as elsewhere in this directory, rather than as a bundled constant function; the private lemmas comap_subtype_ofCharacter_trivial and characterPairing_ofCharacter_trivial_self are what the proofs need of it, and neither belongs in this file's interface.

TauCeti.ClassFunction.indExtend_mem_virtualCharacters carries the hypothesis that φ(1) is the image of an integer. That is not decoration: the correction term is the scalar multiple φ(1) · 1_G, which lies in the virtual-character lattice — an additive subgroup, not a k-submodule — only for an integral scalar. For a virtual character φ over an algebraically closed field the degree is automatically integral, and TauCeti.ClassFunction.indExtend_mem_irreducibleCharacters discharges the hypothesis with the degree of an irreducible character.

References #

source
noncomputable def TauCeti.ClassFunction.indExtend {k : Type u} {G : Type v} [Field k] [Group G] (H : Subgroup G) [H.FiniteIndex] :
↥(ClassFunction k ↥H) →ₗ[k] ↥(ClassFunction k G)

The exceptional extension φ* of a class function φ of a subgroup H: induce φ corrected by φ(1) times the trivial character of H, then add φ(1) times the trivial character of G.

The corrected class function vanishes at the identity, which is what makes induction from a trivial-intersection subgroup an isometry on it; adding the multiple of the trivial character of G back restores the degree, φ*(1) = φ(1).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem TauCeti.ClassFunction.indExtend_def {k : Type u} {G : Type v} [Field k] [Group G] {H : Subgroup G} [H.FiniteIndex] (φ : ↥(ClassFunction k ↥H)) :
    (indExtend H) φ = H.indClassFunction (φ - ↑φ 1 • ofCharacter (Representation.trivial k (↥H) k)) + ↑φ 1 • ofCharacter (Representation.trivial k G k)

    The defining formula of the exceptional extension. The definition itself is not exposed, so this is what a consumer unfolds it with.

    source
    @[simp]
    theorem TauCeti.ClassFunction.indExtend_ofCharacter_trivial {k : Type u} {G : Type v} [Field k] [Group G] {H : Subgroup G} [H.FiniteIndex] :
    (indExtend H) (ofCharacter (Representation.trivial k (↥H) k)) = ofCharacter (Representation.trivial k G k)

    The exceptional extension of the trivial character is the trivial character.

    Here the correction cancels the induction outright, 1_H - 1_H = 0, so nothing is induced and the whole value is the correction term on G. No hypothesis on H is needed, and the normalization this records is what makes the extension an extension rather than an arbitrary repair.

    source
    @[simp]
    theorem TauCeti.ClassFunction.indExtend_apply_one {k : Type u} {G : Type v} [Field k] [Group G] {H : Subgroup G} [H.FiniteIndex] (φ : ↥(ClassFunction k ↥H)) :
    ↑((indExtend H) φ) 1 = ↑φ 1

    The exceptional extension has the same degree as the class function it came from.

    The correction term is what makes this work: φ - φ(1) · 1_H vanishes at the identity, so its induction does too, and the value at the identity is the correction term alone.

    source
    theorem TauCeti.ClassFunction.comap_subtype_indExtend {k : Type u} {G : Type v} [Field k] [Group G] {H : Subgroup G} [Finite G] (hH : IsTISubgroup H) (hk : IsUnit ↑(Nat.card ↥H)) (φ : ↥(ClassFunction k ↥H)) :
    (comap H.subtype) ((indExtend H) φ) = φ

    The exceptional extension restricts back to the class function it came from, for a trivial-intersection subgroup whose order is invertible in k.

    The correction term is what makes this work: φ - φ(1) · 1_H vanishes at the identity, so restriction undoes its induction (Subgroup.comap_subtype_indClassFunction_eq_self), and the trivial character of G restricts to that of H, returning the term that was subtracted.

    source
    theorem TauCeti.ClassFunction.indExtend_injective {k : Type u} {G : Type v} [Field k] [Group G] {H : Subgroup G} [Finite G] (hH : IsTISubgroup H) (hk : IsUnit ↑(Nat.card ↥H)) :
    Function.Injective ⇑(indExtend H)

    Distinct class functions have distinct exceptional extensions, restriction being a left inverse of the extension.

    source
    theorem TauCeti.ClassFunction.characterPairing_indExtend_indExtend {k : Type u} {G : Type v} [Field k] [Group G] {H : Subgroup G} [Fintype G] (hG : IsUnit ↑(Nat.card G)) (hH : IsTISubgroup H) (φ ψ : ↥(ClassFunction k ↥H)) :
    (characterPairing ((indExtend H) φ)) ((indExtend H) ψ) = (characterPairing φ) ψ

    The exceptional extension preserves the character pairing, for a trivial-intersection subgroup of a finite group whose order is invertible in k.

    Both the induction isometry and the correction term are used, and the point is that the correction costs nothing. Writing θ = φ - φ(1) · 1_H, induction is an isometry on θ because θ vanishes at the identity; the cross terms ⟨Ind θ, 1_G⟩ collapse to ⟨θ, 1_H⟩ by Frobenius reciprocity, because the trivial character of G restricts to that of H; and 1_G has norm 1. Expanding, every occurrence of φ(1) and ψ(1) cancels.

    source
    theorem TauCeti.ClassFunction.indExtend_mem_virtualCharacters {k : Type u} {G : Type v} [Field k] [Group G] {H : Subgroup G} [Finite G] {φ : ↥(ClassFunction k ↥H)} {n : ℤ} (hφ : ↑φ ∈ virtualCharacters k ↥H) (hn : ↑φ 1 = ↑n) :
    ↑((indExtend H) φ) ∈ virtualCharacters k G

    The exceptional extension of a virtual character of integral degree is a virtual character.

    Both summands are accounted for: induction preserves the virtual-character lattice, and the correction terms are integer multiples of the trivial character, which is the character of the trivial representation. Integrality of φ(1) is what makes those multiples lie in the lattice, which is an additive subgroup and not a k-submodule.

    source
    theorem TauCeti.ClassFunction.indExtend_mem_irreducibleCharacters {k : Type u} {G : Type v} [Field k] [Group G] {H : Subgroup G} [Finite G] [IsAlgClosed k] [CharZero k] [Invertible ↑(Nat.card G)] (hH : IsTISubgroup H) {φ : ↥(ClassFunction k ↥H)} (hφ : ↑φ ∈ irreducibleCharacters k ↥H) :
    ↑((indExtend H) φ) ∈ irreducibleCharacters k G

    The exceptional extension of an irreducible character of a trivial-intersection subgroup is an irreducible character of the whole group.

    This is the exceptional-character correspondence: over an algebraically closed field of characteristic zero in which |G| is invertible, φ ↦ φ* sends Irr(H) into Irr(G), injectively by TauCeti.ClassFunction.indExtend_injective, and with Res_H φ* = φ by TauCeti.ClassFunction.comap_subtype_indExtend.

    The proof is the norm-1 test. The extension is a virtual character of norm 1 whose value at the identity is the degree of φ, a natural number, so it is an irreducible character (TauCeti.mem_irreducibleCharacters_of_characterPairing_self_eq_one).