Induction from a trivial-intersection subgroup

Let H be a trivial-intersection subgroup of a finite group G: one meeting each of its distinct conjugates trivially (TauCeti.IsTISubgroup). A class function on H that vanishes at the identity then induces to G without changing its values on H, and therefore without changing its norm, as long as the relevant group order is invertible in the coefficient field k. This allows cancellation in the group-sum identity and normalization of the character pairing. Concretely, if f is a class function on H with f 1 = 0 then

Res_H (Ind_H^G f) = f when (|H| : k) is a unit, hence ⟨Ind f, Ind f⟩_G = ⟨f, f⟩_H when (|G| : k) is (which gives the former, by TauCeti.isUnit_natCard_subgroup). All the statements below carry that hypothesis.

The first statement is Subgroup.comap_subtype_indClassFunction_eq_self and the second is TauCeti.characterPairing_ind_ind. This is the isometry that the exceptional-character route to Frobenius's theorem runs on: it is what makes a difference χᵢ - χⱼ of two distinct ordinary irreducible characters of H of the same degree, which then vanishes at 1 and has norm 2, induce to a norm-2 virtual character of G, so that it is ± a difference of two irreducible characters of G. (Both qualifications are needed: (χᵢ - χⱼ) 1 = χᵢ 1 - χⱼ 1 is the difference of the two degrees, and the norm is 2 by orthonormality only for distinct ordinary characters.)

The hypothesis is not the tautology that f vanishes off H, which holds for every class function on H and gives no such conclusion. What is used is the trivial-intersection condition: for y ∉ H, an element of H conjugated by y back into H must be the identity, where f vanishes. So exactly the terms of the group sum coming from outside H drop out, and the remaining |H| terms all equal f x.

Main statements

• Subgroup.indClassFun_apply_coe: the induced class function agrees with f on H.
• Subgroup.comap_subtype_indClassFunction_eq_self: restriction undoes induction, Res ∘ Ind = id.
• TauCeti.characterPairing_ind_ind: induction preserves the character pairing.
• TauCeti.characterPairing_ind_ind_of_isTISet and TauCeti.isometry_ind_of_isTISet: the same, for a class function supported on a trivial-intersection set of a proper trivial-intersection subgroup, which is the form Frobenius's theorem uses (applied there to a Frobenius complement).

Implementation notes

Only f₂ 1 = 0 is needed for TauCeti.characterPairing_ind_ind, not the same hypothesis on f₁: the proof is Frobenius reciprocity ⟨Ind f₁, Ind f₂⟩ = ⟨f₁, Res (Ind f₂)⟩ followed by Res (Ind f₂) = f₂, and only the second factor is restricted. Since TauCeti.ClassFunction.characterPairing_symm says the pairing is symmetric, the hypothesis may be put on either argument.

References

• I. M. Isaacs, Character Theory of Finite Groups, Chapter 7, Lemma 7.2 and Theorem 7.5.

theorem Subgroup.indClassFun_apply_coe {k : Type u} {G : Type v} [Field k] [Group G] (H : Subgroup G) [Finite G] (hH : TauCeti.IsTISubgroup H) (hk : IsUnit ↑(Nat.card ↥H)) {f : ↥H → k} (hf : f ∈ TauCeti.ClassFunction k ↥H) (hf1 : f 1 = 0) (x : ↥H) : H.indClassFun f ↑x = f x

A class function vanishing at the identity of a trivial-intersection subgroup induces to a function agreeing with it on the subgroup.

In the group-sum form |H| · (Ind f)(x) = ∑_{y ∈ G} f (y⁻¹ x y) (terms with y⁻¹ x y ∉ H read as 0), a term with y ∉ H contributes nothing: if y⁻¹ x y ∈ H then the trivial-intersection condition forces x = 1, and f vanishes there. The |H| terms with y ∈ H each equal f x, because f is a class function.

theorem Subgroup.comap_subtype_indClassFunction_eq_self {k : Type u} {G : Type v} [Field k] [Group G] (H : Subgroup G) [Finite G] (hH : TauCeti.IsTISubgroup H) (hk : IsUnit ↑(Nat.card ↥H)) (f : ↥(TauCeti.ClassFunction k ↥H)) (hf1 : ↑f 1 = 0) : (TauCeti.ClassFunction.comap H.subtype) (H.indClassFunction f) = f

Restriction undoes induction, for a class function on a trivial-intersection subgroup that vanishes at the identity. This is the bundled form of Subgroup.indClassFun_apply_coe.

theorem TauCeti.characterPairing_ind_ind {k : Type u} {G : Type v} [Field k] [Group G] {H : Subgroup G} [Fintype G] (hG : IsUnit ↑(Nat.card G)) (hH : IsTISubgroup H) (f₁ f₂ : ↥(ClassFunction k ↥H)) (hf₂ : ↑f₂ 1 = 0) : (ClassFunction.characterPairing (H.indClassFunction f₁)) (H.indClassFunction f₂) = (ClassFunction.characterPairing f₁) f₂

Induction from a trivial-intersection subgroup preserves the character pairing, provided the second argument vanishes at the identity. This is the isometry the exceptional-character argument for Frobenius's theorem rests on; taking f₁ = f₂ gives the preservation of the norm.

theorem TauCeti.characterPairing_ind_ind_of_isTISet {k : Type u} {G : Type v} [Field k] [Group G] {H : Subgroup G} {S : Set G} [Fintype G] (hG : IsUnit ↑(Nat.card G)) (hH : IsTISubgroup H) (hne_top : H ≠ ⊤) (hS : IsTISet S H) (f₁ f₂ : ↥(ClassFunction k ↥H)) (hf₂ : ∀ (y : ↥H), ↑y ∉ S → ↑f₂ y = 0) : (ClassFunction.characterPairing (H.indClassFunction f₁)) (H.indClassFunction f₂) = (ClassFunction.characterPairing f₁) f₂

A class function supported on a trivial-intersection set of a proper trivial-intersection subgroup induces isometrically. The support condition supplies the vanishing at the identity that TauCeti.characterPairing_ind_ind asks for, because a trivial-intersection set for a proper subgroup does not contain the identity. Nontriviality of H plays no part, so this asks only for the two halves of TauCeti.IsFrobeniusComplement that the argument uses; for a Frobenius complement hH, pass hH.isTISubgroup and hH.ne_top.

theorem TauCeti.isometry_ind_of_isTISet {k : Type u} {G : Type v} [Field k] [Group G] {H : Subgroup G} {S : Set G} [Fintype G] (hG : IsUnit ↑(Nat.card G)) (hH : IsTISubgroup H) (hne_top : H ≠ ⊤) (hS : IsTISet S H) (f : ↥(ClassFunction k ↥H)) (hf : ∀ (y : ↥H), ↑y ∉ S → ↑f y = 0) : (ClassFunction.characterPairing (H.indClassFunction f)) (H.indClassFunction f) = (ClassFunction.characterPairing f) f

Induction from a trivial-intersection set preserves the norm, the special case of TauCeti.characterPairing_ind_ind_of_isTISet at equal arguments. A difference of two distinct ordinary irreducible characters of H of the same degree is supported off the identity and has norm 2, so it induces to a norm-2 virtual character of G; that is the step the exceptional-character correspondence begins with.

Preserving the pairing at equal arguments is preservation of the norm, which is what "isometry" refers to.