The central character of an irreducible representation

The centre of k[G] acts on an irreducible representation by scalars: a central element acts by an intertwiner, and Schur's lemma over an algebraically closed field leaves only scalars. Recording those scalars is the central character ωᵪ : Z(k[G]) →ₐ[k] k of the representation, the general construction TauCeti.centralCharacter read on ρ.asModule.

Its values on the class sums are the character-theoretic content: taking traces in ρ(K_C) = ωᵪ(K_C) · id turns the defining scalar identity into ωᵪ(K_C) · χ(1) = |C| · χ(g) for any g in the class C. That identity is stated here without division, so that it holds over every algebraically closed field; dividing by the degree χ(1) needs it to be invertible, which it is in characteristic zero.

Because the class sums are integral over ℤ and an algebra homomorphism preserves integrality, every value ωᵪ(K_C) is an algebraic integer. This is the input to the divisibility χ(1) ∣ |G| and to the Dixon-Schneider algorithm, where the row C ↦ ωᵪ(K_C) is a common left eigenrow of the class-multiplication matrices; that eigenrow property holds of any algebra homomorphism out of the centre, and is TauCeti.isClassEigenrow_classSumRow applied to a central character.

Main definitions

• TauCeti.Representation.centralCharacter: the central character of an irreducible representation, a k-algebra homomorphism out of the centre of the group algebra.

Main statements

• TauCeti.Representation.asAlgebraHom_center_apply: a central element of the group algebra acts on the representation as the scalar its central character records, and TauCeti.Representation.centralCharacter_eq_of_ne_zero_of_asAlgebraHom_apply_eq: that scalar is the only one doing so at a single nonzero vector.
• TauCeti.Representation.centralCharacter_classSumCenter_mul_character_one: the class-sum identity ωᵪ(K_C) · χ(1) = |C| · χ(g), in its division-free form, with TauCeti.Representation.centralCharacter_classSumCenter the quotient form for an invertible degree.
• TauCeti.Representation.centralCharacter_eq_of_equiv: equivalent irreducible representations have the same central character.
• TauCeti.Representation.isIntegral_centralCharacter_classSumCenter: the values of the central character on the class sums are algebraic integers.
• TauCeti.Representation.centralCharacter_trivial_classSumCenter: the worked case of the trivial representation, where the value on a class sum is the size of the class.

Implementation notes

These declarations live in TauCeti.Representation, not in the root Representation namespace, so dot notation on a representation does not reach them: they are applied as centralCharacter ρ.

References

This implements the "central characters, integrally" item of Layer 4 of the character theory roadmap. See I. M. Isaacs, Character Theory of Finite Groups, Chapter 3, or J.-P. Serre, Linear Representations of Finite Groups, Section 6.5.

The central character

noncomputable def TauCeti.Representation.centralCharacter {k : Type u} {G : Type v} {V : Type w} [Field k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) [IsAlgClosed k] [FiniteDimensional k V] [ρ.IsIrreducible] : ↥(Subalgebra.center k (MonoidAlgebra k G)) →ₐ[k] k

The central character of an irreducible representation: the algebra homomorphism recording the scalar by which each central element of the group algebra acts.

An irreducible representation is a simple k[G]-module, so this is TauCeti.centralCharacter for the algebra k[G]; the roadmap writes it ωᵪ.

Equations

• TauCeti.Representation.centralCharacter ρ = TauCeti.centralCharacter k (MonoidAlgebra k G) ρ.asModule

theorem TauCeti.Representation.asAlgebraHom_center_apply {k : Type u} {G : Type v} {V : Type w} [Field k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) [IsAlgClosed k] [FiniteDimensional k V] [ρ.IsIrreducible] (z : ↥(Subalgebra.center k (MonoidAlgebra k G))) (v : V) : (ρ.asAlgebraHom ↑z) v = (centralCharacter ρ) z • v

A central element of the group algebra acts on the representation as multiplication by the value of the central character.

Not itself @[simp]: simp reaches this normal form from the map-level TauCeti.Representation.asAlgebraHom_center below.

@[simp]

theorem TauCeti.Representation.asAlgebraHom_center {k : Type u} {G : Type v} {V : Type w} [Field k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) [IsAlgClosed k] [FiniteDimensional k V] [ρ.IsIrreducible] (z : ↥(Subalgebra.center k (MonoidAlgebra k G))) : ρ.asAlgebraHom ↑z = (centralCharacter ρ) z • LinearMap.id

A central element of the group algebra acts on an irreducible representation by a scalar endomorphism.

This is the simp normal form for the action of the centre: the opaque action is replaced by a scalar, applied or not.

theorem TauCeti.Representation.centralCharacter_eq_of_ne_zero_of_asAlgebraHom_apply_eq {k : Type u} {G : Type v} {V : Type w} [Field k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) [IsAlgClosed k] [FiniteDimensional k V] [ρ.IsIrreducible] {z : ↥(Subalgebra.center k (MonoidAlgebra k G))} {c : k} {v : V} (hv : v ≠ 0) (h : (ρ.asAlgebraHom ↑z) v = c • v) : (centralCharacter ρ) 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.

This is TauCeti.centralCharacter_eq_of_ne_zero_of_smul_eq read through Representation.asModuleEquiv.

theorem TauCeti.Representation.trace_asAlgebraHom_center {k : Type u} {G : Type v} {V : Type w} [Field k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) [IsAlgClosed k] [FiniteDimensional k V] [ρ.IsIrreducible] (z : ↥(Subalgebra.center k (MonoidAlgebra k G))) : (LinearMap.trace k V) (ρ.asAlgebraHom ↑z) = (centralCharacter ρ) z * ↑(Module.finrank k V)

The trace of the action of a central element is its central character times the degree.

theorem TauCeti.Representation.centralCharacter_eq_of_equiv {k : Type u} {G : Type v} {V : Type w} [Field k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) [IsAlgClosed k] [FiniteDimensional k V] [ρ.IsIrreducible] {W : Type u_1} [AddCommGroup W] [Module k W] [FiniteDimensional k W] (σ : Representation k G W) [σ.IsIrreducible] (φ : ρ.Equiv σ) : centralCharacter σ = centralCharacter ρ

Equivalent irreducible representations have the same central character. An equivalence commutes with the action of the group algebra, so it carries the scalar action of the centre on one to the scalar action on the other; a nonzero vector then forces the two scalars to agree.

theorem TauCeti.Representation.centralCharacter_classSumCenter_mul_character_one {k : Type u} {G : Type v} {V : Type w} [Field k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) [IsAlgClosed k] [FiniteDimensional k V] [ρ.IsIrreducible] [Fintype G] [DecidableEq G] {C : ConjClasses G} {g : G} (hg : ConjClasses.mk g = C) : (centralCharacter ρ) (classSumCenter C) * ρ.character 1 = ↑(Nat.card ↑C.carrier) * ρ.character g

The central character on a class sum. In division-free form: the value of the central character on the class sum of C, times the degree χ(1), is the size of C times the character value on C.

This is the identity ωᵪ(K_C) = |C| · χ(g) / χ(1) of the roadmap, stated so that no invertibility of the degree is needed; see TauCeti.Representation.centralCharacter_classSumCenter for the quotient form.

theorem TauCeti.Representation.centralCharacter_classSumCenter {k : Type u} {G : Type v} {V : Type w} [Field k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) [IsAlgClosed k] [FiniteDimensional k V] [ρ.IsIrreducible] [Fintype G] [DecidableEq G] {C : ConjClasses G} {g : G} (hg : ConjClasses.mk g = C) (hχ : ρ.character 1 ≠ 0) : (centralCharacter ρ) (classSumCenter C) = ↑(Nat.card ↑C.carrier) * ρ.character g / ρ.character 1

The central character on a class sum, in quotient form, when the degree of the representation is nonzero in k; it is nonzero whenever k has characteristic zero.

theorem TauCeti.Representation.isIntegral_centralCharacter_classSumCenter {k : Type u} {G : Type v} {V : Type w} [Field k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) [IsAlgClosed k] [FiniteDimensional k V] [ρ.IsIrreducible] [Fintype G] [DecidableEq G] (C : ConjClasses G) : IsIntegral ℤ ((centralCharacter ρ) (classSumCenter C))

The values of a central character on the class sums are algebraic integers.

The class sums are integral over ℤ in the centre of k[G], and an algebra homomorphism carries integral elements to integral elements.

The trivial representation

@[simp]

theorem TauCeti.Representation.centralCharacter_trivial_classSumCenter (k : Type u) (G : Type v) [Field k] [Group G] [IsAlgClosed k] [Fintype G] [DecidableEq G] (C : ConjClasses G) : (centralCharacter (Representation.trivial k G k)) (classSumCenter C) = ↑(Nat.card ↑C.carrier)

The central character of the trivial representation on the base field sends the class sum of C to the size of C: every group element acts by the identity there, so a class sum acts by the number of its terms.

This pins the normalization of TauCeti.Representation.centralCharacter. It is derived from TauCeti.Representation.centralCharacter_classSumCenter_mul_character_one as the case χ = 1, where both the degree and the character value on the class are 1.

This is the simp normal form of the value: the central character of the trivial representation on a class sum is evaluated to the size of the class.