The virtual characters induced from a family of subgroups form an ideal

Fix a finite group G and a property P of its subgroups. The virtual characters of G induced from subgroups satisfying P span an additive subgroup TauCeti.ClassFunction.indVirtualCharacters k G P of the functions on G; in Serre's notation, for P the elementary subgroups, this is the image V_G of ⨁_{E} R(E) → R(G).

The theorem of this file is that V_G is an ideal of the virtual-character ring R(G) (TauCeti.ClassFunction.mul_mem_indVirtualCharacters): multiplying an induced virtual character by a virtual character of G gives another induced virtual character. This is the projection formula Subgroup.indClassFun_comp_subtype_mul -- Frobenius reciprocity in its module form -- together with the closure of the virtual characters of a subgroup under restriction and under products. The projection formula asks only that the multiplier be a class function whose restriction to each subgroup of the family is a virtual character, and TauCeti.ClassFunction.mul_mem_indVirtualCharacters_of_forall_comp_subtype records the ideal property under that weaker hypothesis; it is the form in which a class function known only locally to be a virtual character is recognized as one.

The family-general induction map is also bundled here as TauCeti.ClassFunction.indVirtualCharacterDirectSumAddHom, the homomorphism ⨁_{S} R(S) → R(G). Its range is exactly V_G. After tensoring source and target with ℚ, a nonzero multiple of 1 in V_G makes the resulting map surjective. These constructions belong with the ideal property because they work for an arbitrary family and use no cyclic or elementary input; TauCeti.RepresentationTheory.Induction.Artin.Basic supplies those arithmetic specializations.

Its consequence TauCeti.ClassFunction.indVirtualCharacters_eq_virtualCharacters_iff is the standard reduction of an induction theorem to a single membership: V_G is all of R(G) iff the constant function 1 lies in V_G. Brauer's induction theorem is exactly the statement that 1 ∈ V_G for the elementary subgroups, and that arithmetic input is not proved here.

Putting the two together gives the restriction criterion TauCeti.mem_virtualCharacters_of_forall_comp_subtype: as soon as 1 ∈ V_G, a class function whose restriction to every subgroup of the family is a virtual character is itself a virtual character, and TauCeti.mem_virtualCharacters_iff_forall_comp_subtype makes that an equivalence, its forward direction being the compatibility of restriction with the lattice. Both are stated for an arbitrary family and use no cyclic or elementary input; TauCeti.RepresentationTheory.Induction.Brauer.Characterization specializes them to the elementary subgroups, where Brauer's induction theorem supplies the hypothesis.

What is proved here is the form in which that membership is established: TauCeti.ClassFunction.indVirtualCharacters_eq_virtualCharacters_iff_forall_prime weakens it to asking, one prime p at a time, for a multiple m • 1 with p ∤ m that is a combination of induced virtual characters with coefficients in a ring such as ℤ[ζ]. The coefficients descend to ℤ by TauCeti.mem_of_mem_span_of_mem_virtualCharacters, and the primes are assembled by TauCeti.mem_of_forall_prime_exists_nsmul_mem.

Main definitions

• TauCeti.ClassFunction.indVirtualCharacters: the additive subgroup generated by virtual characters induced from a family of subgroups.
• TauCeti.ClassFunction.indVirtualCharacterDirectSumAddHom: the bundled direct-sum induction map from the virtual-character lattices of that family.
• TauCeti.ClassFunction.indVirtualCharacterDirectSumBaseChangeRat: its scalar extension to ℚ.

Main statements

• TauCeti.ClassFunction.indVirtualCharacters_le_virtualCharacters: an induced virtual character is a virtual character.
• TauCeti.ClassFunction.indVirtualCharacters_eq_closure_indFDRepCharacter: induced genuine characters already generate the subgroup of induced virtual characters.
• TauCeti.ClassFunction.range_subtype_comp_indVirtualCharacterDirectSumAddHom: the range of the bundled map is exactly indVirtualCharacters.
• TauCeti.ClassFunction.indVirtualCharacterDirectSumAddHom_surjective_iff: the bundled induction map is surjective exactly when the induced virtual characters exhaust all virtual characters.
• TauCeti.ClassFunction.indVirtualCharacterDirectSumBaseChangeRat_surjective_of_nsmul_one_mem: a general criterion for rational surjectivity of the scalar-extended induction map.
• TauCeti.ClassFunction.mul_mem_indVirtualCharacters_of_forall_comp_subtype: the projection-formula step, for a class function that is a virtual character on each subgroup of the family.
• TauCeti.ClassFunction.mul_mem_indVirtualCharacters: the ideal property.
• TauCeti.ClassFunction.mul_mem_span_indVirtualCharacters: the corresponding ideal property for spans over a subring of the coefficient field.
• TauCeti.ClassFunction.nsmul_mem_indVirtualCharacters_of_nsmul_one_mem: propagation of a multiple of 1 to the same multiple of every virtual character.
• TauCeti.ClassFunction.indVirtualCharacters_eq_virtualCharacters_iff: the induction theorem for a family of subgroups holds exactly when 1 is induced from that family.
• TauCeti.ClassFunction.indVirtualCharacters_eq_virtualCharacters_iff_forall_prime: equivalently, for every prime p some multiple m • 1 with p ∤ m is induced with coefficients in a subring of k that retracts additively onto ℤ.
• TauCeti.mem_virtualCharacters_of_forall_comp_subtype: if 1 is induced from a family of subgroups, a class function whose restrictions to the family are virtual characters is a virtual character.
• TauCeti.mem_virtualCharacters_iff_forall_comp_subtype: for a family of subgroups satisfying an induction theorem, the restrictions to that family detect the virtual characters among the class functions.

References

• J.-P. Serre, Linear Representations of Finite Groups, Springer GTM 42 (1977), Section 10.1, where V_G is introduced and shown to be an ideal, and Theorem 18; Chapter 10, in the proof of Theorem 18, for the reduction to one prime at a time over ℤ[ζ].
• C. W. Curtis, I. Reiner, Methods of Representation Theory, Vol. I, Wiley (1981), Section 15.

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

The virtual characters of G induced from a family of subgroups: the additive subgroup of G → k generated by Ind_S^G ψ for S satisfying P and ψ a virtual character of S.

For P the cyclic or elementary subgroups this is the subgroup generated by induction from their virtual-character lattices; it is the image of the induction map ⨁_S R(S) → R(G).

theorem TauCeti.ClassFunction.indClassFun_mem_indVirtualCharacters {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] {P : Subgroup G → Prop} {S : Subgroup G} (hS : P S) {ψ : ↥S → k} (hψ : ψ ∈ virtualCharacters k ↥S) : S.indClassFun ψ ∈ indVirtualCharacters k G P

A virtual character induced from a subgroup of the family is a member.

theorem TauCeti.ClassFunction.indClassFun_mem_span_indVirtualCharacters {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] {P : Subgroup G → Prop} (A : Subring k) {S : Subgroup G} (hS : P S) {ψ : ↥S → k} (hψ : ψ ∈ Submodule.span ↥A ↑(virtualCharacters k ↥S)) : S.indClassFun ψ ∈ Submodule.span ↥A ↑(indVirtualCharacters k G P)

Induction preserves A-combinations of virtual characters, for any subring A of k: an A-combination of virtual characters of a subgroup of the family induces to an A-combination of induced virtual characters, induction being additive and k-homogeneous.

theorem TauCeti.ClassFunction.indVirtualCharacters_le_iff {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] {P : Subgroup G → Prop} {H : AddSubgroup (G → k)} : indVirtualCharacters k G P ≤ H ↔ ∀ (S : Subgroup G), P S → ∀ ψ ∈ virtualCharacters k ↥S, S.indClassFun ψ ∈ H

The universal property of TauCeti.ClassFunction.indVirtualCharacters: it is contained in an additive subgroup exactly when every induced virtual character of the family is.

theorem TauCeti.ClassFunction.indVirtualCharacters_eq_closure_indFDRepCharacter {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] {P : Subgroup G → Prop} : indVirtualCharacters k G P = AddSubgroup.closure {f : G → k | ∃ (S : Subgroup G), P S ∧ ∃ (V : FDRep k ↥S), S.indClassFun V.character = f}

Induced genuine characters generate the induced virtual characters. Although TauCeti.ClassFunction.indVirtualCharacters is defined by inducing all virtual characters, it is already generated by the inductions of characters of genuine finite-dimensional representations.

theorem TauCeti.ClassFunction.indVirtualCharacters_mono {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] {P Q : Subgroup G → Prop} (h : ∀ (S : Subgroup G), P S → Q S) : indVirtualCharacters k G P ≤ indVirtualCharacters k G Q

Enlarging the family of subgroups enlarges the subgroup of induced virtual characters.

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

An induced virtual character is a virtual character. Equivalently, the induction map lands in R(G), so TauCeti.ClassFunction.indVirtualCharacters really is a subgroup of the virtual-character lattice.

The direct-sum induction map

noncomputable def TauCeti.ClassFunction.indVirtualCharacterDirectSumAddHom (k : Type u) (G : Type v) [Field k] [Group G] [Finite G] (P : Subgroup G → Prop) : (DirectSum { S : Subgroup G // P S } fun (S : { S : Subgroup G // P S }) => ↥(virtualCharacters k ↥↑S)) →+ ↥(virtualCharacters k G)

The direct-sum induction homomorphism for a family of subgroups. Its S-component is Ind_S^G : R(S) → R(G).

@[simp]

theorem TauCeti.ClassFunction.indVirtualCharacterDirectSumAddHom_of {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] {P : Subgroup G → Prop} [DecidableEq { S : Subgroup G // P S }] (S : { S : Subgroup G // P S }) (ψ : ↥(virtualCharacters k ↥↑S)) : (indVirtualCharacterDirectSumAddHom k G P) ((DirectSum.of (fun (S : { S : Subgroup G // P S }) => ↥(virtualCharacters k ↥↑S)) S) ψ) = (indVirtualCharacterAddHom k G ↑S) ψ

The direct-sum induction map sends a vector supported at S to induction from S.

theorem TauCeti.ClassFunction.range_subtype_comp_indVirtualCharacterDirectSumAddHom {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] {P : Subgroup G → Prop} : ((virtualCharacters k G).subtype.comp (indVirtualCharacterDirectSumAddHom k G P)).range = indVirtualCharacters k G P

The range of the bundled induction map, after forgetting the target subtype, is exactly the canonical subgroup indVirtualCharacters k G P.

theorem TauCeti.ClassFunction.indVirtualCharacterDirectSumAddHom_surjective_iff {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] {P : Subgroup G → Prop} : Function.Surjective ⇑(indVirtualCharacterDirectSumAddHom k G P) ↔ indVirtualCharacters k G P = virtualCharacters k G

The direct-sum induction map for a family of subgroups is surjective exactly when the virtual characters induced from that family exhaust the virtual characters of G.

theorem TauCeti.ClassFunction.mul_mem_indVirtualCharacters_of_forall_comp_subtype {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] {P : Subgroup G → Prop} {f : G → k} (hf : f ∈ ClassFunction k G) (hres : ∀ (S : Subgroup G), P S → (fun (s : ↥S) => f ↑s) ∈ virtualCharacters k ↥S) {u : G → k} (hu : u ∈ indVirtualCharacters k G P) : f * u ∈ indVirtualCharacters k G P

The induced virtual characters absorb multiplication by a class function that is a virtual character on the family. For a virtual character ψ of a subgroup S of the family, the projection formula rewrites f · Ind_S^G ψ as Ind_S^G ((Res_S f) · ψ), and (Res_S f) · ψ is a virtual character of S as soon as Res_S f is, the virtual characters being closed under products. Only the class-function property of f enters, through the projection formula.

TauCeti.ClassFunction.mul_mem_indVirtualCharacters is the case of a virtual character f, where the restriction hypothesis is automatic.

theorem TauCeti.ClassFunction.mul_mem_indVirtualCharacters {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] {P : Subgroup G → Prop} {f u : G → k} (hf : f ∈ virtualCharacters k G) (hu : u ∈ indVirtualCharacters k G P) : f * u ∈ indVirtualCharacters k G P

The induced virtual characters form an ideal of the virtual-character ring. Multiplying an induced virtual character by a virtual character of G gives an induced virtual character, because a virtual character is a class function whose restriction to every subgroup is again a virtual character.

This is the structural half of every induction theorem: once 1 is known to be induced from the family, TauCeti.ClassFunction.indVirtualCharacters_eq_virtualCharacters_iff turns the ideal into all of R(G).

theorem TauCeti.ClassFunction.mul_mem_span_indVirtualCharacters {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] (A : Subring k) (P : Subgroup G → Prop) {f u : G → k} (hf : f ∈ Submodule.span ↥A ↑(virtualCharacters k G)) (hu : u ∈ Submodule.span ↥A ↑(indVirtualCharacters k G P)) : f * u ∈ Submodule.span ↥A ↑(indVirtualCharacters k G P)

Multiplying an A-linear combination of virtual characters by an A-linear combination of virtual characters induced from a family of subgroups remains in the induced span.

theorem TauCeti.ClassFunction.nsmul_mem_indVirtualCharacters_of_nsmul_one_mem {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] {P : Subgroup G → Prop} {n : ℕ} (h : n • 1 ∈ indVirtualCharacters k G P) {f : G → k} (hf : f ∈ virtualCharacters k G) : n • f ∈ indVirtualCharacters k G P

If a natural-number multiple of the trivial character is induced from a family, then the same multiple of every virtual character is induced from that family.

Rational scalar extension

noncomputable def TauCeti.ClassFunction.indVirtualCharacterDirectSumBaseChangeRat (k : Type u) (G : Type v) [Field k] [Group G] [Finite G] (P : Subgroup G → Prop) : TensorProduct ℤ ℚ (DirectSum { S : Subgroup G // P S } fun (S : { S : Subgroup G // P S }) => ↥(virtualCharacters k ↥↑S)) →ₗ[ℚ] TensorProduct ℤ ℚ ↥(virtualCharacters k G)

The direct-sum induction map after extension of scalars from ℤ to ℚ.

@[simp]

theorem TauCeti.ClassFunction.indVirtualCharacterDirectSumBaseChangeRat_tmul {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] (P : Subgroup G → Prop) (q : ℚ) (x : DirectSum { S : Subgroup G // P S } fun (S : { S : Subgroup G // P S }) => ↥(virtualCharacters k ↥↑S)) : (indVirtualCharacterDirectSumBaseChangeRat k G P) (q ⊗ₜ[ℤ] x) = q ⊗ₜ[ℤ] (indVirtualCharacterDirectSumAddHom k G P) x

Rationalized induction sends a pure tensor to the tensor of its induced component.

theorem TauCeti.ClassFunction.indVirtualCharacterDirectSumBaseChangeRat_surjective_of_nsmul_one_mem {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] (P : Subgroup G → Prop) (n : ℕ) (hn : n ≠ 0) (h : n • 1 ∈ indVirtualCharacters k G P) : Function.Surjective ⇑(indVirtualCharacterDirectSumBaseChangeRat k G P)

A nonzero multiple of the trivial character in the induced subgroup makes rationalized induction surjective.

theorem TauCeti.ClassFunction.indVirtualCharacters_eq_virtualCharacters_iff {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] {P : Subgroup G → Prop} : indVirtualCharacters k G P = virtualCharacters k G ↔ 1 ∈ indVirtualCharacters k G P

An induction theorem is a single membership. The virtual characters induced from a family of subgroups exhaust R(G) exactly when the constant function 1, the character of the trivial representation, is one of them.

Brauer's induction theorem is this statement for the elementary subgroups, and its whole content is therefore the membership 1 ∈ V_G.

theorem TauCeti.mem_virtualCharacters_of_forall_comp_subtype {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] {P : Subgroup G → Prop} (h1 : 1 ∈ ClassFunction.indVirtualCharacters k G P) {f : G → k} (hf : f ∈ ClassFunction k G) (hres : ∀ (S : Subgroup G), P S → (fun (s : ↥S) => f ↑s) ∈ virtualCharacters k ↥S) : f ∈ virtualCharacters k G

The restriction criterion for virtual characters. If the constant function 1 is induced from a family of subgroups, then a class function on G whose restriction to every subgroup of the family is a virtual character is itself a virtual character.

Writing f = f · 1 and pushing f inside the inductions through the projection formula (TauCeti.ClassFunction.mul_mem_indVirtualCharacters_of_forall_comp_subtype) exhibits f as a sum of virtual characters induced from the family. By TauCeti.ClassFunction.indVirtualCharacters_eq_virtualCharacters_iff the hypothesis on the family is exactly the induction theorem for it.

theorem TauCeti.mem_virtualCharacters_iff_forall_comp_subtype {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] {P : Subgroup G → Prop} (hP : ClassFunction.indVirtualCharacters k G P = virtualCharacters k G) {f : G → k} (hf : f ∈ ClassFunction k G) : f ∈ virtualCharacters k G ↔ ∀ (S : Subgroup G), P S → (fun (s : ↥S) => f ↑s) ∈ virtualCharacters k ↥S

An induction theorem for a family of subgroups makes restriction to that family detect the virtual characters. For a class function on G, membership in the virtual-character lattice is equivalent to membership of all its restrictions to the family.

The forward direction TauCeti.comp_subtype_mem_virtualCharacters needs no hypothesis on the family; the hypothesis is used only for the converse.

theorem TauCeti.ClassFunction.indVirtualCharacters_eq_virtualCharacters_iff_forall_prime {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] {P : Subgroup G → Prop} [IsAlgClosed k] (A : Subring k) (t : ↥A →+ ℤ) (ht : t 1 = 1) : indVirtualCharacters k G P = virtualCharacters k G ↔ ∀ (p : ℕ), Nat.Prime p → ∃ (m : ℕ), ¬p ∣ m ∧ m • 1 ∈ Submodule.span ↥A ↑(indVirtualCharacters k G P)

An induction theorem, one prime at a time and with coefficients in a subring. Let A be a subring of k admitting an additive map t : A → ℤ with t 1 = 1; for example ℤ[ζ] for a root of unity ζ in characteristic zero (PowerBasis.exists_linearMap_apply_one). The virtual characters induced from a family of subgroups exhaust R(G) exactly when, for every prime p, some multiple m • 1 with p ∤ m is an A-linear combination of them.

This reduces an induction theorem to a separate statement for each prime p. In Serre's proof of Brauer's induction theorem, that statement is supplied, for the elementary subgroups, by the p-elementary subgroups with coefficients in ℤ[ζ], ζ a primitive |G|-th root of unity; this declaration does not prove it.