Representations of finite abelian groups

TheoremSimple finite-dimensional representations of a monoid are irreducible#✓fully proved

Let \(k\) be a field and let \(G\) be a monoid. If a finite-dimensional representation \(V\) of \(G\) over \(k\) is simple as an object of the category of finite-dimensional representations of \(G\) over \(k\), then \(V\) is irreducible as a representation: \(V \ne 0\), and the only subrepresentations of \(V\) are \(0\) and \(V\).

theorem _root_.FDRep.isIrreducible_of_simple {k G : Type*} [Field k] [Monoid G]
    (V : FDRep k G) [Simple V] : Representation.IsIrreducible V.ρ
Used by 1
Used bySimple finite-dimensional representations of commutative monoids are one-dimensional

TheoremSimple finite-dimensional representations of commutative monoids are one-dimensional#✓fully proved

Let \(k\) be an algebraically closed field and let \(G\) be a commutative monoid. Every finite-dimensional representation \(V\) of \(G\) over \(k\) that is simple as an object of the category of finite-dimensional representations of \(G\) over \(k\) has dimension \(1\) over \(k\).

theorem _root_.FDRep.finrank_eq_one_of_isMulCommutative
    {k G : Type*} [Field k] [IsAlgClosed k] [Monoid G] [IsMulCommutative G]
    (V : FDRep k G) [Simple V] : Module.finrank k V = 1
Uses 1 · Used by 3
Proof usesSimple finite-dimensional representations of a monoid are irreducible
Used byThe character of a simple representation as a monoid homomorphism · Characters of simple representations of commutative monoids are multiplicative · Simple representations of commutative monoids act by scalars

TheoremSimple representations of commutative monoids act by scalars#✓fully proved

Let \(k\) be an algebraically closed field, \(G\) a monoid with commutative multiplication, and \(V\) a simple finite-dimensional representation of \(G\) over \(k\) (a simple object of the category of finite-dimensional representations), with action \(\rho\) and character \(\chi_V(g) = \operatorname{tr} \rho(g)\). Then for every \(g \in G\) the map \(\rho(g)\) is scalar multiplication by \(\chi_V(g)\), that is, \(\rho(g) = \chi_V(g) \cdot \mathrm{id}_V\).

theorem _root_.FDRep.rho_eq_character_smul_of_simple
    {k G : Type*} [Field k] [IsAlgClosed k] [Monoid G] [IsMulCommutative G]
    (V : FDRep k G) [Simple V] (g : G) :
    V.ρ g = V.character g • LinearMap.id
Uses 1 · Used by 1
Proof usesSimple finite-dimensional representations of commutative monoids are one-dimensional
Used byCharacters of simple representations of commutative monoids are multiplicative

TheoremCharacters of simple representations of commutative monoids are multiplicative#✓fully proved

Let \(k\) be an algebraically closed field, let \(G\) be a commutative monoid, and let \(V\) be a finite-dimensional representation of \(G\) over \(k\) that is simple as an object of the category of finite-dimensional representations of \(G\) over \(k\). Let \(\chi_V : G \to k\) be the character of \(V\), where \(\chi_V(g)\) is the trace of the action of \(g\) on \(V\). Then \(\chi_V(gh) = \chi_V(g)\,\chi_V(h)\) for all \(g, h \in G\).

theorem _root_.FDRep.character_mul_of_simple
    {k G : Type*} [Field k] [IsAlgClosed k] [Monoid G] [IsMulCommutative G]
    (V : FDRep k G) [Simple V] (g h : G) :
    V.character (g * h) = V.character g * V.character h
Uses 2 · Used by 1
Proof usesSimple finite-dimensional representations of commutative monoids are one-dimensional · Simple representations of commutative monoids act by scalars
Used byThe character of a simple representation as a monoid homomorphism

DefinitionThe character of a simple representation as a monoid homomorphism#✓fully proved

Let \(k\) be an algebraically closed field, let \(G\) be a commutative monoid, and let \(V\) be a finite-dimensional representation of \(G\) over \(k\) that is simple as an object of the category of finite-dimensional representations of \(G\) over \(k\). The character \(\chi_V : G \to k\) of \(V\), where \(\chi_V(g)\) is the trace of the action of \(g\) on \(V\), satisfies \(\chi_V(1) = 1\) and \(\chi_V(gh) = \chi_V(g)\,\chi_V(h)\) for all \(g, h \in G\); this is \(\chi_V\) regarded as a monoid homomorphism from \(G\) to \(k\).

noncomputable def _root_.FDRep.characterMonoidHom
    {k G : Type*} [Field k] [IsAlgClosed k] [Monoid G] [IsMulCommutative G]
    (V : FDRep k G) [Simple V] : G →* k where
  toFun := V.character
  map_one' := by simp [V.finrank_eq_one_of_isMulCommutative]
  map_mul' := V.character_mul_of_simple
Uses 2 · Used by 2
Statement usesCharacters of simple representations of commutative monoids are multiplicative · Simple finite-dimensional representations of commutative monoids are one-dimensional
Used byCharacters of simple representations of a finite abelian group are homomorphisms · The character homomorphism has the character as its underlying function

TheoremThe character homomorphism has the character as its underlying function#✓fully proved

Let \(k\) be an algebraically closed field, let \(G\) be a commutative monoid, and let \(V\) be a finite-dimensional representation of \(G\) over \(k\) that is simple as an object of the category of finite-dimensional representations of \(G\) over \(k\). The character of \(V\), regarded as a monoid homomorphism from \(G\) to \(k\), has the character \(\chi_V : G \to k\) of \(V\) as its underlying function, where \(\chi_V(g)\) is the trace of the action of \(g\) on \(V\).

@[simp]
theorem _root_.FDRep.coe_characterMonoidHom
    {k G : Type*} [Field k] [IsAlgClosed k] [Monoid G] [IsMulCommutative G]
    (V : FDRep k G) [Simple V] : ⇑V.characterMonoidHom = V.character
Uses 1 · Used by 1
Statement usesThe character of a simple representation as a monoid homomorphism
Used byCharacters of simple representations of a finite abelian group are homomorphisms

DefinitionThe one-dimensional representation of a homomorphism#✓fully proved

Let \(k\) be a field, let \(G\) be a monoid, and let \(\varphi : G \to k\) be a monoid homomorphism. This is the finite-dimensional representation \(k_\varphi\) of \(G\) on the one-dimensional space \(k\) in which each \(g \in G\) acts by multiplication by \(\varphi(g)\), that is, by the linear map \(x \mapsto \varphi(g)\,x\).

noncomputable def _root_.FDRep.ofMonoidHom {k G : Type*} [Field k] [Monoid G]
    (φ : G →* k) : FDRep k G :=
  FDRep.of
    { toFun := fun g => φ g • (LinearMap.id : k →ₗ[k] k)
      map_one' := by
        ext
        simp
      map_mul' := by
        intro g h
        ext
        simp [mul_smul, mul_comm] }
Used by 5
Used byEvery homomorphism of a finite abelian group to the complex numbers is a simple character · The action in the one-dimensional representation of a homomorphism · The character of the representation of a homomorphism is the homomorphism · The representation of a homomorphism is one-dimensional · The representation of a homomorphism is simple

TheoremThe action in the one-dimensional representation of a homomorphism#✓fully proved

Let \(k\) be a field, let \(G\) be a monoid, let \(\varphi : G \to k\) be a monoid homomorphism, and let \(k_\varphi\) be the one-dimensional representation of \(G\) on \(k\) defined by \(\varphi\). For every \(g \in G\), the action of \(g\) on \(k_\varphi\) is \(\varphi(g)\) times the identity map of \(k\).

@[simp]
theorem _root_.FDRep.ofMonoidHom_ρ {k G : Type*} [Field k] [Monoid G]
    (φ : G →* k) (g : G) : (FDRep.ofMonoidHom φ).ρ g = φ g • LinearMap.id
Uses 1
Statement usesThe one-dimensional representation of a homomorphism

TheoremThe representation of a homomorphism is one-dimensional#✓fully proved

Let \(k\) be a field, let \(G\) be a monoid, let \(\varphi : G \to k\) be a monoid homomorphism, and let \(k_\varphi\) be the representation of \(G\) on \(k\) in which each \(g \in G\) acts by multiplication by \(\varphi(g)\). Then \(k_\varphi\) has dimension \(1\) over \(k\).

@[simp]
theorem _root_.FDRep.ofMonoidHom_finrank {k G : Type*} [Field k] [Monoid G]
    (φ : G →* k) : Module.finrank k (FDRep.ofMonoidHom φ) = 1
Uses 1
Statement usesThe one-dimensional representation of a homomorphism

TheoremThe character of the representation of a homomorphism is the homomorphism#✓fully proved

Let \(k\) be a field, let \(G\) be a monoid, let \(\varphi : G \to k\) be a monoid homomorphism, and let \(k_\varphi\) be the one-dimensional representation of \(G\) on \(k\) in which each \(g \in G\) acts by multiplication by \(\varphi(g)\). The character of \(k_\varphi\) is \(\varphi\): the trace of the action of each \(g \in G\) on \(k_\varphi\) is \(\varphi(g)\).

@[simp]
theorem _root_.FDRep.ofMonoidHom_character {k G : Type*} [Field k] [Monoid G]
    (φ : G →* k) : (FDRep.ofMonoidHom φ).character = φ
Uses 1 · Used by 1
Statement usesThe one-dimensional representation of a homomorphism
Used byEvery homomorphism of a finite abelian group to the complex numbers is a simple character

TheoremThe representation of a homomorphism is simple#✓fully proved

Let \(k\) be a field, let \(G\) be a monoid, let \(\varphi : G \to k\) be a monoid homomorphism, and let \(k_\varphi\) be the one-dimensional representation of \(G\) on \(k\) in which each \(g \in G\) acts by multiplication by \(\varphi(g)\). Then \(k_\varphi\) is a simple object of the category of finite-dimensional representations of \(G\) over \(k\).

theorem _root_.FDRep.ofMonoidHom_simple {k G : Type*} [Field k] [Monoid G]
    (φ : G →* k) : Simple (FDRep.ofMonoidHom φ)
Uses 1 · Used by 1
Statement usesThe one-dimensional representation of a homomorphism
Used byEvery homomorphism of a finite abelian group to the complex numbers is a simple character

TheoremCharacters of simple representations of a finite abelian group are homomorphisms#✓fully proved

Let \(G\) be a finite abelian group and let \(V\) be a simple finite-dimensional complex representation of \(G\). Then there is a monoid homomorphism \(\varphi : G \to \mathbb{C}\) such that the character of \(V\) equals \(\varphi\).

Proof: Simplicity of \(V\) makes it irreducible, and complex irreducible representations of an abelian group are one-dimensional (the corollary in Wikipedia, “Schur's lemma”), so \(V\) is one-dimensional. Endomorphisms of a one-dimensional space are scalars, and their traces give the multiplicative character.

public theorem abelian_simple_char_is_hom (G : Type*) [CommGroup G]
    [Finite G] (V : FDRep ℂ G) [Simple V] :
    ∃ φ : G →* ℂ, V.character = ⇑φ
Sources
  • J.-P. Serre, Linear Representations of Finite Groups, GTM 42, §2.8 (degree-one characters of abelian groups).
Uses 2
Proof usesThe character of a simple representation as a monoid homomorphism · The character homomorphism has the character as its underlying function

TheoremEvery homomorphism of a finite abelian group to the complex numbers is a simple character#✓fully proved

Let \(G\) be a finite abelian group and let \(\varphi : G \to \mathbb{C}\) be a monoid homomorphism. Then there is a simple finite-dimensional complex representation \(V\) of \(G\) whose character equals \(\varphi\).

Proof: Let each \(g \in G\) act on the one-dimensional space \(\mathbb{C}\) by the scalar \(\varphi(g)\); its trace is \(\varphi(g)\). One-dimensional modules are simple. Wikipedia, “Representation theory of finite groups”, notes that the irreducible characters of an abelian group are its homomorphisms to \(\mathbb{C}^\times\).

public theorem abelian_hom_is_simple_char (G : Type*) [CommGroup G]
    [Finite G] (φ : G →* ℂ) :
    ∃ V : FDRep ℂ G, Simple V ∧ V.character = ⇑φ
Sources
  • J.-P. Serre, Linear Representations of Finite Groups, GTM 42, Ch. I (one-dimensional representations from characters).
Uses 3
Proof usesThe one-dimensional representation of a homomorphism · The character of the representation of a homomorphism is the homomorphism · The representation of a homomorphism is simple

TheoremCharacters determine simple representations of a finite abelian group#✓fully proved

Let \(G\) be a finite abelian group and let \(V\) and \(W\) be simple finite-dimensional complex representations of \(G\), with characters \(\chi_V\) and \(\chi_W\). If \(\chi_V = \chi_W\), then \(V\) and \(W\) are isomorphic.

Proof: For functions \(\chi, \psi : G \to \mathbb{C}\) write \(\langle \chi, \psi \rangle = \frac{1}{|G|} \sum_{g \in G} \chi(g)\,\psi(g^{-1})\), where \(|G|\) is the order of \(G\). The orthonormality of irreducible characters gives \(\langle \chi_V, \chi_V \rangle = 1\). Replacing the second character by the equal character \(\chi_W\) gives \(\langle \chi_V, \chi_W \rangle = 1\), which forces \(V \cong W\). This is the orthonormality of irreducible characters in Wikipedia, “Character theory”.

public theorem abelian_simple_iso_of_char_eq (G : Type*) [CommGroup G]
    [Finite G] (V W : FDRep ℂ G) [Simple V] [Simple W]
    (h : V.character = W.character) : Nonempty (V ≅ W)
Sources
  • J.-P. Serre, Linear Representations of Finite Groups, GTM 42, §2.8 (characters determine representations of abelian groups).
14 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.