Induction between Grothendieck groups of group algebras

Let S be a subgroup of a finite group G and k a commutative ring. The group algebra k[G] is a free k[S]-module of finite rank, with a basis indexed by the cosets of S (TauCeti.MonoidAlgebra.basisCosets). Hence coextension of scalars M ↦ Hom_{k[S]}(k[G], M) is exact and preserves finite generation, and it descends to the exact Grothendieck groups of finitely generated modules:

ind S : G₀(k[S]) →+ G₀(k[G]),   [M] ↦ [Hom_{k[S]}(k[G], M)].

The module Hom_{k[S]}(k[G], M) is the coinduced module, and since S has finite index it is isomorphic to the induced module. So on the class of a representation ρ of S, ind S is the class of the induced representation Ind_S^G ρ (TauCeti.indK0_of_asModule_of_equiv), in particular of Tau Ceti's finite-dimensional induction TauCeti.indFDRep over a field (TauCeti.indK0_of_indFDRep), and the class of the trivial line goes to the class of the permutation module k[G ⧸ S], that is, to the permutation class TauCeti.permK0 k G (G ⧸ S) (TauCeti.indK0_of_trivial).

The exactness of induction is what makes ind S well defined on the exact Grothendieck group, whose relations come from all short exact sequences, including the non-split ones that occur when the characteristic of k divides the order of G.

Induction is transitive: for subgroups S ≤ T of G, inducing from S to T and then to G is inducing from S to G (TauCeti.indK0_indK0). Since G₀ of a subgroup of T is indexed by S.subgroupOf T rather than by S, the statement transports classes between the two along the isomorphism Subgroup.subgroupOfEquivOfLe, by restriction (TauCeti.resK0).

Main definitions

• TauCeti.indK0: induction from a subgroup as a homomorphism of exact Grothendieck groups of finitely generated group-algebra modules.

Main results

• TauCeti.indK0_of: the class of a module goes to the class of its coinduced module.
• TauCeti.indK0_of_asModule_of_equiv: the class of a representation goes to the class of any representation equivalent to its induced representation.
• TauCeti.indK0_of_trivial: the class of the trivial line goes to the permutation class of the cosets.
• TauCeti.indK0_of_ofMulAction_quotient: for D ≤ S, the class of the permutation module k[S ⧸ (D ⊓ S)] goes to the class of the permutation module k[G ⧸ D].
• TauCeti.indK0_of_indFDRep: over a field, the class of a finite-dimensional representation goes to the class of TauCeti.indFDRep of it.
• TauCeti.indK0_comp_indK0 and TauCeti.indK0_indK0: induction is transitive along a chain of subgroups S ≤ T ≤ G.

References

• J.-P. Serre, Linear Representations of Finite Groups, Part III, §14.1, for the induction homomorphism R_k(H) → R_k(G).

noncomputable def TauCeti.indK0 (k : Type u) [CommRing k] {G : Type u} [Group G] [Finite G] (S : Subgroup G) : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k ↥S)) →+ ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G))

Induction on the Grothendieck group of a group algebra. For a subgroup S of a finite group G, coinduction M ↦ Hom_{k[S]}(k[G], M) of finitely generated k[S]-modules is exact, so it induces G₀(k[S]) →+ G₀(k[G]). Since S has finite index, the coinduced module is the induced one (TauCeti.indK0_of_asModule_of_equiv).

@[simp]

theorem TauCeti.indK0_of (k : Type u) [CommRing k] {G : Type u} [Group G] [Finite G] (S : Subgroup G) (M : FGModuleCat (MonoidAlgebra k ↥S)) : (indK0 k S) (ExactK0.of M) = ExactK0.of (((MonoidAlgebra.mapDomainAlgHom k k S.subtype).finiteModulesCoextendScalars ⋯ ⋯).obj M)

Induction sends the class of a module M to the class of its coinduced module Hom_{k[S]}(k[G], M).

theorem TauCeti.indK0_of_asModule_of_equiv (k : Type u) [CommRing k] {G : Type u} [Group G] [Finite G] (S : Subgroup G) {V W : Type u} [AddCommGroup V] [Module k V] [Module.Finite k V] [AddCommGroup W] [Module k W] (ρ : Representation k (↥S) V) (σ : Representation k G W) (e : (Representation.ind S.subtype ρ).Equiv σ) : (indK0 k S) (ExactK0.of ↧ρ.asModule) = ExactK0.of ↧σ.asModule

Induction of the class of a representation. If σ is a representation of G equivalent to the representation induced from a representation ρ of S, then induction sends the class of the k[S]-module of ρ to the class of the k[G]-module of σ. The space of σ is finite over k because the induced space is.

@[simp]

theorem TauCeti.indK0_of_trivial (k : Type u) [CommRing k] {G : Type u} [Group G] [Finite G] (S : Subgroup G) : (indK0 k S) (ExactK0.of ↧(Representation.trivial k (↥S) k).asModule) = permK0 k G (G ⧸ S)

Induction of the trivial line. Induction from S sends the class of the trivial one-dimensional representation to the permutation class of G ⧸ S, the class of the permutation module k[G ⧸ S].

@[simp]

theorem TauCeti.indK0_of_ofMulAction_quotient (k : Type u) [CommRing k] {G : Type u} [Group G] [Finite G] (S : Subgroup G) {D : Subgroup G} (h : D ≤ S) : (indK0 k S) (ExactK0.of ↧(Representation.ofMulAction k (↥S) (↥S ⧸ D.subgroupOf S)).asModule) = ExactK0.of ↧(Representation.ofMulAction k G (G ⧸ D)).asModule

Induction of a coset permutation module. For a subgroup D ≤ S, induction from S sends the class of the permutation module k[S ⧸ (D ⊓ S)] to the class of the permutation module k[G ⧸ D].

theorem TauCeti.indK0_comp_indK0 (k : Type u) [CommRing k] {G : Type u} [Group G] [Finite G] (S : Subgroup G) {T : Subgroup G} (h : S ≤ T) : (indK0 k T).comp (indK0 k (S.subgroupOf T)) = (indK0 k S).comp (resK0 k (Subgroup.subgroupOfEquivOfLe h).symm.toMonoidHom)

Induction is transitive. For subgroups S ≤ T of G, inducing from S.subgroupOf T to T and then from T to G is inducing from S to G, after transporting classes from S.subgroupOf T to S by restriction along Subgroup.subgroupOfEquivOfLe.

theorem TauCeti.indK0_indK0 (k : Type u) [CommRing k] {G : Type u} [Group G] [Finite G] (S : Subgroup G) {T : Subgroup G} (h : S ≤ T) (x : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k ↥(S.subgroupOf T)))) : (indK0 k T) ((indK0 k (S.subgroupOf T)) x) = (indK0 k S) ((resK0 k (Subgroup.subgroupOfEquivOfLe h).symm.toMonoidHom) x)

Induction is transitive, on classes: TauCeti.indK0_comp_indK0 evaluated at x.

@[simp]

theorem TauCeti.indK0_of_indFDRep (k : Type u) [Field k] {G : Type u} [Group G] [Finite G] {S : Subgroup G} (A : FDRep k ↥S) : (indK0 k S) (ExactK0.of ↧(Representation.asModule A.ρ)) = ExactK0.of ↧(Representation.asModule (indFDRep A).ρ)

Induction of a finite-dimensional representation. Over a field, induction from S sends the class of a finite-dimensional representation A of S to the class of the induced representation TauCeti.indFDRep A.