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 TauCeti.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 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 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.

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.indVirtualCharacterDirectSumBaseChangeRat_surjective_of_nsmul_one_mem: a general criterion for rational surjectivity of the scalar-extended induction map.
• TauCeti.ClassFunction.mul_mem_indVirtualCharacters: the ideal property.
• 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.

References

This is the "Ind_H^G : R(H) → R(G) is a homomorphism of R(G)-modules -- Frobenius reciprocity as a module identity" item of Layer 6 in TauCetiRoadmap/RepresentationTheory/InductionRestriction/README.md, and the reduction step of the Brauer-induction item of the same layer.

• 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.
• 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).

Equations

• TauCeti.ClassFunction.indVirtualCharacters k G P = AddSubgroup.closure (TauCeti.ClassFunction.indVirtualCharacterSet✝ k G P)

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) : indClassFun S ψ ∈ indVirtualCharacters k G P

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

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, indClassFun S ψ ∈ 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), indClassFun S 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).

Equations

• TauCeti.ClassFunction.indVirtualCharacterDirectSumAddHom k G P = DirectSum.toAddMonoid fun (S : { S : Subgroup G // P S }) => TauCeti.ClassFunction.indVirtualCharacterAddHom k G ↑S

@[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.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. For a virtual character f of G and 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 again a virtual character of S, restriction and multiplication both preserving them.

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.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 ℚ.

Equations

• TauCeti.ClassFunction.indVirtualCharacterDirectSumBaseChangeRat k G P = LinearMap.baseChange ℚ (TauCeti.ClassFunction.indVirtualCharacterDirectSumAddHom k G P).toIntLinearMap

@[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.