Restriction between Grothendieck groups of group algebras

Let k be a ring and φ : H →* G a homomorphism of monoids with G finite. A k[G]-module becomes a k[H]-module through the ring homomorphism MonoidAlgebra.mapDomainRingHom k φ : k[H] →+* k[G]. Since k[G] is a finitely generated k-module, it is also a finitely generated k[H]-module (TauCeti.MonoidAlgebra.mapDomainRingHom_moduleFinite_of_finite), so this restriction of scalars sends finitely generated modules to finitely generated modules (RingHom.finiteModulesK0Restrict). It does not change the underlying groups, so it is exact, and it descends to the exact Grothendieck groups:

res φ : G₀(k[G]) →+ G₀(k[H]),   [M] ↦ [M viewed as a k[H]-module through φ].

When k is commutative, for a representation ρ of G this is the class of the composite representation ρ ∘ φ, so it is restriction of representations to a subgroup, and inflation from a quotient. It is contravariantly functorial in φ and, over a field with H finite too, preserves the dimension of a class. Neither H nor k need be finite for the map itself, and H need not be a subgroup: φ is an arbitrary monoid homomorphism into a finite monoid.

Main definitions

• TauCeti.resK0: restriction along φ : H →* G as a homomorphism of exact Grothendieck groups of finitely generated group-algebra modules.

Main results

• TauCeti.resK0_of: the class of a module goes to the class of its restriction of scalars.
• TauCeti.resK0_of_asModule: the class of a representation goes to the class of its composite with φ; in particular TauCeti.resK0_of_trivial, the trivial line goes to the trivial line.
• TauCeti.resK0_id and TauCeti.resK0_comp: restriction is contravariantly functorial.
• TauCeti.finrankK0_resK0: restriction preserves the dimension of a class.

References

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

noncomputable def TauCeti.resK0 (k : Type u) [Ring k] {G H : Type u} [Monoid G] [Monoid H] [Finite G] (φ : H →* G) : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G)) →+ ExactK0 (finiteModulesExactStructure (MonoidAlgebra k H))

Restriction on the Grothendieck group of a group algebra. For a monoid homomorphism φ : H →* G with G finite, viewing a finitely generated k[G]-module as a k[H]-module through φ induces G₀(k[G]) →+ G₀(k[H]). When k is commutative, on the class of a representation ρ of G it is the class of ρ ∘ φ (TauCeti.resK0_of_asModule).

@[simp]

theorem TauCeti.resK0_of (k : Type u) [Ring k] {G H : Type u} [Monoid G] [Monoid H] [Finite G] (φ : H →* G) (M : FGModuleCat (MonoidAlgebra k G)) : (resK0 k φ) (ExactK0.of M) = ExactK0.of (((MonoidAlgebra.mapDomainRingHom k φ).finiteModulesRestrictScalars ⋯).obj M)

Restriction sends the class of a module to the class of the same module with scalars restricted along φ.

@[simp]

theorem TauCeti.resK0_id (k : Type u) [Ring k] {G : Type u} [Monoid G] [Finite G] : resK0 k (MonoidHom.id G) = AddMonoidHom.id (ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G)))

Restriction along the identity homomorphism is the identity.

@[simp]

theorem TauCeti.resK0_comp (k : Type u) [Ring k] {G H K : Type u} [Monoid G] [Monoid H] [Monoid K] [Finite G] [Finite K] (φ : H →* G) (ψ : G →* K) : resK0 k (ψ.comp φ) = (resK0 k φ).comp (resK0 k ψ)

Restriction is contravariantly functorial: restricting along ψ ∘ φ is restricting along ψ and then along φ.

@[simp]

theorem TauCeti.resK0_of_asModule (k : Type u) [CommRing k] {G H : Type u} [Monoid G] [Monoid H] [Finite G] (φ : H →* G) {V : Type u} [AddCommGroup V] [Module k V] [Module.Finite k V] (ρ : Representation k G V) : (resK0 k φ) (ExactK0.of ↧ρ.asModule) = ExactK0.of ↧(Representation.asModule (MonoidHom.comp ρ φ))

Restriction of the class of a representation. Restricting the class of the k[G]-module of a representation ρ along φ gives the class of the k[H]-module of the composite representation ρ ∘ φ.

@[simp]

theorem TauCeti.resK0_of_trivial (k : Type u) [CommRing k] {G H : Type u} [Monoid G] [Monoid H] [Finite G] (φ : H →* G) : (resK0 k φ) (ExactK0.of ↧(Representation.trivial k G k).asModule) = ExactK0.of ↧(Representation.trivial k H k).asModule

Restriction sends the class of the trivial line to the class of the trivial line.

@[simp]

theorem TauCeti.finrankK0_resK0 (k : Type u) [Field k] {G H : Type u} [Monoid G] [Monoid H] [Finite G] [Finite H] (φ : H →* G) (x : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G))) : (finrankK0 k (MonoidAlgebra k H)) ((resK0 k φ) x) = (finrankK0 k (MonoidAlgebra k G)) x

Restriction preserves dimension. Over a field, for finite monoids H and G, the k-dimension of the restriction of a class along φ : H →* G is the dimension of the class.