The irreducible representations carried by the Wedderburn blocks

A Wedderburn presentation e : k[G] ≃ₐ[k] Π i, Matₙᵢ(k) of a finite group algebra is a numerical statement until each block is turned into a representation. This file does that: composing e with the projection onto the i-th factor and with Matrix.toLinAlgEquiv' presents the column space Fin (d i) → k as a k[G]-module, hence as a representation of G.

Two facts make the resulting family the family of irreducibles. Each blockRepresentation e i is irreducible by Representation.isIrreducible_of_asAlgebraHom_surjective, its algebra map onto End k (Fin (d i) → k) being surjective. And the blocks are pairwise inequivalent, because the idempotent e.symm (Pi.single i 1) acts as the identity on the i-th block and as zero on every other one.

Together with TauCeti.exists_algEquiv_pi_matrix_conjClasses this produces, over an algebraically closed field whose characteristic does not divide |G|, a family of pairwise inequivalent irreducible representations of G indexed by the conjugacy classes of G.

Main definitions

• TauCeti.blockAlgHom: the algebra map from k[G] onto the endomorphisms of the i-th column space cut out by a Wedderburn presentation.
• TauCeti.blockRepresentation: the representation of G on that column space.

Main statements

• TauCeti.isIrreducible_blockRepresentation: every block of a Wedderburn presentation carries an irreducible representation.
• TauCeti.isEmpty_equiv_blockRepresentation: distinct blocks carry inequivalent representations.
• TauCeti.exists_irreducible_family_conjClasses: there are as many pairwise inequivalent irreducible representations of G as G has conjugacy classes, in the form of a family indexed by ConjClasses G, whose dimensions have squares summing to |G|.

References

This supplies one half of the block ⇆ irreducible-representation matching that Layer 2.5 of the character theory roadmap asks for, in the concrete form needed by Layer 3's completeness statement. See J.-P. Serre, Linear Representations of Finite Groups, Section 6.4, or I. M. Isaacs, Character Theory of Finite Groups, Chapter 1.

noncomputable def TauCeti.blockAlgHom {k : Type u} {G : Type v} [CommSemiring k] [Monoid G] {ι : Type w} {d : ι → ℕ} (e : MonoidAlgebra k G ≃ₐ[k] (i : ι) → Matrix (Fin (d i)) (Fin (d i)) k) (i : ι) : MonoidAlgebra k G →ₐ[k] Module.End k (Fin (d i) → k)

The algebra map from the group algebra onto the endomorphisms of the i-th column space of a Wedderburn presentation: project e onto the i-th matrix block and let a matrix act on column vectors.

Equations

• TauCeti.blockAlgHom e i = (↑Matrix.toLinAlgEquiv').comp ((Pi.evalAlgHom k (fun (j : ι) => Matrix (Fin (d j)) (Fin (d j)) k) i).comp ↑e)

@[simp]

theorem TauCeti.blockAlgHom_apply {k : Type u} {G : Type v} [CommSemiring k] [Monoid G] {ι : Type w} {d : ι → ℕ} (e : MonoidAlgebra k G ≃ₐ[k] (i : ι) → Matrix (Fin (d i)) (Fin (d i)) k) (i : ι) (x : MonoidAlgebra k G) : (blockAlgHom e i) x = Matrix.toLinAlgEquiv' (e x i)

theorem TauCeti.blockAlgHom_surjective {k : Type u} {G : Type v} [CommSemiring k] [Monoid G] {ι : Type w} {d : ι → ℕ} (e : MonoidAlgebra k G ≃ₐ[k] (i : ι) → Matrix (Fin (d i)) (Fin (d i)) k) (i : ι) : Function.Surjective ⇑(blockAlgHom e i)

Each block of a Wedderburn presentation exhausts the endomorphisms of its column space: e is bijective, the projection onto a factor is surjective, and matrices are all the endomorphisms of a coordinate space.

noncomputable def TauCeti.blockRepresentation {k : Type u} {G : Type v} [CommSemiring k] [Monoid G] {ι : Type w} {d : ι → ℕ} (e : MonoidAlgebra k G ≃ₐ[k] (i : ι) → Matrix (Fin (d i)) (Fin (d i)) k) (i : ι) : Representation k G (Fin (d i) → k)

The representation of G on the i-th block of a Wedderburn presentation of k[G]: the group acts on the column space Fin (d i) → k through the i-th matrix factor.

Equations

• TauCeti.blockRepresentation e i = (↑(TauCeti.blockAlgHom e i).toRingHom).comp (MonoidAlgebra.of k G)

@[simp]

theorem TauCeti.blockRepresentation_apply {k : Type u} {G : Type v} [CommSemiring k] [Monoid G] {ι : Type w} {d : ι → ℕ} (e : MonoidAlgebra k G ≃ₐ[k] (i : ι) → Matrix (Fin (d i)) (Fin (d i)) k) (i : ι) (g : G) : (blockRepresentation e i) g = Matrix.toLinAlgEquiv' (e ((MonoidAlgebra.of k G) g) i)

@[simp]

theorem TauCeti.asAlgebraHom_blockRepresentation {k : Type u} {G : Type v} [CommSemiring k] [Monoid G] {ι : Type w} {d : ι → ℕ} (e : MonoidAlgebra k G ≃ₐ[k] (i : ι) → Matrix (Fin (d i)) (Fin (d i)) k) (i : ι) : (blockRepresentation e i).asAlgebraHom = blockAlgHom e i

The algebra map of TauCeti.blockRepresentation is the block projection it was built from.

theorem TauCeti.isIrreducible_blockRepresentation {k : Type u} {G : Type v} [Field k] [Monoid G] {ι : Type w} {d : ι → ℕ} (e : MonoidAlgebra k G ≃ₐ[k] (i : ι) → Matrix (Fin (d i)) (Fin (d i)) k) (i : ι) [NeZero (d i)] : (blockRepresentation e i).IsIrreducible

Every Wedderburn block carries an irreducible representation.

theorem TauCeti.isEmpty_equiv_blockRepresentation {k : Type u} {G : Type v} [CommSemiring k] [Nontrivial k] [Monoid G] {ι : Type w} {d : ι → ℕ} (e : MonoidAlgebra k G ≃ₐ[k] (i : ι) → Matrix (Fin (d i)) (Fin (d i)) k) {i j : ι} [NeZero (d i)] (hij : i ≠ j) : IsEmpty ((blockRepresentation e i).Equiv (blockRepresentation e j))

Distinct Wedderburn blocks carry inequivalent representations. The idempotent that e matches with Pi.single i 1 acts as the identity on the i-th block and as zero on the j-th.

theorem TauCeti.exists_irreducible_family_conjClasses (k : Type u) (G : Type v) [Field k] [Group G] [Finite G] [NeZero ↑(Nat.card G)] [IsAlgClosed k] : ∃ (d : ConjClasses G → ℕ) (ρ : (C : ConjClasses G) → Representation k G (Fin (d C) → k)), (∀ (C : ConjClasses G), (ρ C).IsIrreducible) ∧ (Pairwise fun (C D : ConjClasses G) => IsEmpty ((ρ C).Equiv (ρ D))) ∧ ∑ᶠ (C : ConjClasses G), d C ^ 2 = Nat.card G

There are as many pairwise inequivalent irreducible representations of G as G has conjugacy classes. Maschke and Artin--Wedderburn present k[G] with its blocks indexed by ConjClasses G, and the blocks carry pairwise inequivalent irreducible representations, of dimensions whose squares add up to |G|, that being the dimension of k[G].

The bound in the other direction, that no family of pairwise inequivalent irreducibles is larger, is TauCeti.ClassFunction.card_le_card_conjClasses.