Identifying the Schur scalar by its trace #
The scalar through which a class-function element acts on an
irreducible representation is determined by the character pairing:
z · dim V = ∑ g, c g · χ_ρ(g).
theorem
RS.trace_asAlgebraHom_classElem
{G : Type u_1}
{V : Type u_2}
[Group G]
[Fintype G]
[AddCommGroup V]
[Module ℂ V]
(ρ : Representation ℂ G V)
(c : G → ℂ)
:
The trace of the action of a class element is the character pairing.
theorem
RS.classElem_scalar_eq
{G : Type u_1}
{V : Type u_2}
[Group G]
[Fintype G]
[AddCommGroup V]
[Module ℂ V]
[FiniteDimensional ℂ V]
{ρ : Representation ℂ G V}
(hirr : IsIrredRep ρ)
(c : G → ℂ)
(hc : ∀ (g h : G), c (h * g * h⁻¹) = c g)
:
ρ.asAlgebraHom (classElem c) = ((∑ g : G, c g * ρ.character g) / ↑(Module.finrank ℂ V)) • LinearMap.id
The identified scalar action: a class-function element acts on an irreducible representation as the character-pairing scalar divided by the dimension.