Wedderburn decomposition of the group algebra

DefinitionAlgebra map of a Wedderburn block#✓fully proved

Let \(k\) be an algebraically closed field, \(G\) a finite group whose order is nonzero in \(k\), and \(e \colon k[G] \to \prod_{j < n} M_{d_j}(k)\) an isomorphism of \(k\)-algebras from the group algebra onto a product of full matrix algebras. For \(i < n\), this is the \(k\)-algebra homomorphism \(k[G] \to \operatorname{End}_k(k^{d_i})\) that sends \(a \in k[G]\) to the linear map \(v \mapsto e(a)_i \, v\), where \(e(a)_i\) is the \(i\)-th component of \(e(a)\).

noncomputable def wedderburnAlgHom (k : Type u) [Field k] [IsAlgClosed k]
    (G : Type u) [Group G] [Fintype G] [NeZero (Nat.card G : k)]
    {n : ℕ} {d : Fin n → ℕ}
    (e : MonoidAlgebra k G ≃ₐ[k] Π j, Matrix (Fin (d j)) (Fin (d j)) k)
    (i : Fin n) :
    MonoidAlgebra k G →ₐ[k] Module.End k (Fin (d i) → k) :=
  (Matrix.toLinAlgEquiv' (R := k) (n := Fin (d i))).toAlgHom.comp
    ((Pi.evalAlgHom k _ i).comp e.toAlgHom)

Used by 2

Used byRepresentation of a Wedderburn block · Wedderburn blocks are irreducible

DefinitionRepresentation of a Wedderburn block#✓fully proved

Let \(k\) be an algebraically closed field, \(G\) a finite group whose order is nonzero in \(k\), and \(e \colon k[G] \to \prod_{j < n} M_{d_j}(k)\) an isomorphism of \(k\)-algebras from the group algebra \(k[G]\) onto a product of full matrix algebras \(M_{d_j}(k)\) of \(d_j \times d_j\) matrices over \(k\). For \(i < n\), this is the representation of \(G\) on \(k^{d_i}\) in which \(g \in G\) acts by \(v \mapsto e(g)_i \, v\), where \(g\) is viewed as an element of \(k[G]\) and \(e(g)_i\) is the \(i\)-th component of \(e(g)\).

noncomputable def wedderburnIrrep (k : Type u) [Field k] [IsAlgClosed k]
    (G : Type u) [Group G] [Fintype G] [NeZero (Nat.card G : k)]
    {n : ℕ} {d : Fin n → ℕ}
    (e : MonoidAlgebra k G ≃ₐ[k] Π j, Matrix (Fin (d j)) (Fin (d j)) k)
    (i : Fin n) :
    Representation k G (Fin (d i) → k) :=
  (wedderburnAlgHom k G e i).toRingHom.toMonoidHom.comp (MonoidAlgebra.of k G)

Uses 1 · Used by 1

Statement usesAlgebra map of a Wedderburn block

Used byWedderburn blocks are irreducible

TheoremWedderburn blocks are irreducible#✓fully proved

Let \(k\) be an algebraically closed field, \(G\) a finite group whose order is nonzero in \(k\), and \(e \colon k[G] \to \prod_{j < n} M_{d_j}(k)\) an isomorphism of \(k\)-algebras from the group algebra \(k[G]\) onto a product of full matrix algebras \(M_{d_j}(k)\) of \(d_j \times d_j\) matrices over \(k\). For every \(i < n\) with \(d_i \ne 0\), the representation of \(G\) on \(k^{d_i}\) in which \(g \in G\) acts by \(v \mapsto e(g)_i \, v\), where \(g\) is viewed as an element of \(k[G]\) and \(e(g)_i\) is the \(i\)-th component of \(e(g)\), is irreducible.

theorem wedderburnIrrep_isIrreducible (k : Type u) [Field k] [IsAlgClosed k]
    (G : Type u) [Group G] [Fintype G] [NeZero (Nat.card G : k)]
    {n : ℕ} {d : Fin n → ℕ}
    (e : MonoidAlgebra k G ≃ₐ[k] Π j, Matrix (Fin (d j)) (Fin (d j)) k)
    (i : Fin n) [NeZero (d i)] :
    (wedderburnIrrep k G e i).IsIrreducible

Uses 2

Statement usesRepresentation of a Wedderburn block

Proof usesAlgebra map of a Wedderburn block

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.