Irreducible characters and class functions

DefinitionClass functions on a group#✓fully proved

Let \(G\) be a group and \(k\) a set. A function \(f : G \to k\) is a class function when it is constant on conjugacy classes, that is, \(f(h g h^{-1}) = f(g)\) for all \(g, h \in G\).

def IsClassFunction {G k : Type*} [Group G] (f : G → k) : Prop :=
  ∀ g h : G, f (h * g * h⁻¹) = f g

Used by 7

Used byNumber of irreducible characters · Characters are class functions · The space of class functions · Class functions as functions on conjugacy classes · Class functions agree on conjugate elements · A class function orthogonal to all irreducible characters vanishes · Class functions factor through conjugacy classes

DefinitionThe space of class functions#✓fully proved

Let \(G\) be a group and \(k\) a field. The space of class functions \(G \to k\) is the \(k\)-linear subspace of the vector space of all functions \(G \to k\), under pointwise addition and scalar multiplication, consisting of the class functions.

def classFunctions (G : Type*) [Group G] (k : Type*) [Field k] :
    Submodule k (G → k) where
  carrier := {f | IsClassFunction f}
  zero_mem' := fun _ _ => rfl
  add_mem' := fun hf hg a b => by simp only [Pi.add_apply, hf a b, hg a b]
  smul_mem' := fun c f hf a b => by simp only [Pi.smul_apply, hf a b]

Uses 1 · Used by 5

Statement usesClass functions on a group

Used byNumber of irreducible characters · Class functions as functions on conjugacy classes · Evaluating a class function on conjugacy classes · Lifting a function on conjugacy classes · Dimension of the space of class functions

TheoremCharacters are class functions#✓fully proved

Let \(G\) be a group and \(k\) a field. For every finite-dimensional representation \(V\) of \(G\) over \(k\), the character of \(V\), the function sending \(g \in G\) to the trace of the linear map by which \(g\) acts on \(V\), is a class function on \(G\).

public theorem character_isClassFunction {G k : Type*} [Group G] [Field k]
    (V : FDRep k G) : IsClassFunction V.character

Sources

• J.-P. Serre, Linear Representations of Finite Groups, GTM 42, §2.1 (the character is constant on conjugacy classes).

Uses 1 · Used by 2

Statement usesClass functions on a group

Used byNumber of irreducible characters · Irreducible characters span the class functions

TheoremClass functions agree on conjugate elements#✓fully proved

Let \(G\) be a group and let \(f : G \to k\) be a class function with values in a set \(k\). If \(x, y \in G\) are conjugate, then \(f(x) = f(y)\).

public theorem IsClassFunction.eq_of_isConj {G k : Type*} [Group G]
    {f : G → k} (hf : IsClassFunction f) {x y : G} (hxy : IsConj x y) : f x = f y

Uses 1 · Used by 2

Statement usesClass functions on a group

Used byClass functions as functions on conjugacy classes · Class functions factor through conjugacy classes

TheoremClass functions factor through conjugacy classes#✓fully proved

Let \(G\) be a group and \(k\) a set, and write \([x]\) for the conjugacy class of \(x \in G\). A function \(f : G \to k\) is a class function if and only if there is a function \(q\) from the set of conjugacy classes of \(G\) to \(k\) such that \(f(x) = q([x])\) for all \(x \in G\).

Proof: A class function is constant on each conjugacy class, so it descends to a function on conjugacy classes. Conversely, if \(f(x) = q([x])\) for all \(x \in G\), then for all \(g, h \in G\) we have \(f(h g h^{-1}) = q([h g h^{-1}]) = q([g]) = f(g)\), because \(h g h^{-1}\) and \(g\) are conjugate.

public theorem isClassFunction_iff_factor_conjClasses {G k : Type*}
    [Group G] (f : G → k) :
    IsClassFunction f ↔ ∃ g : ConjClasses G → k, ∀ x : G, f x = g (ConjClasses.mk x)

Sources

• J.-P. Serre, Linear Representations of Finite Groups, GTM 42, §2 (class functions as functions on conjugacy classes).

Uses 2 · Used by 1

Statement usesClass functions on a group

Proof usesClass functions agree on conjugate elements

Used byClass functions as functions on conjugacy classes

DefinitionClass functions as functions on conjugacy classes#✓fully proved

Let \(G\) be a group and \(k\) a field, and write \([x]\) for the conjugacy class of \(x \in G\). This is the \(k\)-linear isomorphism from the space of class functions \(G \to k\) to the vector space of all functions from the set of conjugacy classes of \(G\) to \(k\) that sends a class function \(f\) to the function \([x] \mapsto f(x)\); its inverse sends a function \(q\) on conjugacy classes to the class function \(x \mapsto q([x])\).

MathlibExt.GroupTheory.ClassFunctionWanted.classFunctionsEquivConjClasses · 25 lines

public def classFunctionsEquivConjClasses (G : Type*) [Group G] (k : Type*) [Field k] :
    classFunctions G k ≃ₗ[k] (ConjClasses G → k) where
  toFun f := Quotient.lift f fun _ _ => f.property.eq_of_isConj
  invFun q :=
    ⟨q ∘ ConjClasses.mk,
      (isClassFunction_iff_factor_conjClasses _).2 ⟨q, fun _ => rfl⟩⟩
  left_inv f := by
    apply Subtype.ext
    funext x
    rfl
  right_inv q := by
    funext c
    refine Quotient.inductionOn c ?_
    intro x
    rfl
  map_add' f g := by
    funext c
    refine Quotient.inductionOn c ?_
    intro x
    rfl
  map_smul' a f := by
    funext c
    refine Quotient.inductionOn c ?_
    intro x
    rfl

Uses 4 · Used by 3

Statement usesClass functions on a group · Class functions agree on conjugate elements · The space of class functions · Class functions factor through conjugacy classes

Used byEvaluating a class function on conjugacy classes · Lifting a function on conjugacy classes · Dimension of the space of class functions

TheoremEvaluating a class function on conjugacy classes#✓fully proved

Let \(G\) be a group and \(k\) a field. For every class function \(f : G \to k\) and every \(x \in G\), the function on conjugacy classes that corresponds to \(f\) under the linear isomorphism between class functions and functions on conjugacy classes takes the value \(f(x)\) at the conjugacy class of \(x\).

@[simp]
public theorem classFunctionsEquivConjClasses_apply_mk {G k : Type*} [Group G] [Field k]
    (f : classFunctions G k) (x : G) :
    classFunctionsEquivConjClasses G k f (ConjClasses.mk x) = (f : G → k) x

Uses 2

Statement usesThe space of class functions · Class functions as functions on conjugacy classes

TheoremLifting a function on conjugacy classes#✓fully proved

Let \(G\) be a group and \(k\) a field. For every function \(q\) from the set of conjugacy classes of \(G\) to \(k\) and every \(x \in G\), the class function that corresponds to \(q\) under the inverse of the linear isomorphism between class functions and functions on conjugacy classes takes at \(x\) the value of \(q\) at the conjugacy class of \(x\).

@[simp]
public theorem classFunctionsEquivConjClasses_symm_apply {G k : Type*} [Group G] [Field k]
    (q : ConjClasses G → k) (x : G) :
    (↑((classFunctionsEquivConjClasses G k).symm q) : G → k) x = q (ConjClasses.mk x)

Uses 2

Statement usesThe space of class functions · Class functions as functions on conjugacy classes

TheoremDimension of the space of class functions#✓fully proved

Let \(G\) be a finite group and \(k\) a field. The space of class functions \(G \to k\) is a \(k\)-vector space whose dimension equals the number of conjugacy classes of \(G\).

Proof: The linear isomorphism between class functions and functions on conjugacy classes reduces this to the space of all functions from the finite set of conjugacy classes of \(G\) to \(k\), whose dimension is the number of conjugacy classes.

public theorem finrank_classFunctions_eq_card_conjClasses (G : Type*)
    [Group G] [Fintype G] (k : Type*) [Field k] :
    Module.finrank k ↥(classFunctions G k) = Nat.card (ConjClasses G)

Sources

• J.-P. Serre, Linear Representations of Finite Groups, GTM 42, §2.7, Theorem 6 (dimension count for class functions).

Uses 2 · Used by 1

Statement usesThe space of class functions

Proof usesClass functions as functions on conjugacy classes

Used byNumber of irreducible characters

TheoremIrreducible representations are simple objects#✓fully proved

Let \(k\) be a field, \(G\) a group and \(\rho\) an irreducible representation of \(G\) on a finite-dimensional \(k\)-vector space \(V\). Then \(\rho\), viewed as an object of the category of finite-dimensional representations of \(G\) over \(k\), is a simple object.

public theorem simple_of_isIrreducible {k V : Type u} {G : Type v} [Field k] [Group G]
    [AddCommGroup V] [Module k V] [FiniteDimensional k V]
    (ρ : Representation k G V) [ρ.IsIrreducible] : Simple (FDRep.of ρ)

Used by 1

Used byA class function orthogonal to all irreducible characters vanishes

TheoremCharacters of nonisomorphic simple representations are linearly independent#✓fully proved

Let \(G\) be a finite group and let \((V_i)_{i \in I}\) be a family of simple finite-dimensional complex representations of \(G\) such that \(V_i \cong V_j\) implies \(i = j\). Then the characters of the \(V_i\) are linearly independent over \(\mathbb{C}\).

public theorem linearIndependent_character {I G : Type*} [Group G] [Finite G]
    (V : I → FDRep ℂ G) [∀ i, Simple (V i)]
    (hV : ∀ ⦃i j⦄, Nonempty (V i ≅ V j) → i = j) :
    LinearIndependent ℂ fun i ↦ (V i).character

Used by 1

Used byIrreducible characters are linearly independent

TheoremA class function orthogonal to all irreducible characters vanishes#✓fully proved

Let \(G\) be a finite group and let \(f : G \to \mathbb{C}\) satisfy \(f(hgh^{-1}) = f(g)\) for all \(g, h \in G\). Suppose that for every simple finite-dimensional complex representation \(W\) of \(G\), with character \(\chi_W\),

\[\frac{1}{|G|} \sum_{g \in G} f(g)\, \chi_W(g^{-1}) = 0.\]

Then \(f = 0\).

public theorem eq_zero_of_isClassFunction_of_orthogonal {G : Type*} [Group G] [Finite G]
    (f : G → ℂ) (hf : ∀ g h : G, f (h * g * h⁻¹) = f g)
    (horth : ∀ (W : FDRep ℂ G) [Simple W],
      (Nat.card G : ℂ)⁻¹ * ∑ᶠ g : G, f g * W.character g⁻¹ = 0) :
    f = 0

Uses 2 · Used by 1

Proof usesIrreducible representations are simple objects · Class functions on a group

Used byIrreducible characters span the class functions

TheoremIrreducible characters are linearly independent#✓fully proved

Let \(G\) be a finite group. The irreducible complex characters of \(G\), that is, the functions \(G \to \mathbb{C}\) that are the character of some simple finite-dimensional complex representation of \(G\), are linearly independent over \(\mathbb{C}\) in the space of functions \(G \to \mathbb{C}\).

Proof: Apply row orthogonality (C. Teleman, Representation Theory, Cambridge lecture notes, 2005, Theorem 8.10) as coordinate functionals to a vanishing finite linear combination of pairwise distinct irreducible characters.

public theorem linearIndependent_irrCharacters (G : Type*) [Group G]
    [Finite G] :
    LinearIndependent ℂ (Subtype.val :
      {χ : G → ℂ // ∃ V : FDRep ℂ G, Simple V ∧ V.character = χ} → (G → ℂ))

Sources

• J.-P. Serre, Linear Representations of Finite Groups, GTM 42, §2.5 (independence of irreducible characters).

Uses 1 · Used by 2

Proof usesCharacters of nonisomorphic simple representations are linearly independent

Used byNumber of irreducible characters · Irreducible characters span the class functions

TheoremIrreducible characters span the class functions#✓fully proved

Let \(G\) be a finite group and let \(f : G \to \mathbb{C}\) satisfy \(f(hgh^{-1}) = f(g)\) for all \(g, h \in G\). Then \(f\) is a \(\mathbb{C}\)-linear combination of irreducible complex characters of \(G\), that is, of functions \(G \to \mathbb{C}\) that are the character of some simple finite-dimensional complex representation of \(G\).

Proof: Subtract the orthogonal projection onto the irreducible characters. The remainder vanishes by Schur's lemma, Maschke's theorem, and the regular representation on a small model of the complex group algebra, as in the proof of Teleman's Theorem 9.3 (completeness of characters).

public theorem mem_span_irrCharacters_of_isClassFunction (G : Type*)
    [Group G] [Finite G] (f : G → ℂ) (hf : ∀ g h : G, f (h * g * h⁻¹) = f g) :
    f ∈ Submodule.span ℂ
      {χ : G → ℂ | ∃ V : FDRep ℂ G, Simple V ∧ V.character = χ}

Sources

• J.-P. Serre, Linear Representations of Finite Groups, GTM 42, §2.7, Theorem 6 (irreducible characters span the class functions).

Uses 3 · Used by 1

Proof usesA class function orthogonal to all irreducible characters vanishes · Characters are class functions · Irreducible characters are linearly independent

Used byNumber of irreducible characters

TheoremNumber of irreducible characters#✓fully proved

Let \(G\) be a finite group. The number of irreducible complex characters of \(G\), that is, of functions \(G \to \mathbb{C}\) that are the character of some simple finite-dimensional complex representation of \(G\), equals the number of conjugacy classes of \(G\).

Proof: The irreducible characters are linearly independent and span the class functions, so they form a basis of that space; compare its cardinality with the known dimension of that space (P. Etingof et al., Introduction to representation theory, arXiv:0901.0827, Theorem 3.5 and Corollary 3.6).

public theorem card_irrCharacters_eq_card_conjClasses (G : Type*)
    [Group G] [Finite G] :
    Nat.card {χ : G → ℂ // ∃ V : FDRep ℂ G, Simple V ∧ V.character = χ} =
      Nat.card (ConjClasses G)

Sources

• J.-P. Serre, Linear Representations of Finite Groups, GTM 42, §2.7 (number of irreducible characters).

Uses 6

Proof usesClass functions on a group · Characters are class functions · The space of class functions · Dimension of the space of class functions · Irreducible characters are linearly independent · Irreducible characters span the class functions

15 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.