Frobenius reciprocity as a character identity

For a finite-index subgroup S of a group G, Mathlib's adjunction Rep.indResAdjunction identifies Hom_G(Ind_S^G A, B) with Hom_S(A, Res_S B). This file transports that adjunction to finite-dimensional representations and reads it off as an identity of character scalar products:

⟨Ind χ, ψ⟩_G = ⟨χ, Res ψ⟩_S,

together with the identity in the other direction ⟨Res ψ, χ⟩_S = ⟨ψ, Ind χ⟩_G.

The same identity holds for arbitrary class functions, with Subgroup.indClassFun in place of the induced character and TauCeti.ClassFunction.comap in place of restriction. That version is proved here too, but by a double count over G × G rather than by the adjunction: no representation is involved, so it also covers class functions that are not characters.

Main statements

• TauCeti.finrank_hom_indFDRep, TauCeti.finrank_hom_resFDRep: the paired intertwining spaces have the same dimension.
• TauCeti.frobenius_reciprocity and TauCeti.frobenius_reciprocity_resFDRep: the character form in both directions, with all scalar products written out as explicit normalized sums.
• TauCeti.characterPairing_indFDRep, TauCeti.characterPairing_resFDRep: the same two identities phrased against TauCeti.ClassFunction.characterPairing.
• TauCeti.card_inv_mul_sum_character_indFDRep: reciprocity against the trivial representation, which says that induction does not change the (normalized) average of a character.
• TauCeti.frobenius_reciprocity_classFunction and TauCeti.characterPairing_ind: the class function form, ⟨Ind f, h⟩_G = ⟨f, Res h⟩_S, for arbitrary class functions f on S and h on G. TauCeti.frobenius_reciprocity is its special case for two characters and follows directly from the representation-theoretic reciprocity isomorphism.

Implementation notes

Only the coefficient field and the invertibility of Nat.card G are assumed; no algebraic closure is needed, because each side is computed by TauCeti.ClassFunction.characterPairing_ofFDRep_eq_finrank rather than by orthogonality of irreducible characters. Invertibility of Nat.card S is not a separate hypothesis: it follows from Subgroup.card_mul_index, via TauCeti.isUnit_natCard_subgroup.

That pairing-to-dimension lemma computes ⟨χ_V, χ_W⟩ as finrank k (W ⟶ V), exchanging the two arguments. So the identity stated in the order ⟨Ind χ, ψ⟩ = ⟨χ, Res ψ⟩ is read off the second reciprocity, finrank_hom_resFDRep. The identity in the order ⟨Res ψ, χ⟩ = ⟨ψ, Ind χ⟩ is then just that one with both sides flipped, by TauCeti.ClassFunction.characterPairing_symm, so it is derived rather than proved again from finrank_hom_indFDRep. Neither direction needs a reindexing of the sums.

The two k-linear equivalences of intertwining spaces that carry the reciprocities are private: only their finrank corollaries are intended as API, and both are opaque transports whose bodies would have to be exposed before a consumer could identify the transported intertwiner.

References

• J.-P. Serre, Linear Representations of Finite Groups, Chapter 7.2.
• I. M. Isaacs, Character Theory of Finite Groups, Lemma 5.2.

theorem TauCeti.finrank_hom_indFDRep {k G : Type u} [Field k] [Group G] {S : Subgroup G} [S.FiniteIndex] (A : FDRep k ↥S) (B : FDRep k G) : Module.finrank k (indFDRep A ⟶ B) = Module.finrank k (A ⟶ S.resFDRep B)

The intertwining space out of an induced representation has the same dimension as the intertwining space into the corresponding restriction. This is the quantitative content of Frobenius reciprocity, and holds over an arbitrary field.

theorem TauCeti.finrank_hom_resFDRep {k G : Type u} [Field k] [Group G] {S : Subgroup G} [S.FiniteIndex] (A : FDRep k ↥S) (B : FDRep k G) : Module.finrank k (S.resFDRep B ⟶ A) = Module.finrank k (B ⟶ indFDRep A)

The dimension form of the second reciprocity.

theorem TauCeti.frobenius_reciprocity {k G : Type u} [Field k] [Group G] {S : Subgroup G} [Fintype G] (hG : IsUnit ↑(Nat.card G)) (A : FDRep k ↥S) (B : FDRep k G) : (↑(Nat.card G))⁻¹ * ∑ g : G, (indFDRep A).character g * B.character g⁻¹ = (↑(Nat.card ↥S))⁻¹ * ∑ s : ↥S, A.character s * B.character (↑s)⁻¹

Frobenius reciprocity as a character identity. The scalar product over G of an induced character with a character of G equals the scalar product over S of the original character with the restricted character.

Both sides are written as explicit normalized sums, so the statement does not depend on the name of any particular pairing; TauCeti.characterPairing_indFDRep is the same identity phrased against TauCeti.ClassFunction.characterPairing. The hypothesis hG is what makes the normalizing factors meaningful; it also supplies the invertibility of Nat.card S.

theorem TauCeti.characterPairing_indFDRep {k G : Type u} [Field k] [Group G] {S : Subgroup G} [Fintype G] (hG : IsUnit ↑(Nat.card G)) (A : FDRep k ↥S) (B : FDRep k G) : (ClassFunction.characterPairing (ClassFunction.ofFDRep (indFDRep A))) (ClassFunction.ofFDRep B) = (ClassFunction.characterPairing (ClassFunction.ofFDRep A)) (ClassFunction.ofFDRep (S.resFDRep B))

Frobenius reciprocity, phrased against the normalized pairing of class functions used by the character-theory development.

theorem TauCeti.characterPairing_resFDRep {k G : Type u} [Field k] [Group G] {S : Subgroup G} [Fintype G] (hG : IsUnit ↑(Nat.card G)) (A : FDRep k ↥S) (B : FDRep k G) : (ClassFunction.characterPairing (ClassFunction.ofFDRep (S.resFDRep B))) (ClassFunction.ofFDRep A) = (ClassFunction.characterPairing (ClassFunction.ofFDRep B)) (ClassFunction.ofFDRep (indFDRep A))

The reciprocity in the other direction, phrased against TauCeti.ClassFunction.characterPairing. The pairing is symmetric, so this is characterPairing_indFDRep with both sides flipped.

theorem TauCeti.frobenius_reciprocity_resFDRep {k G : Type u} [Field k] [Group G] {S : Subgroup G} [Fintype G] (hG : IsUnit ↑(Nat.card G)) (A : FDRep k ↥S) (B : FDRep k G) : (↑(Nat.card ↥S))⁻¹ * ∑ s : ↥S, B.character ↑s * A.character s⁻¹ = (↑(Nat.card G))⁻¹ * ∑ g : G, B.character g * (indFDRep A).character g⁻¹

Frobenius reciprocity in the other direction: the scalar product over S of a restricted character with a character of S equals the scalar product over G of the original character with the induced character. This is characterPairing_resFDRep with the pairing unfolded.

theorem TauCeti.card_inv_mul_sum_character_indFDRep {k G : Type u} [Field k] [Group G] {S : Subgroup G} [Fintype G] (hG : IsUnit ↑(Nat.card G)) (A : FDRep k ↥S) : (↑(Nat.card G))⁻¹ * ∑ g : G, (indFDRep A).character g = (↑(Nat.card ↥S))⁻¹ * ∑ s : ↥S, A.character s

Reciprocity against the trivial representation: the normalized average of an induced character over G is the normalized average of the original character over S. Equivalently, by FDRep.average_char_eq_finrank_invariants, inducing does not change the dimension of the space of invariants.

Both steps of the double count are cleared-denominator identities, so they need only a semiring. The underlying group-sum formula Subgroup.natCard_nsmul_indClassFun needs only additive coefficients. Only the normalized statements below divide and need a field.

theorem TauCeti.frobenius_reciprocity_classFunction {k : Type u} {G : Type v} [Group G] {S : Subgroup G} [Field k] [Fintype G] (hG : IsUnit ↑(Nat.card G)) (f : ↥(ClassFunction k ↥S)) (h : ↥(ClassFunction k G)) : (↑(Nat.card G))⁻¹ * ∑ g : G, S.indClassFun (↑f) g * ↑h g⁻¹ = (↑(Nat.card ↥S))⁻¹ * ∑ s : ↥S, ↑f s * ↑h (↑s)⁻¹

Frobenius reciprocity for class functions. The normalized pairing over G of an induced class function with a class function of G is the normalized pairing over S of the original class function with the restricted one.

Both sides are written as explicit normalized sums, so the statement does not depend on the name of any particular pairing; TauCeti.characterPairing_ind is the same identity phrased against TauCeti.ClassFunction.characterPairing. Specialized to two characters this is TauCeti.frobenius_reciprocity, but no representation is involved here: the identity is a double count over G × G and holds for arbitrary class functions.

theorem TauCeti.characterPairing_ind {k : Type u} {G : Type v} [Group G] {S : Subgroup G} [Field k] [Fintype G] (hG : IsUnit ↑(Nat.card G)) (f : ↥(ClassFunction k ↥S)) (h : ↥(ClassFunction k G)) : (ClassFunction.characterPairing (S.indClassFunction f)) h = (ClassFunction.characterPairing f) ((ClassFunction.comap S.subtype) h)

Frobenius reciprocity for class functions, phrased against the normalized pairing TauCeti.ClassFunction.characterPairing.