The representation ring and its character homomorphism

The representation ring R(G) of a monoid G over a field k is the split Grothendieck ring of the finite-dimensional representations FDRep k G: its underlying additive group is generated by the classes [V] of objects subject only to [V ⊕ W] = [V] + [W], and its multiplication is induced by the tensor product, so that [V] · [W] = [V ⊗ W] with unit the class of the trivial one-dimensional representation.

Split is meant literally, and for a general k and G it is a restriction: the relations imposed are those of the direct sums, not those of all short exact sequences, so what is built here is the ring also known as the Green ring of G over k, and not in general the Grothendieck ring of the abelian category FDRep k G. The two coincide exactly when every short exact sequence of finite-dimensional representations splits — for a finite group G whose order is invertible in k that is Maschke's theorem, while for a general monoid, or in modular characteristic, they differ. Everything below is a statement about the split ring.

Both structures are already available: TauCeti.SplitK0 is exactly the group presented by the biproduct relations, and TauCeti.SplitK0.instCommRing puts the tensor multiplication on it for any braided monoidal additive category. What was missing is that FDRep k G satisfies the smallness hypothesis those constructions ask for, which TauCeti/CategoryTheory/Action/EssentiallySmall.lean supplies, so TauCeti.repRing here is a name for TauCeti.SplitK0 (FDRep k G) rather than a second construction; every lemma about split K₀ applies to it verbatim.

On top of that this file builds the character homomorphism TauCeti.repRingCharacter, the ring homomorphism R(G) → (G → k) sending [V] to FDRep.character V. That the character descends to R(G) at all is the conjunction of three facts about it: it is an isomorphism invariant (FDRep.char_iso), it is additive on biproducts (FDRep.char_biprod), and it is multiplicative on tensor products (FDRep.char_tensor), the unit going to the constant function 1 (FDRep.char_tensorUnit). Its image is described exactly: it is the virtual-character lattice TauCeti.virtualCharacters, and in particular, when G is a group, so that conjugation and hence the class functions make sense, every value is a class function.

For a finite group G over an algebraically closed field of characteristic zero, injectivity is proved in TauCeti/RepresentationTheory/RepresentationRing/Injective.lean as TauCeti.repRingCharacter_injective. Its object-level input, FDRep.nonempty_iso_of_character_eq, says that equal characters determine isomorphic representations. Outside the finite semisimple regime — for a monoid, or in modular characteristic — injectivity is not to be expected in general.

Main definitions

• TauCeti.repRing: the representation ring R(G).
• TauCeti.repRingCharacter: the character homomorphism R(G) →+* (G → k).

Main statements

• TauCeti.repRingCharacter_of: the character homomorphism sends the class of a representation to its character, and TauCeti.repRingCharacter_unique says it is the only ring homomorphism that does.
• TauCeti.repRingCharacter_mem_virtualCharacters and TauCeti.range_repRingCharacter: its image is the virtual-character lattice, with TauCeti.mem_range_repRingCharacter_iff the elementwise form.
• TauCeti.repRingCharacter_mem_classFunction: for a group G, every value of the character homomorphism is a class function, elementwise TauCeti.repRingCharacter_conj.

References

This builds the objects pinned as repRing, repRingCharacter, repRingCharacter_mem_classFunction in Layer 5 of TauCetiRoadmap/RepresentationTheory/CharacterTheory/README.md ("the representation ring and tensor decomposition"), which is also the first bullet of Layer 6 of TauCetiRoadmap/RepresentationTheory/InductionRestriction/README.md ("the representation ring and its character map").

@[reducible, inline]

abbrev TauCeti.repRing (k : Type u) (G : Type v) [Field k] [Monoid G] : Type (max u v)

The representation ring R(G) of a monoid G over a field k: the split Grothendieck ring of FDRep k G, with addition induced by the direct sum and multiplication by the tensor product.

It is a name for the split Grothendieck group of FDRep k G, whose ring structure TauCeti.SplitK0.instCommRing already supplies, so that TauCeti.SplitK0.of is the class map, TauCeti.SplitK0.of_mul_of the computation rule [V] · [W] = [V ⊗ W], and TauCeti.SplitK0.induction_on the induction principle. Splitting the classes only along biproducts is deliberate: FDRep k G is abelian, so one could instead impose the relation of every short exact sequence, but the representation ring is the one where [V] = [V'] + [V''] holds for a split extension. The two presentations agree for a finite group G whose order is invertible in k, every short exact sequence of representations then splitting by Maschke's theorem; for a general monoid G, or in modular characteristic, they differ and this is the split one, the Green ring of G over k.

Equations

• TauCeti.repRing k G = TauCeti.SplitK0 (FDRep k G)

noncomputable def TauCeti.repRingCharacter (k : Type u) (G : Type v) [Field k] [Monoid G] : repRing k G →+* G → k

The character homomorphism of the representation ring: the ring homomorphism R(G) →+* (G → k) sending the class of a representation to its character.

It is a homomorphism of rings, not merely of groups, because the character is multiplicative under the tensor product (FDRep.char_tensor) and takes the tensor unit to the constant function 1 (FDRep.char_tensorUnit).

Equations

• TauCeti.repRingCharacter k G = TauCeti.SplitK0.liftRingHom (TauCeti.characterInvariant✝ k G) ⋯ ⋯

@[simp]

theorem TauCeti.repRingCharacter_of {k : Type u} {G : Type v} [Field k] [Monoid G] (V : FDRep k G) : (repRingCharacter k G) (SplitK0.of V) = V.character

The character homomorphism sends the class of a representation to its character.

theorem TauCeti.repRingCharacter_unique {k : Type u} {G : Type v} [Field k] [Monoid G] (f : repRing k G →+* G → k) (hf : ∀ (V : FDRep k G), f (SplitK0.of V) = V.character) : f = repRingCharacter k G

The character homomorphism is the unique ring homomorphism computing characters on the classes of objects; this is TauCeti.SplitK0.ringHom_ext for the representation ring.

theorem TauCeti.repRingCharacter_mem_virtualCharacters {k : Type u} {G : Type v} [Field k] [Monoid G] (x : repRing k G) : (repRingCharacter k G) x ∈ virtualCharacters k G

Every value of the character homomorphism is a virtual character: the classes of objects generate R(G), and the virtual characters are an additive subgroup containing every character.

@[simp]

theorem TauCeti.range_repRingCharacter (k : Type u) (G : Type v) [Field k] [Monoid G] : (↑(repRingCharacter k G)).range = virtualCharacters k G

The image of the character homomorphism is the virtual-character lattice. Both sides are the additive subgroup generated by the characters: the left because the classes of objects generate R(G) (TauCeti.SplitK0.closure_range_of), the right by definition.

theorem TauCeti.mem_range_repRingCharacter_iff {k : Type u} {G : Type v} [Field k] [Monoid G] {f : G → k} : f ∈ (↑(repRingCharacter k G)).range ↔ f ∈ virtualCharacters k G

A function is a value of the character homomorphism exactly when it is a virtual character.

theorem TauCeti.repRingCharacter_mem_classFunction {k : Type u} {G : Type v} [Field k] [Group G] (x : repRing k G) : (repRingCharacter k G) x ∈ ClassFunction k G

Every value of the character homomorphism is a class function. A character is constant on conjugacy classes, and the class functions form an additive subgroup, so the whole image is contained in them; this is TauCeti.virtualCharacters_le_classFunction read through TauCeti.range_repRingCharacter.

@[simp]

theorem TauCeti.repRingCharacter_conj {k : Type u} {G : Type v} [Field k] [Group G] (x : repRing k G) (g h : G) : (repRingCharacter k G) x (h * g * h⁻¹) = (repRingCharacter k G) x g

The character homomorphism is invariant under conjugating the argument, the elementwise form of TauCeti.repRingCharacter_mem_classFunction; compare FDRep.char_conj.