The induced class function

Induction of representations along a finite-index subgroup S ≤ G sends a character of S to a character of G, by the coset-representative formula TauCeti.character_indFDRep_sum_quotient. That formula makes sense for an arbitrary function on S, and this file takes it as the definition of the induced class function Subgroup.indClassFun. It is the linearization of induction on characters, and the map that turns the restriction/induction pair into an adjoint pair on class functions.

Nothing here mentions a representation, so the file sits below TauCeti.RepresentationTheory.Induction.Character, which imports it to identify the induced character with the induced class function of a character (Subgroup.indClassFun_ofFDRep_character) and to deduce TauCeti.character_ind from Subgroup.indClassFun_eq_natCard_inv_mul_sum.

Main definitions

• Function.indTerm f g x: the summand attached to a representative x, namely f (x⁻¹ g x) when x⁻¹ g x lies in the subgroup and 0 otherwise. It is the summand of the induced-character formula too, which the character file uses at f = ρ.character, together with the coset-invariance lemma Function.indTerm_eq_of_mk_eq and the evaluations Function.indTerm_conj and Function.indTerm_one.
• Subgroup.indClassFun S f: the function G → k obtained from f : S → k by summing f over those left coset representatives that conjugate g into S. There is no division by |S|, so it needs no invertibility hypothesis and no more than an additive commutative monoid of coefficients.
• Subgroup.indClassFunAddHom S: the same construction packaged as an additive map (S → k) →+ (G → k), which is what lets a property be propagated through the additive generation of an AddSubgroup of functions.
• Subgroup.indClassFunction S: the same construction packaged as a k-linear map ClassFunction k S →ₗ[k] ClassFunction k G.

Main statements

• Function.indTerm_eq_zero_of_smul_mk_ne and Subgroup.indClassFun_eq_sum_of_smul_eq_self_mem: only the cosets g fixes contribute, so the coset sum may be taken over any finite set of cosets containing the fixed ones. This is what turns the formula into a finite explicit computation for a concrete group.
• Function.indTerm_eq_of_mk_eq_of_conj: a summand depends only on its coset representative when the inducing function is invariant under conjugation in the subgroup.
• Subgroup.indClassFun_conj and Subgroup.indClassFun_mem_classFunction: induction preserves conjugation invariance over additive coefficients and sends class functions to class functions.
• Subgroup.indClassFun_top and Subgroup.indClassFun_indClassFun_subgroupOf: for conjugation-invariant inducing functions, induction from ⊤ is the identity, and induction is transitive along L ≤ T ≤ G.
• Subgroup.natCard_nsmul_indClassFun: for a conjugation-invariant function f, the additive group-sum form |S| • (Ind f)(g) = ∑_{x ∈ G} f(x⁻¹gx), and its averaged corollary Subgroup.indClassFun_eq_natCard_inv_mul_sum.
• Subgroup.indClassFun_comp_subtype_mul: the projection formula, Ind_S^G ((Res_S f) · ψ) = f · Ind_S^G ψ for a class function f of G.

Frobenius reciprocity for class functions, ⟨Ind f, h⟩_G = ⟨f, Res h⟩_S, is TauCeti.frobenius_reciprocity_classFunction; it needs the pairing, so it lives with the other reciprocities in TauCeti.RepresentationTheory.Induction.FrobeniusReciprocity.

Implementation notes

The definition sums over Quotient.out representatives of G ⧸ S, so it literally matches TauCeti.character_indFDRep_sum_quotient. For a general f the individual summands depend on that choice of representatives; being a class function is a sufficient condition for them not to, and that is what Subgroup.indClassFun_mem_classFunction extracts, in the form of conjugation invariance of the total sum. The additive and scalar identities hold for arbitrary functions.

Function.indTerm and the lemmas that evaluate it are shared, not internal to this file: TauCeti.RepresentationTheory.Induction.Character sums it over right cosets and TauCeti.RepresentationTheory.Induction.FrobeniusReciprocity sums it over all of G. Function.indTerm_eq_of_mk_eq_of_conj gives representative independence for explicitly conjugation-invariant functions over coefficients with zero; Function.indTerm_eq_of_mk_eq specializes it to class functions.

References

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

noncomputable def Function.indTerm {k : Type u} {G : Type v} [Group G] {S : Subgroup G} [Zero k] (f : ↥S → k) (g x : G) : k

The summand of the induced class function attached to a representative x: the value of f at x⁻¹ * g * x when that element lies in the subgroup, and 0 otherwise.

Specialized to the character of a representation of S this is the summand of the induced-character formula TauCeti.character_indFDRep_sum_quotient.

Equations

• Function.indTerm f g x = if h : x⁻¹ * g * x ∈ S then f ⟨x⁻¹ * g * x, h⟩ else 0

theorem Function.indTerm_apply {k : Type u} {G : Type v} [Group G] {S : Subgroup G} [Zero k] (f : ↥S → k) (g x : G) : indTerm f g x = if h : x⁻¹ * g * x ∈ S then f ⟨x⁻¹ * g * x, h⟩ else 0

The defining case split of Function.indTerm.

theorem Function.indTerm_eq_zero_of_smul_mk_ne {k : Type u} {G : Type v} [Group G] {S : Subgroup G} [Zero k] (f : ↥S → k) {g x : G} (h : g • ↑x ≠ ↑x) : indTerm f g x = 0

A summand vanishes unless g fixes the coset of its representative. The conjugate x⁻¹ g x lies in S exactly when g • xS = xS, so only the fixed cosets contribute to Subgroup.indClassFun.

theorem Function.indTerm_conj {k : Type u} {G : Type v} [Group G] {S : Subgroup G} [Zero k] (f : ↥S → k) (g x c : G) : indTerm f (c * g * c⁻¹) x = indTerm f g (c⁻¹ * x)

Conjugating the argument of the summand translates the representative.

theorem Function.indTerm_one {k : Type u} {G : Type v} [Group G] {S : Subgroup G} [Zero k] (f : ↥S → k) (g : G) : indTerm f g 1 = if h : g ∈ S then f ⟨g, h⟩ else 0

The value of the summand at the identity representative.

theorem Function.indTerm_eq_of_mk_eq_of_conj {k : Type u} {G : Type v} [Group G] {S : Subgroup G} [Zero k] (f : ↥S → k) (hf : ∀ (y s : ↥S), f (s * y * s⁻¹) = f y) (g x y : G) (hxy : ↑x = ↑y) : indTerm f g x = indTerm f g y

A conjugation-invariant summand depends only on the left coset of its representative. This form of Function.indTerm_eq_of_mk_eq needs only a zero in the coefficients and an explicit conjugation-invariance hypothesis on f.

noncomputable def Subgroup.indClassFun {k : Type u} {G : Type v} [Group G] [AddCommMonoid k] (S : Subgroup G) [S.FiniteIndex] (f : ↥S → k) : G → k

The induced class function. For f : S → k and g : G, sum f (t⁻¹ g t) over those left coset representatives t of S in G with t⁻¹ g t ∈ S.

The sum has no division by |S|, so the definition needs nothing of the coefficients beyond addition; the averaged group-sum form is Subgroup.indClassFun_eq_natCard_inv_mul_sum. On a character it is the character of the induced representation, by Subgroup.indClassFun_ofFDRep_character.

The representatives are the fixed Quotient.out ones, so this is a function of f alone; and for a conjugation-invariant f the individual summands, and hence the sum, are independent of the representatives chosen. Subgroup.indClassFunction is the bundled form on TauCeti.ClassFunction k S, and is the canonical API.

Equations

• S.indClassFun f g = ∑ t : G ⧸ S, Function.indTerm f g (Quotient.out t)

theorem Subgroup.indClassFun_apply {k : Type u} {G : Type v} [Group G] [AddCommMonoid k] (S : Subgroup G) [S.FiniteIndex] (f : ↥S → k) (g : G) : S.indClassFun f g = ∑ t : G ⧸ S, if h : (Quotient.out t)⁻¹ * g * Quotient.out t ∈ S then f ⟨(Quotient.out t)⁻¹ * g * Quotient.out t, h⟩ else 0

The defining coset sum of Subgroup.indClassFun.

theorem Subgroup.indClassFun_eq_sum_of_smul_eq_self_mem {k : Type u} {G : Type v} [Group G] [AddCommMonoid k] (S : Subgroup G) [S.FiniteIndex] (f : ↥S → k) (g : G) (T : Finset (G ⧸ S)) (hT : ∀ (t : G ⧸ S), g • t = t → t ∈ T) : S.indClassFun f g = ∑ t ∈ T, Function.indTerm f g (Quotient.out t)

The induced class function is a sum over the cosets that g fixes. The summand attached to any other coset vanishes (Function.indTerm_eq_zero_of_smul_mk_ne), so summing over a finite set T of cosets that contains every fixed one already gives the whole sum. In practice T is the set of fixed cosets itself, which for a concrete group is a short explicit list.

Additivity

@[simp]

theorem Subgroup.indClassFun_comp {k : Type u} {G : Type v} [Group G] [AddCommMonoid k] (S : Subgroup G) [S.FiniteIndex] {k' : Type u_1} [AddCommMonoid k'] (φ : k →+ k') (f : ↥S → k) : S.indClassFun (⇑φ ∘ f) = ⇑φ ∘ S.indClassFun f

Induction of functions commutes with every additive map of coefficients. The coset formula uses only addition and zero, so no characteristic or invertibility hypothesis is needed.

@[simp]

theorem Subgroup.indClassFun_zero {k : Type u} {G : Type v} [Group G] [AddCommMonoid k] (S : Subgroup G) [S.FiniteIndex] : S.indClassFun 0 = 0

Induction of functions kills the zero function.

@[simp]

theorem Subgroup.indClassFun_add {k : Type u} {G : Type v} [Group G] [AddCommMonoid k] (S : Subgroup G) [S.FiniteIndex] (f₁ f₂ : ↥S → k) : S.indClassFun (f₁ + f₂) = S.indClassFun f₁ + S.indClassFun f₂

Induction of functions is additive.

noncomputable def Subgroup.indClassFunAddHom {k : Type u} {G : Type v} [Group G] [AddCommMonoid k] (S : Subgroup G) [S.FiniteIndex] : (↥S → k) →+ G → k

Induction of functions on a finite-index subgroup, as an additive map. It is Subgroup.indClassFun bundled by the two lemmas above, which is what lets a property be propagated through the additive generation of an AddSubgroup of functions; Subgroup.indClassFunction is the finer bundling, as a k-linear map on class functions.

Equations

• S.indClassFunAddHom = { toFun := S.indClassFun, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Subgroup.indClassFunAddHom_apply {k : Type u} {G : Type v} [Group G] [AddCommMonoid k] (S : Subgroup G) [S.FiniteIndex] (ψ : ↥S → k) : S.indClassFunAddHom ψ = S.indClassFun ψ

@[simp]

theorem Subgroup.indClassFun_smul {k : Type u} {G : Type v} [Group G] [AddCommMonoid k] (S : Subgroup G) [S.FiniteIndex] {R : Type u_1} [DistribSMul R k] (c : R) (f : ↥S → k) : S.indClassFun (c • f) = c • S.indClassFun f

Induction commutes with any scalar action preserving zero and addition. In particular, this applies to module coefficients without requiring multiplication on the coefficients.

Conjugation invariance and transitivity

@[simp]

theorem Subgroup.indClassFun_conj {k : Type u} {G : Type v} [Group G] [AddCommMonoid k] (S : Subgroup G) [S.FiniteIndex] {f : ↥S → k} (hf : ∀ (y s : ↥S), f (s * y * s⁻¹) = f y) (g c : G) : S.indClassFun f (c * g * c⁻¹) = S.indClassFun f g

Induction preserves conjugation invariance over any additive commutative monoid.

@[simp]

theorem Subgroup.indClassFun_top {k : Type u} {G : Type v} [Group G] [AddCommMonoid k] {f : ↥⊤ → k} (hf : ∀ (y s : ↥⊤), f (s * y * s⁻¹) = f y) (g : G) : ⊤.indClassFun f g = f ⟨g, ⋯⟩

Induction from the whole group is the identity, read along ⊤ ≃ G: the quotient by ⊤ has a single coset. The inducing function need only be conjugation invariant, and the coefficients need only form an additive commutative monoid.

theorem Subgroup.indClassFun_indClassFun_subgroupOf {k : Type u} {G : Type v} [Group G] [AddCommMonoid k] (L : Subgroup G) {T : Subgroup G} (hLT : L ≤ T) [L.FiniteIndex] {f : ↥L → k} (hf : ∀ (y s : ↥L), f (s * y * s⁻¹) = f y) : T.indClassFun ((L.subgroupOf T).indClassFun fun (x : ↥(L.subgroupOf T)) => f ((subgroupOfEquivOfLe hLT) x)) = L.indClassFun f

Transitivity of induction. For subgroups L ≤ T with L of finite index, inducing a conjugation-invariant function of L first to T and then to G is inducing it directly to G: Ind_T^G (Ind_L^T f) = Ind_L^G f. The intermediate step induces from L read as the subgroup L.subgroupOf T of T, with Subgroup.subgroupOfEquivOfLe identifying the two. That T has finite index too follows from L ≤ T (Subgroup.finiteIndex_of_le), so it is not assumed.

Only an additive commutative monoid of coefficients is needed.

The group-sum form

theorem Subgroup.natCard_nsmul_indClassFun {k : Type u} {G : Type v} [Group G] [AddCommMonoid k] (S : Subgroup G) [Fintype G] {f : ↥S → k} (hf : ∀ (y s : ↥S), f (s * y * s⁻¹) = f y) (g : G) : Nat.card ↥S • S.indClassFun f g = ∑ x : G, if h : x⁻¹ * g * x ∈ S then f ⟨x⁻¹ * g * x, h⟩ else 0

The group-sum form of the induced class function, with no division. For a conjugation-invariant function f on S, summing the conjugation summand over all of G rather than over coset representatives adds |S| copies of the induced value. No multiplication on the coefficients is needed.

Conjugation invariance

theorem Function.indTerm_eq_of_mk_eq {k : Type u} {G : Type v} [Group G] {S : Subgroup G} [Semiring k] (f : ↥S → k) (hf : f ∈ TauCeti.ClassFunction k ↥S) (g x y : G) (hxy : ↑x = ↑y) : indTerm f g x = indTerm f g y

For a class function f on S, the induction summand depends only on the left coset of its representative.

theorem Subgroup.indClassFun_mem_classFunction {k : Type u} {G : Type v} [Group G] [Semiring k] (S : Subgroup G) [S.FiniteIndex] {f : ↥S → k} (hf : f ∈ TauCeti.ClassFunction k ↥S) : S.indClassFun f ∈ TauCeti.ClassFunction k G

The induced function of a class function is a class function.

The projection formula

theorem Subgroup.indClassFun_comp_subtype_mul {k : Type u} {G : Type v} [Group G] [Semiring k] {f : G → k} (S : Subgroup G) [S.FiniteIndex] (hf : f ∈ TauCeti.ClassFunction k G) (ψ : ↥S → k) : S.indClassFun ((fun (s : ↥S) => f ↑s) * ψ) = f * S.indClassFun ψ

The projection formula for the induced class function: Ind_S^G ((Res_S f) · ψ) = f · Ind_S^G ψ for a class function f of G and an arbitrary function ψ on S.

This is the class-function shadow of the tensor identity TauCeti.indProjection, and it is what makes induction a map of modules over the ring of class functions: an induced function may be multiplied by f either before or after inducing. Only f is required to be a class function; the identity is pointwise in ψ.

The induced class function as a linear map

noncomputable def Subgroup.indClassFunction {k : Type u} {G : Type v} [Group G] [Semiring k] (S : Subgroup G) [S.FiniteIndex] : ↥(TauCeti.ClassFunction k ↥S) →ₗ[k] ↥(TauCeti.ClassFunction k G)

Induction of class functions, packaged as a k-linear map ClassFunction k S →ₗ[k] ClassFunction k G.

Equations

• S.indClassFunction = { toFun := fun (f : ↥(TauCeti.ClassFunction k ↥S)) => ⟨S.indClassFun ↑f, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Subgroup.indClassFunction_apply {k : Type u} {G : Type v} [Group G] [Semiring k] (S : Subgroup G) [S.FiniteIndex] (f : ↥(TauCeti.ClassFunction k ↥S)) (g : G) : ↑(S.indClassFunction f) g = S.indClassFun (↑f) g

Averaging

theorem Subgroup.indClassFun_eq_natCard_inv_mul_sum {k : Type u} {G : Type v} [Group G] [DivisionSemiring k] (S : Subgroup G) [Fintype G] {f : ↥S → k} (hS : IsUnit ↑(Nat.card ↥S)) (hf : f ∈ TauCeti.ClassFunction k ↥S) (g : G) : S.indClassFun f g = (↑(Nat.card ↥S))⁻¹ * ∑ x : G, if h : x⁻¹ * g * x ∈ S then f ⟨x⁻¹ * g * x, h⟩ else 0

The averaged group-sum form of induction for a class function f on S. The order of the subgroup must be invertible in the coefficient division semiring; without that hypothesis, Subgroup.natCard_nsmul_indClassFun is the division-free identity to use.