The trace of multiplication by an element of a finite monoid algebra

For a finite monoid G the monoid algebra k[G] is free on the monoid elements, so multiplication by a fixed element x is an endomorphism of a finite free module and has a trace. In the basis of monoid elements the matrix of right multiplication by x has g-th diagonal entry x_1, because g * h = g forces h = 1 as soon as G cancels on the left; the trace is therefore |G| * x_1, and it sees nothing of x beyond its coefficient at the identity. The same count on the left needs cancellation on the right and gives the same answer, in the matrix form TauCeti.trace_leftMulMatrix_monoidAlgebra that the character-table files consume. A group cancels on both sides, so all three statements apply to a finite group algebra.

The special case x = g recovers the character of the regular representation, but the general statement is what identifies the scalar in an essential idempotence c * c = a • c, by pairing with TauCeti.LinearMap.trace_eq_mul_finrank_range.

Multiplying on both sides at once, the endomorphism x ↦ g * x * y of a finite group algebra has σ-th diagonal entry y_{σ⁻¹ g⁻¹ σ}, so its trace is the sum of the coefficients of y along the conjugates of g⁻¹, each conjugate counted once for every element conjugating g⁻¹ to it. Over a field k, if y * y = κ • y, this trace is κ times the character of the left ideal k[G] y.

Main statements

• TauCeti.trace_leftMulMatrix_monoidAlgebra: the matrix form, the trace of the left regular matrix of x is |G| * x_1.
• TauCeti.MonoidAlgebra.trace_mulRight: the trace of right multiplication by x on k[G] is |G| * x_1.
• TauCeti.MonoidAlgebra.trace_mulLeft: the same for left multiplication.
• MonoidAlgebra.trace_mulLeft_single_mul_mulRight: the trace of x ↦ g * x * y on a finite group algebra is ∑ σ, y_{σ⁻¹ g⁻¹ σ}.

@[simp]

theorem TauCeti.trace_leftMulMatrix_monoidAlgebra {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] [IsRightCancelMul G] [Fintype G] [DecidableEq G] (x : MonoidAlgebra k G) : ((Algebra.leftMulMatrix (MonoidAlgebra.basis G k)) x).trace = ↑(Fintype.card G) * x.coeff 1

The regular trace reads off the coefficient at the identity. Every diagonal entry of the left regular matrix of x is the coefficient of x at 1, so the trace is |G| times it.

@[simp]

theorem TauCeti.MonoidAlgebra.trace_mulRight {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] [IsLeftCancelMul G] [Finite G] (x : MonoidAlgebra k G) : (LinearMap.trace k (MonoidAlgebra k G)) (LinearMap.mulRight k x) = ↑(Nat.card G) * x.coeff 1

The trace of right multiplication on a finite monoid algebra. Multiplication on the right by x has trace |G| * x_1.

@[simp]

theorem TauCeti.MonoidAlgebra.trace_mulLeft {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] [IsRightCancelMul G] [Finite G] (x : MonoidAlgebra k G) : (LinearMap.trace k (MonoidAlgebra k G)) (LinearMap.mulLeft k x) = ↑(Nat.card G) * x.coeff 1

The trace of left multiplication on a finite monoid algebra. Multiplication on the left by x has trace |G| * x_1, the same as multiplication on the right.

@[simp]

theorem MonoidAlgebra.trace_mulLeft_single_mul_mulRight {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] [Fintype G] (g : G) (y : MonoidAlgebra k G) : (LinearMap.trace k (MonoidAlgebra k G)) (LinearMap.mulLeft k (single g 1) * LinearMap.mulRight k y) = ∑ σ : G, y.coeff (σ⁻¹ * g⁻¹ * σ)

The trace of a two-sided multiplication on a finite group algebra. The endomorphism x ↦ g * x * y of k[G] has trace ∑ σ, y_{σ⁻¹ g⁻¹ σ}: its diagonal entry at σ is the coefficient of σ in g σ y.