The central character of a simple module

A central element z of a k-algebra A acts on an A-module M by an A-linear map, because z commutes with every scalar; this is the algebra homomorphism TauCeti.centerToEnd. When M is a finite-dimensional simple module over an algebraically closed field k, Schur's lemma collapses the endomorphism algebra to k itself, so the action of the centre is by honest scalars. The resulting k-algebra homomorphism Z(A) → k is the central character of M.

For A = k[G] this is the character-theoretic ωᵪ. Its value on the class sum of a conjugacy class C with representative g is the entry χ(g) of the character table weighted by the class size and normalized by the degree: ωᵪ(K_C) = |C| · χ(g) / χ(1), when χ(1) ≠ 0 in k.

Main definitions

• TauCeti.centerToEnd: a central element of A acts on an A-module by an A-linear endomorphism, as a homomorphism of k-algebras Z(A) →ₐ[k] End_A M. No simplicity or finiteness hypothesis is needed.
• TauCeti.centralCharacter: the central character Z(A) →ₐ[k] k of a finite-dimensional simple module over an algebraically closed field.

Main statements

• TauCeti.smul_eq_centralCharacter_smul: the defining property, that a central element acts as multiplication by its central character.
• TauCeti.centralCharacter_eq_of_smul_eq: the central character is the only scalar with that property, in the form asking for the equality at every vector.
• TauCeti.centralCharacter_eq_of_ne_zero_of_smul_eq: the sharper form, computing the central character from the action on a single nonzero vector.

References

This implements the "central characters" item of Layer 4 of the character theory roadmap, in the generality of a simple module over an arbitrary algebra. See I. M. Isaacs, Character Theory of Finite Groups, Chapter 3, or C. W. Curtis and I. Reiner, Representation Theory of Finite Groups and Associative Algebras, §33.

The action of the centre

def TauCeti.centerToEnd (k : Type u) [CommSemiring k] (A : Type v) [Semiring A] [Algebra k A] (M : Type w) [AddCommMonoid M] [Module A M] [Module k M] [IsScalarTower k A M] : ↥(Subalgebra.center k A) →ₐ[k] Module.End A M

A central element of A acts on an A-module M by an A-linear endomorphism, and doing so is a homomorphism of k-algebras from the centre of A to End_A M.

Centrality is exactly what makes the action A-linear rather than merely additive; Mathlib's Module.End.smulLeft packages the individual endomorphism.

Equations

• TauCeti.centerToEnd k A M = { toFun := fun (z : ↥(Subalgebra.center k A)) => Module.End.smulLeft ↑z ⋯, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem TauCeti.centerToEnd_apply (k : Type u) [CommSemiring k] (A : Type v) [Semiring A] [Algebra k A] (M : Type w) [AddCommMonoid M] [Module A M] [Module k M] [IsScalarTower k A M] (z : ↥(Subalgebra.center k A)) (m : M) : ((centerToEnd k A M) z) m = ↑z • m

The endomorphism attached to a central element is multiplication by it.

The central character of a simple module

noncomputable def TauCeti.centralCharacter (k : Type u) [Field k] [IsAlgClosed k] (A : Type v) [Ring A] [Algebra k A] (M : Type w) [AddCommGroup M] [Module A M] [Module k M] [IsScalarTower k A M] [IsSimpleModule A M] [FiniteDimensional k M] : ↥(Subalgebra.center k A) →ₐ[k] k

The central character of a finite-dimensional simple module M over a k-algebra A, for k algebraically closed: the homomorphism of k-algebras recording the scalar by which each central element of A acts on M.

The scalar exists because the action of a central element is A-linear (TauCeti.centerToEnd) and every A-linear endomorphism of M is a scalar (Schur's lemma, TauCeti.endAlgEquivSelfOfIsSimpleModule).

Equations

• TauCeti.centralCharacter k A M = (↑TauCeti.endAlgEquivSelfOfIsSimpleModule).comp (TauCeti.centerToEnd k A M)

@[simp]

theorem TauCeti.smul_eq_centralCharacter_smul (k : Type u) [Field k] [IsAlgClosed k] (A : Type v) [Ring A] [Algebra k A] (M : Type w) [AddCommGroup M] [Module A M] [Module k M] [IsScalarTower k A M] [IsSimpleModule A M] [FiniteDimensional k M] (z : ↥(Subalgebra.center k A)) (m : M) : ↑z • m = (centralCharacter k A M) z • m

The defining property of the central character: a central element acts on the module as multiplication by the scalar the central character assigns to it.

This is the simp normal form: the opaque action of the centre is replaced by the action of a scalar, which is the whole point of the construction.

theorem TauCeti.centralCharacter_eq_of_ne_zero_of_smul_eq {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] {M : Type w} [AddCommGroup M] [Module A M] [Module k M] [IsScalarTower k A M] [IsSimpleModule A M] [FiniteDimensional k M] {z : ↥(Subalgebra.center k A)} {c : k} {m : M} (hm : m ≠ 0) (h : ↑z • m = c • m) : (centralCharacter k A M) z = c

The central character is determined by the action of a central element on a single nonzero vector: no other scalar can reproduce it there.

theorem TauCeti.centralCharacter_eq_of_smul_eq {k : Type u} [Field k] [IsAlgClosed k] {A : Type v} [Ring A] [Algebra k A] {M : Type w} [AddCommGroup M] [Module A M] [Module k M] [IsScalarTower k A M] [IsSimpleModule A M] [FiniteDimensional k M] {z : ↥(Subalgebra.center k A)} {c : k} (h : ∀ (m : M), ↑z • m = c • m) : (centralCharacter k A M) z = c

The central character is the unique scalar by which a central element acts.

A simple module is nonzero, which is what rules out the degenerate case where every scalar would qualify.