The Wedderburn blocks of k[G] classify its irreducible representations

A Wedderburn presentation e : k[G] ≃ₐ[k] Π i, Matₙᵢ(k) of a finite group algebra over an algebraically closed field carries an irreducible representation on each block, and distinct blocks carry inequivalent ones (TauCeti/RepresentationTheory/CharacterTable/BlockRepresentation.lean). This file supplies the missing half, that the list is complete: every finite-dimensional irreducible representation of G over k is equivalent to a block representation. The block index is therefore a faithful index of the irreducible representations up to equivalence, and everything read off a presentation — first of all the multiset of degrees nᵢ — is an invariant of G.

Completeness is not a new argument: a family of pairwise inequivalent irreducibles indexed by as many indices as G has conjugacy classes already exhausts the irreducibles (TauCeti.ClassFunction.exists_nonempty_equiv), and a presentation has exactly that many blocks (TauCeti.card_eq_card_conjClasses_of_algEquiv_pi_matrix). What was missing was the assembly, and the invariance statements it unlocks.

Main results

• TauCeti.exists_nonempty_equiv_blockRepresentation: every irreducible representation of G is equivalent to a block representation, so the blocks are a complete irredundant list.
• TauCeti.exists_degree_eq_finrank: the dimension of an irreducible representation is the degree of the block it matches, and TauCeti.exists_isIrreducible_finrank_eq is the converse, that each degree is realized.
• TauCeti.exists_equiv_blockRepresentation: two Wedderburn presentations of k[G] differ by a permutation of the blocks, matching degrees and block representations.
• TauCeti.natCard_degree_fiber_eq: the multiset of degrees does not depend on the presentation, in the form that each degree occurs equally often in the two.
• AlgEquiv.nonempty_equiv_index_simpleSubmoduleClasses: the block index is in bijection with the isomorphism classes of simple k[G]-modules.

Implementation notes

The degree multiset is compared through the cardinalities of the fibres of the degree function, Nat.card {i // d i = n}, rather than through Multiset.map d Finset.univ.val: the index types carry Finite rather than Fintype, and the fibre form needs no decidability or enumeration and says the same thing.

The [∀ i, NeZero (d i)] hypotheses are essential throughout, exactly as in IsSemisimpleRing.exists_ringEquiv_pi_matrix_divisionRing, which produces them: a block of size zero is the trivial ring, carries no representation, and could be inserted into any presentation without changing the product, so without positivity neither the block count nor the degree multiset would be an invariant.

Only the representation-level dictionary is new here. The module-level one, that the blocks of a presentation of any semisimple ring are in bijection with the isomorphism classes of its simple modules, is RingEquiv.nonempty_equiv_simpleSubmoduleClasses_of_pi; its group-algebra case is recorded below as a corollary, since the two dictionaries are what TauCeti/RepresentationTheory/CharacterTable/Wedderburn.lean names as the statements needed before its block count may be called the count of irreducible representations.

References

See J.-P. Serre, Linear Representations of Finite Groups, Section 6.4, or C. W. Curtis and I. Reiner, Representation Theory of Finite Groups and Associative Algebras, Section 26.

theorem TauCeti.exists_nonempty_equiv_blockRepresentation {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [IsAlgClosed k] [Invertible ↑(Nat.card G)] {ι : Type w} [Finite ι] {d : ι → ℕ} [∀ (i : ι), NeZero (d i)] (e : MonoidAlgebra k G ≃ₐ[k] (i : ι) → Matrix (Fin (d i)) (Fin (d i)) k) {W : Type w'} [AddCommGroup W] [Module k W] [FiniteDimensional k W] (σ : Representation k G W) [σ.IsIrreducible] : ∃ (i : ι), Nonempty (σ.Equiv (blockRepresentation e i))

The Wedderburn blocks are a complete list of the irreducible representations. Every finite-dimensional irreducible representation of G over an algebraically closed field whose characteristic does not divide |G| is equivalent to the representation carried by one of the blocks of any Wedderburn presentation of k[G].

Together with TauCeti.isIrreducible_blockRepresentation and TauCeti.isEmpty_equiv_blockRepresentation this makes the block index a faithful index of the irreducible representations up to equivalence.

theorem TauCeti.exists_degree_eq_finrank {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [IsAlgClosed k] [Invertible ↑(Nat.card G)] {ι : Type w} [Finite ι] {d : ι → ℕ} [∀ (i : ι), NeZero (d i)] (e : MonoidAlgebra k G ≃ₐ[k] (i : ι) → Matrix (Fin (d i)) (Fin (d i)) k) {W : Type w'} [AddCommGroup W] [Module k W] [FiniteDimensional k W] (σ : Representation k G W) [σ.IsIrreducible] : ∃ (i : ι), d i = Module.finrank k W

The dimension of an irreducible representation is one of the Wedderburn degrees.

theorem TauCeti.exists_isIrreducible_finrank_eq {k : Type u} {G : Type v} [Field k] [Group G] {ι : Type w} {d : ι → ℕ} [∀ (i : ι), NeZero (d i)] (e : MonoidAlgebra k G ≃ₐ[k] (i : ι) → Matrix (Fin (d i)) (Fin (d i)) k) (i : ι) : ∃ (W : Type u) (x : AddCommGroup W) (x_1 : Module k W) (σ : Representation k G W), σ.IsIrreducible ∧ Module.finrank k W = d i

Every Wedderburn degree is the dimension of an irreducible representation, namely of the representation carried by that block. This is the converse of TauCeti.exists_degree_eq_finrank.

theorem AlgEquiv.nonempty_equiv_index_simpleSubmoduleClasses {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [Invertible ↑(Nat.card G)] {ι : Type w} {d : ι → ℕ} [∀ (i : ι), NeZero (d i)] (e : MonoidAlgebra k G ≃ₐ[k] (i : ι) → Matrix (Fin (d i)) (Fin (d i)) k) : Nonempty (ι ≃ TauCeti.SimpleSubmoduleClasses (MonoidAlgebra k G) (MonoidAlgebra k G))

The block index is in bijection with the isomorphism classes of simple k[G]-modules. This is the group-algebra case of RingEquiv.nonempty_equiv_simpleSubmoduleClasses_of_pi, the module-level companion of TauCeti.exists_nonempty_equiv_blockRepresentation.

theorem TauCeti.exists_equiv_blockRepresentation {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [IsAlgClosed k] [Invertible ↑(Nat.card G)] {ι : Type w} [Finite ι] {d : ι → ℕ} [∀ (i : ι), NeZero (d i)] {ι' : Type w'} [Finite ι'] {d' : ι' → ℕ} [∀ (j : ι'), NeZero (d' j)] (e : MonoidAlgebra k G ≃ₐ[k] (i : ι) → Matrix (Fin (d i)) (Fin (d i)) k) (e' : MonoidAlgebra k G ≃ₐ[k] (j : ι') → Matrix (Fin (d' j)) (Fin (d' j)) k) : ∃ (σ : ι ≃ ι'), ∀ (i : ι), d i = d' (σ i) ∧ Nonempty ((blockRepresentation e i).Equiv (blockRepresentation e' (σ i)))

Two Wedderburn presentations of k[G] differ by a permutation of their blocks. The permutation matches the degrees and the representations the blocks carry, so every invariant read off a presentation is an invariant of G.

The bijection is not canonical — nothing orders the blocks — so it is produced existentially.

theorem TauCeti.natCard_index_eq {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [IsAlgClosed k] [Invertible ↑(Nat.card G)] {ι : Type w} [Finite ι] {d : ι → ℕ} [∀ (i : ι), NeZero (d i)] {ι' : Type w'} [Finite ι'] {d' : ι' → ℕ} [∀ (j : ι'), NeZero (d' j)] (e : MonoidAlgebra k G ≃ₐ[k] (i : ι) → Matrix (Fin (d i)) (Fin (d i)) k) (e' : MonoidAlgebra k G ≃ₐ[k] (j : ι') → Matrix (Fin (d' j)) (Fin (d' j)) k) : Nat.card ι = Nat.card ι'

The block count does not depend on the presentation.

theorem TauCeti.natCard_degree_fiber_eq {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [IsAlgClosed k] [Invertible ↑(Nat.card G)] {ι : Type w} [Finite ι] {d : ι → ℕ} [∀ (i : ι), NeZero (d i)] {ι' : Type w'} [Finite ι'] {d' : ι' → ℕ} [∀ (j : ι'), NeZero (d' j)] (e : MonoidAlgebra k G ≃ₐ[k] (i : ι) → Matrix (Fin (d i)) (Fin (d i)) k) (e' : MonoidAlgebra k G ≃ₐ[k] (j : ι') → Matrix (Fin (d' j)) (Fin (d' j)) k) (n : ℕ) : Nat.card { i : ι // d i = n } = Nat.card { j : ι' // d' j = n }

The multiset of Wedderburn degrees does not depend on the presentation: every degree occurs equally often in the two. Together with TauCeti.exists_degree_eq_finrank and TauCeti.exists_isIrreducible_finrank_eq this says that the degrees list the dimensions of the irreducible representations of G, one dimension for each equivalence class.