Induction from a covering family of subgroups spans the class functions

Let 𝒮 be a family of subgroups of a finite group G that covers G up to conjugacy: every element of G has a conjugate lying in some member of 𝒮. Over a field k in which |G| is invertible, induction from 𝒮 is then surjective on class functions: the class functions Ind_S^G ψ, for S ∈ 𝒮 and ψ a class function of S, span all class functions of G (TauCeti.ClassFunction.indSpan_eq_top).

The proof is the classical duality argument. The character pairing is nondegenerate, so the span is everything as soon as nothing nonzero is orthogonal to it. Frobenius reciprocity converts orthogonality to every class function induced from S into the vanishing of the restriction of h to S, and a class function whose restriction to every member of 𝒮 vanishes is zero, because each x is conjugate into some member and a class function is constant on conjugacy classes.

The cyclic subgroups cover G, for the trivial reason that x generates a cyclic subgroup containing it, so the class functions induced from them span (TauCeti.ClassFunction.indSpan_cyclic_eq_top). The covering hypothesis is stated for a general family because the elementary subgroups, which Brauer's induction theorem uses, satisfy it too.

Over an algebraically closed k the spanning set can be cut down to genuine induced characters: the irreducible characters of S span the class functions of S, so TauCeti.ClassFunction.indCharacterSpan_cyclic_eq_top says that the characters induced from the irreducible characters of the cyclic subgroups already span.

Relation to Artin's induction theorem

Artin's induction theorem is the sharper arithmetic statement, about the virtual-character lattice TauCeti.virtualCharacters rather than about the class functions: over a characteristic-zero splitting field, |G| • χ is a ℤ-linear combination of characters induced from cyclic subgroups. The rational form says that every character is a ℚ-linear combination of them — equivalently, that some nonzero integer multiple is an integral combination — or that ⨁_{C cyclic} R(C) → R(G) is surjective after tensoring with ℚ. The |G| statement is strictly sharper.

This file supplies the duality half of that development, run on the class functions instead of on ℚ ⊗ R(G), and the family-general comparison between the integral induced-character span and the canonical subgroup of induced virtual characters. Over an algebraically closed field in which the selected subgroup orders are invertible, TauCeti.ClassFunction.indVirtualCharacters_eq_indCharacterSpanInt identifies those two integral targets. TauCeti.RepresentationTheory.Induction.Artin.Basic supplies the arithmetic half: it proves the sharp |G| statement, specializes this comparison to its conventional induced-character-span endpoint, and proves the rational surjectivity of the direct-sum induction map bundled in TauCeti.RepresentationTheory.Induction.Ideal. The integral theorems indexed by the elementary subgroups are proved in TauCeti.RepresentationTheory.Induction.Brauer.Induction and TauCeti.RepresentationTheory.Induction.Brauer.Characterization. The covering-family formulation is stated here for its own sake: the elementary subgroups Brauer's theorem uses satisfy the same hypothesis.

Main definitions

• TauCeti.ClassFunction.indSpan: the submodule of class functions of G spanned by the class functions induced from a family 𝒮 of subgroups.
• TauCeti.ClassFunction.indCharacterSpan: the smaller submodule generated by inductions of only irreducible characters of the members of 𝒮.
• TauCeti.ClassFunction.indCharacterSpanInt: the additive subgroup generated by the same induced characters, with integer coefficients.

Main statements

• TauCeti.ClassFunction.indSpan_eq_top: induction from a family of subgroups covering G up to conjugacy spans all class functions, and TauCeti.ClassFunction.indSpan_cyclic_eq_top: its cyclic case, with TauCeti.ClassFunction.exists_sum_smul_ind_cyclic the explicit finite-combination form.
• TauCeti.ClassFunction.indCharacterSpan_eq_indSpan: over an algebraically closed field in which the orders of the selected subgroups are invertible, inducing only the irreducible characters of the subgroups spans as much as inducing all their class functions, whence TauCeti.ClassFunction.indCharacterSpan_eq_top and TauCeti.ClassFunction.indCharacterSpan_cyclic_eq_top, with TauCeti.ClassFunction.exists_sum_smul_ind_ofCharacter_cyclic the explicit form.
• TauCeti.ClassFunction.indVirtualCharacters_eq_indCharacterSpanInt: over an algebraically closed field in which the selected subgroup orders are invertible, the canonical subgroup of induced virtual characters equals the integral span of induced irreducible characters.

Implementation notes

Only the invertibility of |G| in k is assumed for the first form; no algebraic closure is needed, because the duality argument runs on TauCeti.ClassFunction.characterPairing_nondegenerate alone. Algebraic closure enters only in the refinement to induced characters, where completeness of the irreducible characters of the subgroup is used. That refinement needs no assumption on |G| at all, only invertibility of the orders of the members of 𝒮, so it takes that as an explicit hypothesis rather than an ambient instance; the covering corollaries supply it from TauCeti.isUnit_natCard_subgroup.

The covering hypothesis is written out as ∀ x : G, ∃ S ∈ 𝒮, ∃ y : G, y * x * y⁻¹ ∈ S rather than bundled into a predicate: it is used once, and the cyclic instance discharges it with y = 1.

The class-function spanning theorems produce coefficients in k. In contrast, TauCeti.ClassFunction.indCharacterSpanInt and its comparison with induced virtual characters are statements about additive subgroups and therefore integral coefficients; see the discussion above of what still separates these structural results from Artin's induction theorem.

References

The duality argument is used to prove the ℤ-membership of |G| • χ in the subgroup generated by cyclic-induced characters and the rational surjectivity of ⨁_{C cyclic} R(C) → R(G) in TauCeti.RepresentationTheory.Induction.Artin.Basic through the canonical induced-virtual-character API.

• J.-P. Serre, Linear Representations of Finite Groups, Springer GTM 42 (1977), Section 9.2, Theorem 17, whose duality argument this follows. Serre runs it on ℚ ⊗ R(G), which is what makes his conclusion the rational one; here it runs on the class functions over k.
• C. W. Curtis, I. Reiner, Methods of Representation Theory, Vol. I, Wiley (1981), Section 15.

Class functions induced from a family of subgroups

def TauCeti.ClassFunction.indSet (k : Type u) (G : Type v) [Field k] [Group G] [Finite G] (𝒮 : Set (Subgroup G)) : Set ↥(ClassFunction k G)

The set of class functions of G induced from the members of a family 𝒮 of subgroups.

noncomputable def TauCeti.ClassFunction.indSpan (k : Type u) (G : Type v) [Field k] [Group G] [Finite G] (𝒮 : Set (Subgroup G)) : Submodule k ↥(ClassFunction k G)

The submodule generated by TauCeti.ClassFunction.indSet.

@[simp]

theorem TauCeti.ClassFunction.mem_indSet (k : Type u) (G : Type v) [Field k] [Group G] [Finite G] {𝒮 : Set (Subgroup G)} {f : ↥(ClassFunction k G)} : f ∈ indSet k G 𝒮 ↔ ∃ S ∈ 𝒮, ∃ (ψ : ↥(ClassFunction k ↥S)), S.indClassFunction ψ = f

Membership in the generating set for TauCeti.ClassFunction.indSpan.

theorem TauCeti.ClassFunction.ind_mem_indSpan {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] {𝒮 : Set (Subgroup G)} {S : Subgroup G} (hS : S ∈ 𝒮) (ψ : ↥(ClassFunction k ↥S)) : S.indClassFunction ψ ∈ indSpan k G 𝒮

A class function induced from a member of 𝒮 lies in TauCeti.ClassFunction.indSpan, the submodule these generate.

theorem TauCeti.ClassFunction.indSpan_le_iff {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] {𝒮 : Set (Subgroup G)} {p : Submodule k ↥(ClassFunction k G)} : indSpan k G 𝒮 ≤ p ↔ ∀ S ∈ 𝒮, ∀ (ψ : ↥(ClassFunction k ↥S)), S.indClassFunction ψ ∈ p

The universal property of TauCeti.ClassFunction.indSpan: it is contained in a submodule exactly when every class function induced from a member of 𝒮 is.

theorem TauCeti.ClassFunction.eq_zero_of_characterPairing_indSpan_eq_zero {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [Invertible ↑(Nat.card G)] {𝒮 : Set (Subgroup G)} (h𝒮 : ∀ (x : G), ∃ S ∈ 𝒮, ∃ (y : G), y * x * y⁻¹ ∈ S) {h : ↥(ClassFunction k G)} (hh : have this := Fintype.ofFinite G; ∀ f ∈ indSpan k G 𝒮, (characterPairing f) h = 0) : h = 0

A class function orthogonal to every induction from 𝒮 vanishes, when 𝒮 covers G up to conjugacy. Frobenius reciprocity turns orthogonality to all of Ind_S^G (ClassFunction k S) into orthogonality of the restriction of h to S against all class functions of S, so that restriction is zero by nondegeneracy of the pairing on S. Any conjugate of x lying in S then evaluates h at x.

theorem TauCeti.ClassFunction.indSpan_eq_top {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [Invertible ↑(Nat.card G)] {𝒮 : Set (Subgroup G)} (h𝒮 : ∀ (x : G), ∃ S ∈ 𝒮, ∃ (y : G), y * x * y⁻¹ ∈ S) : indSpan k G 𝒮 = ⊤

Induction from a covering family of subgroups is surjective on class functions. If every element of the finite group G is conjugate into a member of 𝒮, and |G| is invertible in k, then the class functions induced from the members of 𝒮 span all class functions of G.

TauCeti.ClassFunction.indSpan_cyclic_eq_top is the case of the cyclic subgroups; the family of elementary subgroups, which Brauer's induction theorem uses, satisfies the same hypothesis.

theorem TauCeti.ClassFunction.indSpan_cyclic_eq_top {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [Invertible ↑(Nat.card G)] : indSpan k G {S : Subgroup G | IsCyclic ↥S} = ⊤

The class functions induced from the cyclic subgroups span. Over a field in which the order of the finite group G is invertible, the class functions induced from the cyclic subgroups of G span all class functions of G; equivalently, the induction map ⨁_{C cyclic} ClassFunction k C → ClassFunction k G is surjective.

The explicit finite-combination form is TauCeti.ClassFunction.exists_sum_smul_ind_cyclic, and TauCeti.ClassFunction.indCharacterSpan_cyclic_eq_top refines the spanning set to induced characters.

This is not Artin's induction theorem: the coefficients here are arbitrary elements of k, while Artin's theorem is a statement about TauCeti.virtualCharacters, asserting that they may be taken rational and that |G| • χ is an integral combination of induced virtual characters. Both forms are proved in TauCeti.RepresentationTheory.Induction.Artin.Basic.

theorem TauCeti.ClassFunction.exists_sum_smul_ind_cyclic {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [Invertible ↑(Nat.card G)] (f : ↥(ClassFunction k G)) : ∃ (n : ℕ) (C : Fin n → Subgroup G) (_ : ∀ (i : Fin n), IsCyclic ↥(C i)) (ψ : (i : Fin n) → ↥(ClassFunction k ↥(C i))) (c : Fin n → k), ∑ i : Fin n, c i • (C i).indClassFunction (ψ i) = f

TauCeti.ClassFunction.indSpan_cyclic_eq_top written out: every class function of G is a finite k-linear combination of class functions induced from cyclic subgroups.

Characters induced from a family of subgroups

def TauCeti.ClassFunction.indCharacterSet (k : Type u) (G : Type v) [Field k] [Group G] [Finite G] (𝒮 : Set (Subgroup G)) : Set ↥(ClassFunction k G)

The set of characters induced from the irreducible characters of the members of a family 𝒮 of subgroups of G.

noncomputable def TauCeti.ClassFunction.indCharacterSpan (k : Type u) (G : Type v) [Field k] [Group G] [Finite G] (𝒮 : Set (Subgroup G)) : Submodule k ↥(ClassFunction k G)

The submodule of class functions of G spanned by the characters induced from the irreducible characters of the members of a family 𝒮 of subgroups of G.

This is contained in TauCeti.ClassFunction.indSpan, and over an algebraically closed field in which the orders of the selected subgroups are invertible the two agree (TauCeti.ClassFunction.indCharacterSpan_eq_indSpan).

As in TauCeti.ClassFunction.le_span_irreducibleCharacters, the irreducibles are taken on the coordinate spaces Fin n → k, which is where the Wedderburn presentation of the group algebra produces them.

@[simp]

theorem TauCeti.ClassFunction.mem_indCharacterSet (k : Type u) (G : Type v) [Field k] [Group G] [Finite G] {𝒮 : Set (Subgroup G)} {f : ↥(ClassFunction k G)} : f ∈ indCharacterSet k G 𝒮 ↔ ∃ S ∈ 𝒮, ∃ (n : ℕ) (ρ : Representation k (↥S) (Fin n → k)), ρ.IsIrreducible ∧ S.indClassFunction (ofCharacter ρ) = f

Membership in the generating set for TauCeti.ClassFunction.indCharacterSpan.

theorem TauCeti.ClassFunction.ind_ofCharacter_mem_indCharacterSpan {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] {𝒮 : Set (Subgroup G)} {S : Subgroup G} (hS : S ∈ 𝒮) {n : ℕ} (ρ : Representation k (↥S) (Fin n → k)) (hρ : ρ.IsIrreducible) : S.indClassFunction (ofCharacter ρ) ∈ indCharacterSpan k G 𝒮

A character induced from an irreducible character of a member of 𝒮 lies in TauCeti.ClassFunction.indCharacterSpan, the submodule these generate.

theorem TauCeti.ClassFunction.indCharacterSpan_le_iff {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] {𝒮 : Set (Subgroup G)} {p : Submodule k ↥(ClassFunction k G)} : indCharacterSpan k G 𝒮 ≤ p ↔ ∀ S ∈ 𝒮, ∀ (n : ℕ) (ρ : Representation k (↥S) (Fin n → k)), ρ.IsIrreducible → S.indClassFunction (ofCharacter ρ) ∈ p

The universal property of TauCeti.ClassFunction.indCharacterSpan: it is contained in a submodule exactly when every character induced from an irreducible character of a member of 𝒮 is.

def TauCeti.ClassFunction.indCharacterSpanInt (k : Type u) (G : Type v) [Field k] [Group G] [Finite G] (P : Subgroup G → Prop) : AddSubgroup (G → k)

The additive subgroup of functions on G generated by characters induced from irreducible characters of the subgroups satisfying P. This is the integral-lattice counterpart of TauCeti.ClassFunction.indCharacterSpan; unlike that k-linear span, its coefficients are integers.

theorem Subgroup.indClassFunction_ofCharacter_mem_indCharacterSpanInt {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] {P : Subgroup G → Prop} (C : Subgroup G) (hC : P C) {n : ℕ} (ρ : Representation k (↥C) (Fin n → k)) (hρ : ρ.IsIrreducible) : ↑(C.indClassFunction (TauCeti.ClassFunction.ofCharacter ρ)) ∈ TauCeti.ClassFunction.indCharacterSpanInt k G P

A character induced from an irreducible character of a subgroup satisfying P belongs to TauCeti.ClassFunction.indCharacterSpanInt.

theorem TauCeti.ClassFunction.indCharacterSpanInt_le_iff {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] {P : Subgroup G → Prop} {H : AddSubgroup (G → k)} : indCharacterSpanInt k G P ≤ H ↔ ∀ (C : Subgroup G), P C → ∀ (n : ℕ) (ρ : Representation k (↥C) (Fin n → k)), ρ.IsIrreducible → ↑(C.indClassFunction (ofCharacter ρ)) ∈ H

The universal property of TauCeti.ClassFunction.indCharacterSpanInt: it is contained in an additive subgroup exactly when every generating induced irreducible character is.

theorem TauCeti.ClassFunction.indCharacterSpanInt_le_indVirtualCharacters {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] {P : Subgroup G → Prop} : indCharacterSpanInt k G P ≤ indVirtualCharacters k G P

A character induced from an irreducible character of a subgroup satisfying P is induced from a virtual character of that subgroup, so the induced-irreducible span sits inside the canonical subgroup induced from the family.

theorem TauCeti.ClassFunction.indVirtualCharacters_le_indCharacterSpanInt {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [IsAlgClosed k] {P : Subgroup G → Prop} (hP : ∀ (C : Subgroup G), P C → IsUnit ↑(Nat.card ↥C)) : indVirtualCharacters k G P ≤ indCharacterSpanInt k G P

The virtual characters induced from a family are generated by induced irreducible characters. Over an algebraically closed field in which each selected subgroup order is invertible, a virtual character of a subgroup C is an integer combination of its irreducible characters (TauCeti.virtualCharacters_eq_closure_irreducibleCharacters), and induction is additive, so inducing all of R(C) produces nothing beyond what inducing the irreducible characters produces.

theorem TauCeti.ClassFunction.indVirtualCharacters_eq_indCharacterSpanInt {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [IsAlgClosed k] {P : Subgroup G → Prop} (hP : ∀ (C : Subgroup G), P C → IsUnit ↑(Nat.card ↥C)) : indVirtualCharacters k G P = indCharacterSpanInt k G P

The canonical induced-virtual-character subgroup is generated by induced irreducible characters. Over an algebraically closed field in which each selected subgroup order is invertible, it makes no difference, for any family P, whether one induces the irreducible characters of its members or all of their virtual characters.

theorem TauCeti.ClassFunction.indCharacterSpan_le_indSpan {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] (𝒮 : Set (Subgroup G)) : indCharacterSpan k G 𝒮 ≤ indSpan k G 𝒮

A character is a class function, so inducing only the irreducible characters of the members of 𝒮 spans no more than inducing all their class functions.

theorem TauCeti.ClassFunction.indSpan_le_indCharacterSpan {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [IsAlgClosed k] {𝒮 : Set (Subgroup G)} (h𝒮 : ∀ S ∈ 𝒮, IsUnit ↑(Nat.card ↥S)) : indSpan k G 𝒮 ≤ indCharacterSpan k G 𝒮

Inducing an arbitrary class function of a subgroup gains nothing over inducing its irreducible characters: over an algebraically closed field the latter already span the class functions of the subgroup, and induction is linear.

Only the orders of the selected subgroups need be invertible in k; |G| itself is irrelevant here, and the covering corollaries below supply the hypothesis from TauCeti.isUnit_natCard_subgroup.

theorem TauCeti.ClassFunction.indCharacterSpan_eq_indSpan {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [IsAlgClosed k] {𝒮 : Set (Subgroup G)} (h𝒮 : ∀ S ∈ 𝒮, IsUnit ↑(Nat.card ↥S)) : indCharacterSpan k G 𝒮 = indSpan k G 𝒮

Over an algebraically closed field, inducing the irreducible characters of the members of 𝒮 spans exactly as much as inducing all their class functions. As in TauCeti.ClassFunction.indSpan_le_indCharacterSpan, only the orders of the members of 𝒮 need be invertible.

theorem TauCeti.ClassFunction.indCharacterSpan_eq_top {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [IsAlgClosed k] [Invertible ↑(Nat.card G)] {𝒮 : Set (Subgroup G)} (h𝒮 : ∀ (x : G), ∃ S ∈ 𝒮, ∃ (y : G), y * x * y⁻¹ ∈ S) : indCharacterSpan k G 𝒮 = ⊤

Induction of irreducible characters from a covering family of subgroups already spans the class functions, over an algebraically closed field in which |G| is invertible.

theorem TauCeti.ClassFunction.indCharacterSpan_cyclic_eq_top {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [IsAlgClosed k] [Invertible ↑(Nat.card G)] : indCharacterSpan k G {S : Subgroup G | IsCyclic ↥S} = ⊤

The characters induced from the irreducible characters of the cyclic subgroups span. Over an algebraically closed field in which the order of the finite group G is invertible, they span all class functions of G.

In particular every character of G is a k-linear combination of characters induced from cyclic subgroups; TauCeti.ClassFunction.exists_sum_smul_ind_ofCharacter_cyclic writes that combination out. The coefficients are arbitrary elements of k. Artin's induction theorem asserts that they may be taken rational; TauCeti.ClassFunction.natCard_nsmul_mem_indVirtualCharacters_isCyclic gives its sharp integral form through the canonical virtual-character API.

theorem TauCeti.ClassFunction.exists_sum_smul_ind_ofCharacter_cyclic {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [IsAlgClosed k] [Invertible ↑(Nat.card G)] (f : ↥(ClassFunction k G)) : ∃ (n : ℕ) (C : Fin n → Subgroup G) (_ : ∀ (i : Fin n), IsCyclic ↥(C i)) (d : Fin n → ℕ) (ρ : (i : Fin n) → Representation k (↥(C i)) (Fin (d i) → k)) (_ : ∀ (i : Fin n), (ρ i).IsIrreducible) (c : Fin n → k), ∑ i : Fin n, c i • (C i).indClassFunction (ofCharacter (ρ i)) = f

TauCeti.ClassFunction.indCharacterSpan_cyclic_eq_top written out over an algebraically closed field: every class function of G — in particular, by TauCeti.ClassFunction.ofCharacter, every character of G — is a finite k-linear combination of characters induced from irreducible characters of cyclic subgroups.