The class-sum basis of the center

For a finite group G and a commutative semiring k, the coefficients of a central element of the group algebra k[G] are constant on conjugacy classes. This identifies the center linearly with the space of k-valued functions on ConjClasses G.

The corresponding family is a basis already over a commutative semiring. Over a ring satisfying the strong rank condition, this implies that the dimension of the center is the number of conjugacy classes.

The identification is built by sending a central element to its coefficient function as a TauCeti.ClassFunction, and composing with the equivalence TauCeti.ClassFunction.equivConjClasses, so the descent to the quotient and its linearity are reused rather than repeated here.

This implementation follows the Character Theory roadmap and its suggested declarations.

def TauCeti.centerToClassFunction {G : Type u_1} {k : Type u_2} [Group G] [CommSemiring k] : ↥(Subalgebra.center k (MonoidAlgebra k G)) →ₗ[k] ↥(ClassFunction k G)

The coefficient function of a central group-algebra element, as a class function on G.

Equations

• TauCeti.centerToClassFunction = { toFun := fun (z : ↥(Subalgebra.center k (MonoidAlgebra k G))) => ⟨fun (g : G) => (↑z).coeff g, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.centerToClassFunction_apply {G : Type u_1} {k : Type u_2} [Group G] [CommSemiring k] (z : ↥(Subalgebra.center k (MonoidAlgebra k G))) (g : G) : ↑(centerToClassFunction z) g = (↑z).coeff g

The class function of a central element is its coefficient function.

theorem TauCeti.center_coeff_eq_of_isConj {G : Type u_1} {k : Type u_2} [Group G] [CommSemiring k] (z : ↥(Subalgebra.center k (MonoidAlgebra k G))) {g h : G} (hgh : IsConj g h) : (↑z).coeff g = (↑z).coeff h

The coefficients of a central group-algebra element agree on conjugate group elements.

noncomputable def TauCeti.centerToConjClasses {G : Type u_1} {k : Type u_2} [Group G] [CommSemiring k] (z : ↥(Subalgebra.center k (MonoidAlgebra k G))) : ConjClasses G → k

Read the coefficients of a central group-algebra element as a function on conjugacy classes.

Equations

• TauCeti.centerToConjClasses z = TauCeti.ClassFunction.equivConjClasses (TauCeti.centerToClassFunction z)

@[simp]

theorem TauCeti.centerToConjClasses_mk {G : Type u_1} {k : Type u_2} [Group G] [CommSemiring k] (z : ↥(Subalgebra.center k (MonoidAlgebra k G))) (g : G) : centerToConjClasses z (ConjClasses.mk g) = (↑z).coeff g

Reading the coefficient on the conjugacy class of g recovers the coefficient at g.

noncomputable def TauCeti.classSumCenter {G : Type u_1} {k : Type u_2} [Group G] [Fintype G] [DecidableEq G] [CommSemiring k] (C : ConjClasses G) : ↥(Subalgebra.center k (MonoidAlgebra k G))

Regard a class sum as an element of the center of the group algebra.

Equations

• TauCeti.classSumCenter C = ⟨TauCeti.classSum k C, ⋯⟩

@[simp]

theorem TauCeti.classSumCenter_coe {G : Type u_1} {k : Type u_2} [Group G] [Fintype G] [DecidableEq G] [CommSemiring k] (C : ConjClasses G) : ↑(classSumCenter C) = classSum k C

The underlying group-algebra element of a central class sum is the class sum.

@[simp]

theorem TauCeti.classSumCenter_mk_one {G : Type u_1} {k : Type u_2} [Group G] [Fintype G] [DecidableEq G] [CommSemiring k] : classSumCenter (ConjClasses.mk 1) = 1

The class sum of the conjugacy class of 1, as an element of the center, is 1.

noncomputable def TauCeti.ofConjClassesCenter {G : Type u_1} {k : Type u_2} [Group G] [Fintype G] [DecidableEq G] [CommSemiring k] (f : ConjClasses G → k) : ↥(Subalgebra.center k (MonoidAlgebra k G))

Convert a function on conjugacy classes to the corresponding linear combination of class sums.

Equations

• TauCeti.ofConjClassesCenter f = ∑ C : ConjClasses G, f C • TauCeti.classSumCenter C

@[simp]

theorem TauCeti.ofConjClassesCenter_coeff {G : Type u_1} {k : Type u_2} [Group G] [Fintype G] [DecidableEq G] [CommSemiring k] (f : ConjClasses G → k) (g : G) : (↑(ofConjClassesCenter f)).coeff g = f (ConjClasses.mk g)

The coefficient at g of the class-sum expansion is the value on the class of g.

noncomputable def TauCeti.centerEquivConjClasses {G : Type u_1} {k : Type u_2} [Group G] [Fintype G] [DecidableEq G] [CommSemiring k] : ↥(Subalgebra.center k (MonoidAlgebra k G)) ≃ₗ[k] ConjClasses G → k

The center of a finite group algebra is linearly equivalent to the functions on conjugacy classes, by taking coefficients.

Equations

• TauCeti.centerEquivConjClasses = { toFun := TauCeti.centerToConjClasses, map_add' := ⋯, map_smul' := ⋯, invFun := TauCeti.ofConjClassesCenter, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem TauCeti.centerEquivConjClasses_apply {G : Type u_1} {k : Type u_2} [Group G] [Fintype G] [DecidableEq G] [CommSemiring k] (z : ↥(Subalgebra.center k (MonoidAlgebra k G))) : centerEquivConjClasses z = centerToConjClasses z

The forward map of centerEquivConjClasses reads the coefficients of a central element.

@[simp]

theorem TauCeti.centerEquivConjClasses_symm_apply {G : Type u_1} {k : Type u_2} [Group G] [Fintype G] [DecidableEq G] [CommSemiring k] (f : ConjClasses G → k) : centerEquivConjClasses.symm f = ofConjClassesCenter f

The inverse of centerEquivConjClasses forms the corresponding linear combination of class sums.

noncomputable def TauCeti.classSumBasis {G : Type u_1} {k : Type u_2} [Group G] [Fintype G] [DecidableEq G] [CommSemiring k] : Module.Basis (ConjClasses G) k ↥(Subalgebra.center k (MonoidAlgebra k G))

The class sums, regarded as central group-algebra elements, form a basis of the center.

Equations

• TauCeti.classSumBasis = Module.Basis.ofEquivFun TauCeti.centerEquivConjClasses

@[simp]

theorem TauCeti.classSumBasis_apply {G : Type u_1} {k : Type u_2} [Group G] [Fintype G] [DecidableEq G] [CommSemiring k] (C : ConjClasses G) : classSumBasis C = classSumCenter C

A vector in the class-sum basis is the corresponding central class sum.

@[simp]

theorem TauCeti.classSumBasis_repr_apply {G : Type u_1} {k : Type u_2} [Group G] [Fintype G] [DecidableEq G] [CommSemiring k] (z : ↥(Subalgebra.center k (MonoidAlgebra k G))) (C : ConjClasses G) : (classSumBasis.repr z) C = centerToConjClasses z C

The coordinate of a central element in the class-sum basis is its coefficient on that conjugacy class.

instance TauCeti.instModuleFiniteCenterMonoidAlgebra (k : Type u_1) (G : Type u_2) [CommSemiring k] [Group G] [Finite G] : Module.Finite k ↥(Subalgebra.center k (MonoidAlgebra k G))

The center of a finite group algebra is finite as a module, with its class-sum basis.

theorem TauCeti.finrank_center_monoidAlgebra (k : Type u_1) (G : Type u_2) [CommSemiring k] [Group G] [Finite G] [StrongRankCondition k] : Module.finrank k ↥(Subalgebra.center k (MonoidAlgebra k G)) = Nat.card (ConjClasses G)

The dimension of the center of a finite group algebra is the number of conjugacy classes.