The action of a class sum on a representation

A representation of a finite group G extends to the group algebra, so each class sum K_C acts on it. This file computes that action and its trace: the action is the sum of the actions of the members of the class, and, the character being constant on a conjugacy class, the trace is the size of the class times the character value there.

Neither statement needs irreducibility or an algebraically closed field; they are the traces that turn the defining scalar identity of a central character into the class-sum formula ωᵪ(K_C) · χ(1) = |C| · χ(g).

Main statements

• TauCeti.Representation.asAlgebraHom_classSum: a class sum acts by the sum of the actions of the elements of the class.
• TauCeti.Representation.trace_asAlgebraHom_classSum: the trace of that action is |C| · χ(g) for any g in C.

Implementation notes

These declarations live in TauCeti.Representation, not in the root Representation namespace, so dot notation on a representation does not reach them.

theorem TauCeti.Representation.asAlgebraHom_classSum {k : Type u} {G : Type v} {V : Type w} [Group G] [Fintype G] [DecidableEq G] [CommSemiring k] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (C : ConjClasses G) : ρ.asAlgebraHom (classSum k C) = ∑ x : ↑C.carrier, ρ ↑x

A class sum acts on a representation by the sum of the actions of the elements of the class.

theorem TauCeti.Representation.trace_asAlgebraHom_classSum {k : Type u} {G : Type v} {V : Type w} [Group G] [Fintype G] [DecidableEq G] [Field k] [AddCommGroup V] [Module k V] (ρ : Representation k G V) {C : ConjClasses G} {g : G} (hg : ConjClasses.mk g = C) : (LinearMap.trace k V) (ρ.asAlgebraHom (classSum k C)) = ↑(Nat.card ↑C.carrier) * ρ.character g

The character is constant on a conjugacy class, so the trace of the action of a class sum is the size of the class times the character value there.