Semisimple modules are determined by their traces

Let A be an algebra over a field k of characteristic zero. A finite-dimensional semisimple A-module M gives the trace function a ↦ tr_k (a • · : M → M) on A. This file proves that the trace function determines M up to isomorphism (IsSemisimpleModule.nonempty_linearEquiv_of_trace_eq). No finiteness is asked of A, which is the point: for the group algebra of an infinite group, such as GL n ℂ, it is what lets characters determine semisimple representations.

The argument isolates one isotypic type at a time by an element of A. For a semisimple module X finite over its endomorphism ring and a simple module S, the projection of X onto its S-isotypic component along the sum of the other isotypic components commutes with every endomorphism, because isotypic components are fully invariant. Jacobson density then writes it as the action of some a : A (IsSemisimpleModule.exists_forall_smul_eq_ite): a acts as the identity on every simple submodule of X isomorphic to S, and as zero on every other simple submodule. Applied to X = M × N, the trace of a on M is the multiplicity of S in M times the dimension of S, and likewise on N. In characteristic zero equal traces therefore give equal multiplicities, and finite semisimple modules with equal multiplicities are isomorphic (IsSemisimpleModule.nonempty_linearEquiv_of_jordanHolderMultiplicity_eq).

Main results

• IsSemisimpleModule.nonempty_linearEquiv_of_trace_eq: finite-dimensional semisimple modules over an algebra in characteristic zero with the same traces are isomorphic.

References

• S. Lang, Algebra, revised third edition, Chapter XVII, Corollary 3.8.

theorem IsSemisimpleModule.nonempty_linearEquiv_of_trace_eq {k : Type u_1} [Field k] {A : Type u} [Ring A] [Algebra k A] [CharZero k] (M : Type u_2) [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] [FiniteDimensional k M] [IsSemisimpleModule A M] (N : Type u_3) [AddCommGroup N] [Module k N] [Module A N] [IsScalarTower k A N] [FiniteDimensional k N] [IsSemisimpleModule A N] (h : ∀ (a : A), (LinearMap.trace k M) ((Algebra.lsmul k k M) a) = (LinearMap.trace k N) ((Algebra.lsmul k k N) a)) : Nonempty (M ≃ₗ[A] N)

Semisimple modules are determined by their traces. Over an algebra A over a field of characteristic zero, two finite-dimensional semisimple A-modules on which every element of A acts with the same trace are isomorphic. No finiteness is asked of A.