The Wedderburn blocks of a finite group algebra

Over an algebraically closed field k whose characteristic does not divide the order of a finite group G, Maschke's theorem makes k[G] semisimple and Artin--Wedderburn presents it as a finite product of matrix algebras ∏ᵢ Matₙᵢ(k). This file reads the two classical numerical invariants off such a presentation:

• TauCeti.sum_sq_eq_card_of_algEquiv_pi_matrix: the matrix sizes satisfy ∑ᵢ nᵢ² = |G|, because both sides compute dimₖ k[G];
• TauCeti.card_eq_card_conjClasses_of_algEquiv_pi_matrix: the number of blocks is the number of conjugacy classes of G, because both sides compute dimₖ Z(k[G]) — on one side through the class-sum basis (TauCeti.finrank_center_monoidAlgebra), on the other because the center of a product of matrix algebras over k is the product of their (one-dimensional) centers.

TauCeti.exists_algEquiv_pi_matrix assembles Maschke and Artin--Wedderburn into the existence of a presentation, and TauCeti.exists_algEquiv_pi_matrix_conjClasses packages the three results: there is a presentation of k[G] indexed by the conjugacy classes of G whose degrees have squares summing to |G|.

Two further statements about a Wedderburn presentation are deliberately not proved here, and are needed before the block count can be called the count of irreducible representations: that the blocks are in bijection with the isomorphism classes of simple k[G]-modules, and that the multiset of degrees does not depend on the chosen presentation. What this file supplies is the numerical half, which is what the dimension arguments can see. Both are proved downstream, in TauCeti/RepresentationTheory/CharacterTable/IrreducibleClassification.lean, as AlgEquiv.nonempty_equiv_index_simpleSubmoduleClasses and TauCeti.natCard_degree_fiber_eq, on top of the block representations of TauCeti/RepresentationTheory/CharacterTable/BlockRepresentation.lean and the exhaustion TauCeti.ClassFunction.exists_nonempty_equiv of TauCeti/RepresentationTheory/CharacterTable/Completeness.lean.

theorem TauCeti.sum_sq_eq_card_of_algEquiv_pi_matrix {k : Type u_1} {G : Type u_2} [Field k] {ι : Type u_3} {d : ι → ℕ} [Monoid G] [Finite G] [Fintype ι] (e : MonoidAlgebra k G ≃ₐ[k] (i : ι) → Matrix (Fin (d i)) (Fin (d i)) k) : ∑ i : ι, d i ^ 2 = Nat.card G

The sum of the squares of the matrix sizes is the order of the group: both sides compute the dimension of k[G].

noncomputable def TauCeti.centerMonoidAlgebraAlgEquivPi {k : Type u_1} {G : Type u_2} [Field k] {ι : Type u_3} {d : ι → ℕ} [Monoid G] [∀ (i : ι), NeZero (d i)] (e : MonoidAlgebra k G ≃ₐ[k] (i : ι) → Matrix (Fin (d i)) (Fin (d i)) k) : ↥(Subalgebra.center k (MonoidAlgebra k G)) ≃ₐ[k] ι → k

The center of the group algebra splits: a Wedderburn presentation of k[G] with blocks indexed by ι identifies Z(k[G]) with the algebra ι → k of functions on the blocks.

Equations

• TauCeti.centerMonoidAlgebraAlgEquivPi e = (TauCeti.centerCongr e).trans (TauCeti.centerPiMatrixAlgEquiv k d)

@[simp]

theorem TauCeti.algebraMap_centerMonoidAlgebraAlgEquivPi_apply {k : Type u_1} {G : Type u_2} [Field k] {ι : Type u_3} {d : ι → ℕ} [Monoid G] [∀ (i : ι), NeZero (d i)] (e : MonoidAlgebra k G ≃ₐ[k] (i : ι) → Matrix (Fin (d i)) (Fin (d i)) k) (z : ↥(Subalgebra.center k (MonoidAlgebra k G))) (i : ι) : (algebraMap k (Matrix (Fin (d i)) (Fin (d i)) k)) ((centerMonoidAlgebraAlgEquivPi e) z i) = e (↑z) i

centerMonoidAlgebraAlgEquivPi e records, block by block, the scalar that a central element of k[G] acts by: the i-th component of the image of e is that scalar matrix.

@[simp]

theorem TauCeti.centerMonoidAlgebraAlgEquivPi_symm_apply {k : Type u_1} {G : Type u_2} [Field k] {ι : Type u_3} {d : ι → ℕ} [Monoid G] [∀ (i : ι), NeZero (d i)] (e : MonoidAlgebra k G ≃ₐ[k] (i : ι) → Matrix (Fin (d i)) (Fin (d i)) k) (f : ι → k) (i : ι) : e (↑((centerMonoidAlgebraAlgEquivPi e).symm f)) i = (algebraMap k (Matrix (Fin (d i)) (Fin (d i)) k)) (f i)

The inverse of centerMonoidAlgebraAlgEquivPi e builds the central element acting on each block by the prescribed scalar.

theorem TauCeti.card_eq_card_conjClasses_of_algEquiv_pi_matrix {k : Type u_1} {G : Type u_2} [Field k] {ι : Type u_3} {d : ι → ℕ} [Group G] [Finite G] [Fintype ι] [∀ (i : ι), NeZero (d i)] (e : MonoidAlgebra k G ≃ₐ[k] (i : ι) → Matrix (Fin (d i)) (Fin (d i)) k) : Fintype.card ι = Nat.card (ConjClasses G)

The number of Wedderburn blocks of k[G] is the number of conjugacy classes of G: both sides compute the dimension of Z(k[G]).

This is the numerical half of the count #irreducibles = #conjugacy classes; identifying the blocks with the isomorphism classes of simple k[G]-modules is a separate statement.

theorem TauCeti.exists_algEquiv_pi_matrix (k : Type u_1) (G : Type u_2) [Field k] [Group G] [Finite G] [NeZero ↑(Nat.card G)] [IsAlgClosed k] : ∃ (n : ℕ) (d : Fin n → ℕ), (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (MonoidAlgebra k G ≃ₐ[k] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) k)

Maschke and Artin--Wedderburn for a finite group algebra: over an algebraically closed field whose characteristic does not divide |G|, the group algebra is a finite product of matrix algebras of positive size.

theorem TauCeti.exists_algEquiv_pi_matrix_conjClasses (k : Type u_1) (G : Type u_2) [Field k] [Group G] [Finite G] [NeZero ↑(Nat.card G)] [IsAlgClosed k] : ∃ (d : ConjClasses G → ℕ), (∀ (i : ConjClasses G), NeZero (d i)) ∧ ∑ᶠ (i : ConjClasses G), d i ^ 2 = Nat.card G ∧ Nonempty (MonoidAlgebra k G ≃ₐ[k] (i : ConjClasses G) → Matrix (Fin (d i)) (Fin (d i)) k)

The Wedderburn decomposition of k[G], with its blocks indexed by the conjugacy classes of G themselves, and with the degrees squaring to a sum of |G|.

The indexing is by an arbitrary bijection between the blocks and the conjugacy classes: the statement asserts nothing about which class labels a given block.