The Grothendieck ring of finite-dimensional representations

Let G be a monoid and k a field. Tensoring with a fixed finite-dimensional representation, on either side, carries short exact sequences in FDRep k G to short exact sequences: the forgetful functor to k-modules is faithful, exact and monoidal, and every k-module is flat. So the canonical exact structure on the abelian category FDRep k G is monoidal, and its exact Grothendieck group, the free abelian group on the classes [V] modulo [V₂] = [V₁] + [V₃] for every short exact sequence 0 → V₁ → V₂ → V₃ → 0, is a commutative ring with [V] * [W] = [V ⊗ W] (TauCeti.ExactK0.instCommRing).

For a finite group this is the ring R_k(G) = G₀(k[G]) of Serre, Part III, in every characteristic. The comparison TauCeti.ExactK0.fromSplitRingHom from the split Grothendieck ring TauCeti.repRing k G is a ring homomorphism whose underlying additive map is the surjection TauCeti.ExactK0.fromSplit; it need not be injective when the characteristic of k divides the order of G, since short exact sequences of representations then need not split.

Main results

• FDRep.shortExact_map_tensorLeft, FDRep.shortExact_map_tensorRight: tensoring with a fixed representation preserves short exact sequences.
• TauCeti.isMonoidal_abelian_fdRep: the canonical exact structure on FDRep k G is monoidal, so its exact K₀ is a commutative ring.

References

• J.-P. Serre, Linear Representations of Finite Groups, Springer GTM 42 (1977), §14.1.

theorem FDRep.shortExact_map_tensorLeft {k : Type u} {G : Type v} [Field k] [Monoid G] {S : CategoryTheory.ShortComplex (FDRep k G)} (hS : S.ShortExact) (V : FDRep k G) : (S.map (CategoryTheory.MonoidalCategory.tensorLeft V)).ShortExact

Tensoring on the left is exact. Tensoring with a fixed finite-dimensional representation on the left carries a short exact sequence of representations to a short exact sequence.

theorem FDRep.shortExact_map_tensorRight {k : Type u} {G : Type v} [Field k] [Monoid G] {S : CategoryTheory.ShortComplex (FDRep k G)} (hS : S.ShortExact) (V : FDRep k G) : (S.map (CategoryTheory.MonoidalCategory.tensorRight V)).ShortExact

Tensoring on the right is exact. Tensoring with a fixed finite-dimensional representation on the right carries a short exact sequence of representations to a short exact sequence.

instance TauCeti.isMonoidal_abelian_fdRep {k : Type u} {G : Type v} [Field k] [Monoid G] : (ExactStructure.abelian (FDRep k G)).IsMonoidal

The tensor product of finite-dimensional representations is biexact. The canonical exact structure on FDRep k G is monoidal, so its exact Grothendieck group is a commutative ring under the tensor product.