The ring structure on the Grothendieck group of a group algebra

Let k be a field and G a finite monoid. The exact Grothendieck group G₀(k[G]) = ExactK0 (finiteModulesExactStructure k[G]) of finitely generated k[G]-modules is the Grothendieck group in which restriction (TauCeti.resK0), induction (TauCeti.indK0) and permutation classes (TauCeti.permK0) live. This file makes it a commutative ring, with

[V] * [W] = [V ⊗ W] and 1 = [k],

the tensor product of representations over k with the diagonal action, and the trivial line.

The tensor product is a structure on representations rather than on k[G]-modules, so the ring structure is the one of the exact Grothendieck ring of FDRep k G (TauCeti.ExactK0.instCommRing with TauCeti.isMonoidal_abelian_fdRep), carried along the exact equivalence TauCeti.fdRepEquivalence : FDRep k G ≌ FGModuleCat k[G]. The resulting identification of the two Grothendieck rings is TauCeti.fdRepK0RingEquiv, sending the class of a representation V to the class of its group-algebra module Representation.asModule V.ρ. The additive structure of G₀(k[G]) is left untouched: only the multiplication and the unit are new.

Restriction along a monoid homomorphism is then multiplicative and unital (TauCeti.resK0_mul, TauCeti.resK0_one), because restricting a tensor product of representations is tensoring the restrictions; bundled, it is the ring homomorphism TauCeti.resK0RingHom.

Implementation notes

When G is commutative, k[G] is a commutative ring and k[G]-modules also have a tensor product over k[G]. That is not the product used here: the product of G₀(k[G]) is the tensor product over k with the diagonal action of G, the one of representations.

Main definitions

• TauCeti.fdRepK0RingEquiv: the exact Grothendieck ring of FDRep k G is isomorphic to G₀(k[G]).
• TauCeti.instCommRingExactK0MonoidAlgebra: the commutative ring structure on G₀(k[G]).
• TauCeti.resK0RingHom: restriction as a ring homomorphism.

Main results

• TauCeti.fdRepK0RingEquiv_of: the class of a representation goes to the class of its group-algebra module.
• TauCeti.of_asModule_mul_of_asModule: the product of the classes of two representations is the class of their tensor product.
• TauCeti.exactK0_one_eq_of_trivial: the unit is the class of the trivial line.
• TauCeti.fdRepK0RingEquiv_hom_ext₂: biadditive maps out of G₀(k[G]) and G₀(k[H]) are determined by their values on pairs of classes of representations.
• TauCeti.resK0_mul and TauCeti.resK0_one: restriction is a ring homomorphism.

References

• J.-P. Serre, Linear Representations of Finite Groups, Springer GTM 42 (1977), §14.1, for the ring R_k(G) of a finite group over a field of arbitrary characteristic.

@[instance_reducible]

noncomputable instance TauCeti.instMulExactK0FGModuleCatMonoidAlgebraFiniteModulesExactStructure (k G : Type u) [Field k] [Monoid G] [Finite G] : Mul (ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G)))

The multiplication of G₀(k[G]): the tensor product of representations, carried along the equivalence TauCeti.fdRepEquivalence. It is characterised by TauCeti.of_asModule_mul_of_asModule.

@[instance_reducible]

noncomputable instance TauCeti.instOneExactK0FGModuleCatMonoidAlgebraFiniteModulesExactStructure (k G : Type u) [Field k] [Monoid G] [Finite G] : One (ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G)))

The unit of G₀(k[G]): the class of the trivial line (TauCeti.exactK0_one_eq_of_trivial).

noncomputable def TauCeti.fdRepK0RingEquiv (k G : Type u) [Field k] [Monoid G] [Finite G] : ExactK0 (ExactStructure.abelian (FDRep k G)) ≃+* ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G))

The Grothendieck ring of FDRep k G is G₀(k[G]). The exact Grothendieck group of the abelian category of finite-dimensional representations is identified with the exact Grothendieck group of finitely generated k[G]-modules by the equivalence TauCeti.fdRepEquivalence, and this identification is multiplicative for the tensor product of representations.

@[simp]

theorem TauCeti.fdRepK0RingEquiv_of {k G : Type u} [Field k] [Monoid G] [Finite G] (V : FDRep k G) : (fdRepK0RingEquiv k G) (ExactK0.of V) = ExactK0.of ↧(Representation.asModule V.ρ)

TauCeti.fdRepK0RingEquiv sends the class of a representation to the class of its group-algebra module.

@[instance_reducible]

noncomputable instance TauCeti.instCommRingExactK0MonoidAlgebra (k G : Type u) [Field k] [Monoid G] [Finite G] : CommRing (ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G)))

G₀(k[G]) is a commutative ring under the tensor product of representations, with unit the class of the trivial line. Its additive group is the exact Grothendieck group of finitely generated k[G]-modules; the ring axioms are those of the Grothendieck ring of FDRep k G, read through TauCeti.fdRepK0RingEquiv.

@[simp]

theorem TauCeti.of_asModule_mul_of_asModule {k G : Type u} [Field k] [Monoid G] [Finite G] (V W : FDRep k G) : ExactK0.of ↧(Representation.asModule V.ρ) * ExactK0.of ↧(Representation.asModule W.ρ) = ExactK0.of ↧(Representation.asModule (CategoryTheory.MonoidalCategoryStruct.tensorObj V W).ρ)

The product of two classes is the class of the tensor product: in G₀(k[G]), [V] * [W] = [V ⊗ W] for finite-dimensional representations V and W.

theorem TauCeti.exactK0_one_eq_of_trivial {k G : Type u} [Field k] [Monoid G] [Finite G] : 1 = ExactK0.of ↧(Representation.trivial k G k).asModule

The unit is the class of the trivial line: in G₀(k[G]), 1 = [k].

theorem TauCeti.fdRepK0RingEquiv_hom_ext₂ {k G H : Type u} [Field k] [Monoid G] [Monoid H] [Finite G] [Finite H] {M : Type u_1} [AddCommGroup M] {f g : ExactK0 (finiteModulesExactStructure (MonoidAlgebra k G)) →+ ExactK0 (finiteModulesExactStructure (MonoidAlgebra k H)) →+ M} (h : ∀ (V : FDRep k G) (W : FDRep k H), (f ((fdRepK0RingEquiv k G) (ExactK0.of V))) ((fdRepK0RingEquiv k H) (ExactK0.of W)) = (g ((fdRepK0RingEquiv k G) (ExactK0.of V))) ((fdRepK0RingEquiv k H) (ExactK0.of W))) : f = g

Biadditive maps are determined on representations. Two biadditive maps out of G₀(k[G]) and G₀(k[H]) agree once they agree on pairs of classes of representations, read through TauCeti.fdRepK0RingEquiv.

theorem TauCeti.resK0_fdRepK0RingEquiv_of {k G H : Type u} [Field k] [Monoid G] [Monoid H] [Finite G] [Finite H] (φ : H →* G) (V : FDRep k G) : (resK0 k φ) ((fdRepK0RingEquiv k G) (ExactK0.of V)) = (fdRepK0RingEquiv k H) (ExactK0.of ((Action.res (FGModuleCat k) φ).obj V))

Restriction of the class of a representation, read through TauCeti.fdRepK0RingEquiv: it is the class of the restricted representation Action.res φ V.

@[simp]

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

Restriction is multiplicative: restricting the class of a tensor product is the product of the restricted classes.

@[simp]

theorem TauCeti.resK0_one {k G H : Type u} [Field k] [Monoid G] [Monoid H] [Finite G] [Finite H] (φ : H →* G) : (resK0 k φ) 1 = 1

Restriction is unital: it sends the class of the trivial line to the class of the trivial line.

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

Restriction as a ring homomorphism G₀(k[G]) →+* G₀(k[H]): the additive map TauCeti.resK0 together with its multiplicativity TauCeti.resK0_mul and unitality TauCeti.resK0_one.

@[simp]

theorem TauCeti.coe_resK0RingHom {k G H : Type u} [Field k] [Monoid G] [Monoid H] [Finite G] [Finite H] (φ : H →* G) : ⇑(resK0RingHom k φ) = ⇑(resK0 k φ)

The underlying function of TauCeti.resK0RingHom is TauCeti.resK0.

@[simp]

theorem TauCeti.coe_addMonoidHom_resK0RingHom {k G H : Type u} [Field k] [Monoid G] [Monoid H] [Finite G] [Finite H] (φ : H →* G) : ↑(resK0RingHom k φ) = resK0 k φ

The underlying additive map of TauCeti.resK0RingHom is TauCeti.resK0.