Characters of representations

TheoremCharacter values at inverses are complex conjugates#✓fully proved

Let \(\rho\) be a representation of a finite group \(G\) on a finite-dimensional complex vector space \(V\), with character \(\chi_\rho\). For every \(g \in G\), \(\chi_\rho(g^{-1}) = \overline{\chi_\rho(g)}\).

theorem char_inv_eq_conj
    {G : Type u} [Group G] [Fintype G]
    {V : Type u} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
    (ρ : Representation ℂ G V) (g : G) :
    ρ.character g⁻¹ = starRingEnd ℂ (ρ.character g)

Used by 1

Used byCharacter of the dual representation

TheoremCharacter of the dual representation#✓fully proved

Let \(\rho\) be a representation of a finite group \(G\) on a finite-dimensional complex vector space \(V\), and let \(\rho^*\) be its dual representation. For every \(g \in G\), the character of \(\rho^*\) at \(g\) is the complex conjugate of the character of \(\rho\) at \(g\): \(\chi_{\rho^*}(g) = \overline{\chi_\rho(g)}\).

theorem char_dual_eq_conj
    {G : Type u} [Group G] [Fintype G]
    {V : Type u} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
    (ρ : Representation ℂ G V) (g : G) :
    ρ.dual.character g = starRingEnd ℂ (ρ.character g)

Uses 1

Proof usesCharacter values at inverses are complex conjugates

DefinitionClass inner product#✓fully proved

Let \(G\) be a finite group and \(k\) a field in which \(|G|\) is invertible. For functions \(f_1, f_2 \colon G \to k\), their class inner product is \(\langle f_1, f_2 \rangle = |G|^{-1} \sum_{g \in G} f_1(g) f_2(g^{-1})\).

noncomputable def classInnerProduct {G : Type u} [Group G] [Fintype G] {k : Type u}
    [Field k] [Invertible (Nat.card G : k)] (f₁ f₂ : G → k) : k :=
  (Nat.card G : k)⁻¹ * ∑ g : G, f₁ g * f₂ g⁻¹

Used by 1

Used byCharacter criterion for irreducibility

TheoremCharacter criterion for irreducibility#✓fully proved

A finite-dimensional representation σ of a finite group over an algebraically closed field of characteristic zero is irreducible if and only if the self-pairing of its character is 1.

public theorem irreducible_iff_classInnerProduct_self_eq_one
    {G : Type u} [Group G] [Fintype G] {k : Type u} [Field k]
    {V : Type u} [AddCommGroup V] [Module k V] [FiniteDimensional k V]
    [Invertible (Nat.card G : k)] [IsAlgClosed k] [CharZero k]
    (σ : Representation k G V) :
    σ.IsIrreducible ↔ classInnerProduct σ.character σ.character = 1

Uses 1

Statement usesClass inner product

TheoremEigenvalues of \(\rho(g)\) are roots of unity of order dividing that of \(g\)#✓fully proved

Let \(\rho\) be a representation of a finite group \(G\) on a finite-dimensional complex vector space \(V\), let \(g \in G\), and let \(\operatorname{ord}(g)\) be the order of \(g\). Every eigenvalue \(\mu\) of \(\rho(g)\) satisfies \(\mu^{\operatorname{ord}(g)} = 1\).

The minimal polynomial of \(\rho(g)\) divides \(X^{\operatorname{ord}(g)} - 1\), and \(\mu\) is a root of the minimal polynomial.

theorem hasEigenvalue_pow_orderOf_eq_one
    {G : Type u} [Group G] [Fintype G]
    {V : Type u} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
    (ρ : Representation ℂ G V) (g : G) {μ : ℂ}
    (hμ : Module.End.HasEigenvalue (ρ g) μ) :
    μ ^ orderOf g = 1

Used by 1

Used byEigenvalues of \(\rho(g)\) are \(|G|\)-th roots of unity

TheoremEigenvalues of \(\rho(g)\) are \(|G|\)-th roots of unity#✓fully proved

Let \(\rho\) be a representation of a finite group \(G\) on a finite-dimensional complex vector space \(V\), and let \(g \in G\). Every eigenvalue \(\mu\) of \(\rho(g)\) satisfies \(\mu^{|G|} = 1\).

This follows because the order of \(g\) divides \(|G|\).

theorem hasEigenvalue_pow_card_eq_one
    {G : Type u} [Group G] [Fintype G]
    {V : Type u} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
    (ρ : Representation ℂ G V) (g : G) {μ : ℂ}
    (hμ : Module.End.HasEigenvalue (ρ g) μ) :
    μ ^ Fintype.card G = 1

Uses 1 · Used by 1

Proof usesEigenvalues of \(\rho(g)\) are roots of unity of order dividing that of \(g\)

Used byCharacteristic roots of \(\rho(g)\) are \(|G|\)-th roots of unity

TheoremCharacteristic roots of \(\rho(g)\) are \(|G|\)-th roots of unity#✓fully proved

Let \(\rho\) be a representation of a finite group \(G\) on a finite-dimensional complex vector space \(V\), and let \(g \in G\). Every root \(\mu\) of the characteristic polynomial of the matrix of \(\rho(g)\) in a fixed basis of \(V\) satisfies \(\mu^{|G|} = 1\).

theorem char_charpoly_roots_pow_eq_one
    {G : Type u} [Group G] [Fintype G]
    {V : Type u} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
    (ρ : Representation ℂ G V) (g : G) :
    ∀ μ ∈ ((LinearMap.toMatrix (Module.finBasis ℂ V) (Module.finBasis ℂ V)
      (ρ g)).charpoly.roots), μ ^ Fintype.card G = 1

Uses 1

Proof usesEigenvalues of \(\rho(g)\) are \(|G|\)-th roots of unity

TheoremParseval / sum-of-squares for characters#✓fully proved

If χ is a combination of the characters of pairwise non-equivalent irreducible representations with coefficients n i, then the self-pairing of χ is the sum of the squares of the coefficients. In particular, for a single irreducible ρ, taking χ = χ_ρ gives self-pairing 1, and for the regular character the formula recovers ∑ (dim ρ_i) ^ 2 = |G| once the regular character is expanded in irreducibles.

theorem character_selfPairing_eq_sum_sq
    {G : Type u} [Group G] [Fintype G] {k : Type u} [Field k]
    [Invertible (Nat.card G : k)] [IsAlgClosed k]
    {ι : Type u} [Fintype ι] [DecidableEq ι]
    {V : ι → Type u} [∀ i, AddCommGroup (V i)] [∀ i, Module k (V i)]
    [∀ i, FiniteDimensional k (V i)]
    (ρ : ∀ i, Representation k G (V i))
    [∀ i, (ρ i).IsIrreducible]
    (h_pairwise : ∀ i j, i ≠ j → ¬Nonempty (Representation.Equiv (ρ i) (ρ j)))
    (n : ι → ℕ)
    (χ : G → k)
    (hχ : ∀ g : G, χ g = ∑ i, (n i : k) * (ρ i).character g) :
    (Nat.card G : k)⁻¹ * ∑ g : G, χ g * χ g⁻¹ = ∑ i, ((n i : k) ^ 2)

TheoremSum of squares of the Wedderburn block sizes#✓fully proved

If |G| is nonzero in an algebraically closed field, the group algebra of a finite group is a product of matrix algebras with nonzero block sizes whose squares sum to |G|.

theorem wedderburn_sum_sq_eq_card
    (k : Type u) [Field k] [IsAlgClosed k]
    (G : Type u) [Group G] [Fintype G] [NeZero (Nat.card G : k)] :
    ∃ (n : ℕ) (d : Fin n → ℕ), (∀ i, NeZero (d i)) ∧
      (∑ i, (d i) ^ 2 = Nat.card G) ∧
      Nonempty (MonoidAlgebra k G ≃ₐ[k] Π i, Matrix (Fin (d i)) (Fin (d i)) k)

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.