The intertwining-number formula #
Let H and K be subgroups of a finite group G. Frobenius reciprocity moves a pairing of two
induced class functions down to H, and the Mackey decomposition then splits the restriction to
H of the function induced from K into a sum over the double cosets H \ G / K. Applying
Frobenius reciprocity once more, inside H, to each summand gives
⟨Ind_H^G f, Ind_K^G h⟩_G = ∑_{HsK} ⟨{}^s h, f⟩_{H ⊓ sKs⁻¹},
where {}^s h is the conjugate y ↦ h (s⁻¹ y s) of h on the Mackey subgroup and f is
restricted to that same subgroup. The corresponding decomposition of intertwining spaces gives
the intertwining-number formula, over every field,
dim Hom_G(Ind_H^G A, Ind_K^G B) = ∑_{HsK} dim Hom_{H ⊓ sKs⁻¹}(Res A, {}^s B),
the quantitative core of the Mackey irreducibility criterion.
Taking K = H and h = f, the double coset of 1 is the class of every element of H, its
Mackey subgroup is all of H, and its term is the self-pairing ⟨f, f⟩_H. Splitting that term
off is TauCeti.characterPairing_ind_ind_mackey_erase, and
TauCeti.finrank_hom_indFDRep_mackey_erase is the same split for dimensions, where the term
becomes dim End_H A: this is the shape in which the Mackey irreducibility criterion reads the
formula.
A term of the sum is read at a representative s of its double coset, but does not depend on that
choice: replacing s by h₁ s h₂ with h₁ ∈ H and h₂ ∈ K leaves the dimension unchanged
(TauCeti.finrank_hom_res_mackeyToH_mul_left_mul_right).
Main statements #
TauCeti.characterPairing_ind_ind_mackey: the intertwining-number formula for class functions.TauCeti.finrank_hom_indFDRep_mackey: the intertwining-number formula as an identity of intertwining-space dimensions.TauCeti.characterPairing_mackeyClassFunction_of_mem: the term of a double coset meetingHis the self-pairing overH.TauCeti.characterPairing_ind_ind_mackey_erase: the formula forK = H, with the term of the identity double coset split off.TauCeti.finrank_hom_indFDRep_mackey_erase: the same split for intertwining-space dimensions, whose identity-coset term isdim End_H A.TauCeti.finrank_hom_res_mackeyToH_one: the Mackey term at the identity representative has the same dimension as the ordinary intertwining space overH.TauCeti.finrank_hom_res_mackeyToH_of_normal: for normalH, a Mackey term has the same dimension as the ordinary intertwining space fromAto{}^s A.TauCeti.finrank_hom_res_mackeyToH_mul_left_mul_right: a term of the formula does not depend on the representative chosen for its double coset.
Implementation notes #
The formula is proved for class functions first and specialized to characters, exactly as
TauCeti.frobenius_reciprocity_classFunction is: no representation is involved in the class
function form, so it also covers class functions that are not characters.
The character pairing produces an identity in k of the casts of the dimensions, with
Hom_G(Ind_K^G B, Ind_H^G A) on the left. The natural-number formula instead uses
FDRep.indHomMackeyLinearEquiv, preserving the direction of Hom on both sides, and holds over
every field, including when |G| vanishes in k. Its self-intertwining specialization therefore
supplies the dimension formula for the Mackey irreducibility criterion in every characteristic.
The invariance of a single term under a change of representative is also proved by transporting
the intertwining space itself, and holds over any field.
The right-hand argument of each intertwining space is the representation TauCeti.mackeySummand
is induced from, written the way TauCeti.mackeySummand writes it: the restriction of B along
TauCeti.mackeyToH, which is the conjugate {}^s B restricted to the Mackey subgroup
(TauCeti.mackeySummand_eq_indFDRep_res_conjFDRep unfolds it into those two steps).
References #
- J.-P. Serre, Linear Representations of Finite Groups, Chapter 7.3, Proposition 22.
- I. M. Isaacs, Character Theory of Finite Groups, Chapter 5.
The intertwining-number formula for class functions. The pairing over G of a class
function induced from H with one induced from K is the sum, over the double cosets
H \ G / K, of the pairings over the Mackey subgroup H ⊓ sKs⁻¹ of the conjugate {}^s h with
the restriction of f.
The term of a double coset that meets H. When the chosen representative lies in H, the
Mackey subgroup is all of H, conjugating by the representative does not change a class function,
and the term of TauCeti.characterPairing_ind_ind_mackey is the self-pairing ⟨f, f⟩_H.
For K = H this is the term of the identity double coset, the one that
TauCeti.characterPairing_ind_ind_mackey_erase splits off.
The intertwining-number formula with the identity double coset split off. Inducing one
class function f from H to G, the self-pairing of the result is ⟨f, f⟩_H plus the Mackey
terms of the remaining double cosets.
For the character of an irreducible representation over an algebraically closed field the first
summand is 1 (TauCeti.ClassFunction.characterPairing_ofFDRep_self), so the self-pairing of
Ind_H^G f is 1 exactly when the remaining terms sum to zero. That the terms then vanish
one by one is a separate matter: TauCeti.finrank_hom_indFDRep_mackey_erase gives a formula
of natural-number dimensions over every field, where a zero sum forces every summand to vanish.
The character-pairing identity below separately assumes that the group order is invertible in
k; in positive characteristic, vanishing of the sum of dimension casts alone does not imply
vanishing of the dimensions. The natural-number formula underlies the Mackey irreducibility
criterion.
The class function of the source of the Mackey summand -- the representation
TauCeti.mackeySummand is induced from, namely the conjugate {}^s A restricted to the Mackey
subgroup -- is the conjugated class function TauCeti.mackeyClassFunction.
The intertwining-number formula, as an identity in k of the casts of the dimensions of
the intertwining spaces: the dimension of Hom_G(Ind_K^G B, Ind_H^G A) is the sum, over the double
cosets H \ G / K, of the dimensions of Hom_{H ⊓ sKs⁻¹}(Res A, {}^s B).
The characteristic-free natural-number formula
TauCeti.finrank_hom_indFDRep_mackey instead uses Hom_G(Ind_H^G A, Ind_K^G B) on the left.
The intertwining-number formula, over every field:
dim Hom_G(Ind_H^G A, Ind_K^G B) = ∑_{HsK} dim Hom_{H ⊓ sKs⁻¹}(Res A, {}^s B).
Applied with K = H and B = A, the identity double coset contributes dim End_H A, and the
formula is the quantitative core of the Mackey irreducibility criterion.
At the identity representative, the Mackey intertwining space has the same dimension as the ordinary intertwining space over the subgroup.
For a normal subgroup, the dimension of a Mackey intertwining space equals the dimension of
the ordinary intertwining space from A to its conjugate {}^s A.
The Mackey term depends only on the double coset, as a dimension: the intertwining space
Hom_{H ⊓ sKs⁻¹}(Res A, {}^s B) has the same dimension at s and at h₁ s h₂ for h₁ ∈ H and
h₂ ∈ K, which is exactly the change of representative of the double coset HsK.
Nothing is assumed of k beyond being a field: the two intertwining spaces are carried into one
another by the action of h₁ on A and of h₂ on B.
The intertwining-number formula for a single induced representation, over every field and with the identity double coset split off:
dim End_G(Ind_H^G A) = dim End_H A + ∑_{HsH ≠ H} dim Hom_{H ⊓ sHs⁻¹}(Res A, {}^s A).
All the summands are natural numbers, so Ind_H^G A has a one-dimensional endomorphism algebra
exactly when A does and every non-identity double coset contributes nothing.