The projection formula in the Grothendieck ring of a group algebra

Let k be a field, G a finite group and S a subgroup. Induction TauCeti.indK0 k S : G₀(k[S]) →+ G₀(k[G]) is not a ring homomorphism, but it is a homomorphism of G₀(k[G])-modules, where G₀(k[S]) is a G₀(k[G])-module through restriction:

Ind_S^G (y · Res_S^G x) = (Ind_S^G y) · x in G₀(k[G])

(TauCeti.indK0_mul_resK0). This is the representation-level projection formula Ind_S^G (A ⊗ Res_S^G B) ≅ (Ind_S^G A) ⊗ B (TauCeti.indFDRepProjection) read on classes, both sides being additive in each variable. It holds in every characteristic, with the relations of G₀(k[G]) coming from all short exact sequences, split or not.

Applied to y = 1, it says that multiplying a class by the permutation class [k[G ⧸ S]], the induction of the unit (TauCeti.indK0_one), is inducing its restriction. This is how an identity among permutation classes, such as Artin's identity, spreads to every class of G₀(k[G]).

Main results

• TauCeti.indK0_fdRepK0RingEquiv_of: induction of the class of a representation, read through TauCeti.fdRepK0RingEquiv, is the class of the induced representation.
• TauCeti.indK0_mul_resK0: the projection formula.
• TauCeti.indK0_one: induction of the unit is the permutation class of the cosets.
• TauCeti.indK0_resK0: inducing a restricted class multiplies it by that permutation class.

References

• J.-P. Serre, Linear Representations of Finite Groups, Springer GTM 42 (1977), §14.1, for restriction, induction and the projection formula on R_k(G) in arbitrary characteristic.

theorem TauCeti.indK0_fdRepK0RingEquiv_of {k G : Type u} [Field k] [Group G] [Finite G] {S : Subgroup G} (A : FDRep k ↥S) : (indK0 k S) ((fdRepK0RingEquiv k ↥S) (ExactK0.of A)) = (fdRepK0RingEquiv k G) (ExactK0.of (indFDRep A))

Induction of the class of a representation, read through TauCeti.fdRepK0RingEquiv: it is the class of the induced representation TauCeti.indFDRep A.

@[simp]

theorem TauCeti.indK0_mul_resK0 {k G : Type u} [Field k] [Group G] [Finite G] {S : Subgroup G} (y : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k ↥S))) (x : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G))) : (indK0 k S) (y * (resK0 k S.subtype) x) = (indK0 k S) y * x

The projection formula in G₀(k[G]), Ind_S^G (y · Res_S^G x) = (Ind_S^G y) · x: induction from a subgroup is a homomorphism of G₀(k[G])-modules, where G₀(k[S]) is a G₀(k[G])-module through restriction.

@[simp]

theorem TauCeti.indK0_one {k G : Type u} [Field k] [Group G] [Finite G] {S : Subgroup G} : (indK0 k S) 1 = permK0 k G (G ⧸ S)

Induction of the unit is the permutation class [k[G ⧸ S]] of the cosets of S.

theorem TauCeti.indK0_resK0 {k G : Type u} [Field k] [Group G] [Finite G] {S : Subgroup G} (x : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G))) : (indK0 k S) ((resK0 k S.subtype) x) = permK0 k G (G ⧸ S) * x

Inducing a restricted class multiplies it by the permutation class of the cosets: Ind_S^G (Res_S^G x) = [k[G ⧸ S]] · x, the projection formula at the unit.