Representation theory

AbbreviationRepresentation#

A representation of a group \(G\) is a way of letting \(G\) act on a vector space by linear maps, compatibly with the group multiplication. It turns questions about an abstract group into questions of linear algebra, where matrices, traces and eigenvalues are available. Representations are a main tool for studying finite groups and for the symmetry arguments of number theory, geometry and physics.

Definition

Let \(k\) be a field, \(G\) a group and \(V\) a vector space over \(k\). A representation of \(G\) on \(V\) is a map \(\rho\) assigning to each \(g \in G\) a linear map \(\rho(g) \colon V \to V\) such that

\[\rho(gh) = \rho(g)\,\rho(h) \quad \text{for all } g, h \in G, \qquad \rho(e) = \mathrm{id}_V,\]

where \(e\) is the identity of \(G\). In other words, \(\rho\) is a homomorphism from \(G\) to the linear maps of \(V\) under composition. Since \(\rho(g)\rho(g^{-1}) = \rho(g^{-1})\rho(g) = \mathrm{id}_V\), each \(\rho(g)\) is a bijection, so \(\rho\) can be regarded as a homomorphism from \(G\) to the group of invertible linear maps of \(V\); conversely, any such homomorphism is a representation. One often writes \(g \cdot v\) for \(\rho(g)v\), and calls \(V\) itself the representation when \(\rho\) is understood. The dimension of \(V\) is the degree of the representation. If \(V\) has finite dimension \(n\), a choice of basis turns each \(\rho(g)\) into an invertible matrix, and \(\rho\) into a homomorphism from \(G\) to the general linear group of \(n \times n\) matrices over \(k\).

If \(\sigma\) is a representation of \(G\) on \(W\), a linear map \(f \colon V \to W\) is an intertwining map when \(f(\rho(g)v) = \sigma(g)f(v)\) for all \(g\) and \(v\). Two representations are equivalent when a bijective intertwining map joins them; equivalent representations are regarded as the same.

Examples
  • The trivial representation. Every \(g\) acts as the identity.
  • One-dimensional representations. A representation on \(k\) itself is a homomorphism from \(G\) to the nonzero elements of \(k\) under multiplication. The signature of a permutation gives such a representation of the symmetric group, with each permutation acting by \(\pm 1\). For a cyclic group of order \(n\) with generator \(g\) and an \(n\)-th root of unity \(\zeta\) in \(\mathbb{C}\), letting \(g^m\) act by multiplication by \(\zeta^m\) gives a representation on \(\mathbb{C}\).
  • Permutation representations. If \(G\) acts on a set \(X\), let \(k[X]\) be the vector space with basis \(\{e_x : x \in X\}\). This gives a permutation representation, in which \(g\) sends \(e_x\) to \(e_{gx}\). The case \(X = G\), with \(G\) acting on itself by left multiplication, is the regular representation on the group algebra \(k[G]\).
Constructions

A subspace \(W \subseteq V\) with \(\rho(g)W \subseteq W\) for all \(g\) is a subrepresentation, and restricting each \(\rho(g)\) to \(W\) gives a representation of \(G\) on \(W\). Representations of \(G\) can be combined: there are direct sums, on which \(G\) acts in each summand; tensor products, on which \(g\) acts by \(\rho(g) \otimes \sigma(g)\) (see tensor product); and duals, on which \(g\) acts on the dual space by the transpose of \(\rho(g^{-1})\).

Irreducible representations

A representation is irreducible when it is nonzero and its only subrepresentations are \(0\) and the whole space. Irreducible representations are the building blocks of the theory.

Both hypotheses of Maschke's theorem matter. Over a field of prime characteristic \(p\), the cyclic group of order \(p\) acts on \(k^2\) with generator acting by \((x, y) \mapsto (x + y, y)\); the line \(y = 0\) is invariant, but it is the only invariant line, so it has no invariant complement. The same matrix gives a representation of the integers on \(\mathbb{C}^2\) with the same defect.

Modules over the group algebra

A representation \(\rho\) extends linearly to an algebra homomorphism from the group algebra \(k[G]\) to the linear maps of \(V\), which makes \(V\) a module over \(k[G]\). Conversely, a \(k[G]\)-module \(M\) is a representation of \(G\), with \(g\) acting as multiplication by the basis element \(g\). Under this dictionary subrepresentations are submodules, and a representation is irreducible exactly when its module is simple, so representation theory becomes part of module theory. In the module form, Maschke's theorem says that every submodule of a \(k[G]\)-module has a complementary submodule, for \(G\) finite and \(|G| \neq 0\) in \(k\).

The character of a finite-dimensional representation is the function \(g \mapsto \operatorname{tr} \rho(g)\); for finite groups over \(\mathbb{C}\) it determines the representation up to equivalence, and the orthogonality of characters organizes the irreducible ones. Finite-dimensional representations and intertwining maps form a category. A representation is a group action by linear maps; variants require continuity for topological groups, or replace \(G\) by a Lie algebra or an associative algebra.

In Mathlib

Mathlib defines a representation for any monoid \(G\), any semiring \(k\) and any module \(V\) over \(k\), as a monoid homomorphism from \(G\) to the \(k\)-linear maps of \(V\) under composition. The definition is an abbreviation for this type of homomorphisms rather than a structure, so \(V\) stays a separate parameter; invertibility of each \(\rho(g)\) is not assumed and follows when \(G\) is a group. Irreducibility and semisimplicity are stated for vector spaces over a field. Intertwining maps and equivalences are bundled structures. The module over the group algebra lives on a separate copy of \(V\), so that the original scalar action of \(k\) and the new action of \(k[G]\) do not clash; likewise, the representation built from a \(k[G]\)-module acts on a copy of that module. Bundled categories of representations, in which an object packages a module with its representation, sit on top of this definition, and Maschke's theorem is proved in its module form with the hypothesis that \(|G|\) is nonzero in \(k\), from which every such representation is shown to be semisimple.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibRepresentation
Uses 5 · Used by 5
Statement usesGroup · Field · Module · Linear map · Group morphism
Used byCategory of finite-dimensional representations · Character · Orthogonality of characters · Maschke theorem · Irreducible representation

AbbreviationCategory of finite-dimensional representations#

The category of finite-dimensional representations of a group \(G\) over a field \(k\) has as objects the finite-dimensional representations of \(G\) over \(k\), and as morphisms the linear maps that commute with the action of \(G\). Treating representations as the objects of a category, rather than one at a time, is the natural setting for the main tools of representation theory: Schur's lemma is a statement about its morphisms, semisimplicity is a statement about its subobjects, and tensor products and duals of representations make it a rigid monoidal category.

Definition

Let \(k\) be a field and \(G\) a group. An object of the category of finite-dimensional representations, often written \(\mathrm{FDRep}_k(G)\), is a pair \((V, \rho_V)\) where \(V\) is a finite-dimensional vector space over \(k\) and \(\rho_V \colon G \to \mathrm{GL}(V)\) is a group homomorphism. A morphism \(f \colon (V, \rho_V) \to (W, \rho_W)\) is a linear map \(f \colon V \to W\) that is equivariant, meaning

\[f \circ \rho_V(g) = \rho_W(g) \circ f \quad \text{for every } g \in G.\]

Composition and identities are those of linear maps, and the composite of two equivariant maps is again equivariant. Two representations are isomorphic in this category exactly when there is a linear isomorphism between them that intertwines the two actions. The same definition makes sense for a monoid \(G\), with \(\rho_V\) a monoid homomorphism into the endomorphisms of \(V\); for a group the maps \(\rho_V(g)\) are then automatically invertible, since \(\rho_V(g)\rho_V(g^{-1}) = \rho_V(g^{-1})\rho_V(g) = \rho_V(1)\) is the identity.

Examples
  • The trivial representation \(k\), on which every element of \(G\) acts as the identity, is the unit for the tensor product described below.
  • For a finite group \(G\), the group algebra \(k[G]\) with \(G\) acting by left multiplication on basis vectors is the regular representation, of dimension \(|G|\). More generally, an action of \(G\) on a finite set \(X\) gives a permutation representation on the vector space with basis \(X\).
  • The sign of a permutation gives a one-dimensional representation of the symmetric group \(S_n\), on which \(\sigma\) acts as multiplication by \(\operatorname{sgn}(\sigma)\).
  • For the cyclic group of order \(n\) with generator \(g\), and a primitive \(n\)-th root of unity \(\zeta \in \mathbb{C}\), each \(j = 0, 1, \dots, n-1\) gives a one-dimensional complex representation with \(g\) acting as multiplication by \(\zeta^j\); no two of these are isomorphic.
Properties

The morphisms between two objects form a finite-dimensional vector space, and composition is bilinear, so the category is \(k\)-linear. It has kernels, cokernels and all finite limits, and it is an abelian category.

Tensor products and duals. The tensor product \(V \otimes W\) carries the action \(g \mapsto \rho_V(g) \otimes \rho_W(g)\), which makes the category a monoidal category with the trivial representation as unit. The dual space \(V^*\) is a representation with \(g\) acting by the transpose of \(\rho_V(g^{-1})\), and the space of all linear maps from \(V\) to \(W\), with \(g\) acting by \(\varphi \mapsto \rho_W(g) \circ \varphi \circ \rho_V(g)^{-1}\), is isomorphic as a representation to \(V^* \otimes W\). The vectors of this space fixed by \(G\) are exactly the morphisms from \(V\) to \(W\).

Simple objects. The simple objects of the category are the irreducible representations. When \(k\) is algebraically closed, Schur's lemma says that for simple objects \(V\) and \(W\) the space of morphisms from \(V\) to \(W\) has dimension \(1\) if \(V \cong W\) and \(0\) otherwise.

Semisimplicity. Suppose now that \(G\) is finite and that the characteristic of \(k\) does not divide \(|G|\), so that \(|G|\) is invertible in \(k\). Maschke's theorem says that every submodule of a module over the group algebra \(k[G]\) has a complementary submodule. Applied to representations, it shows that every invariant subspace has an invariant complement, so every object of the category is a direct sum of simple objects and every short exact sequence splits. If \(k\) is moreover algebraically closed, then a representation \(V\) is simple exactly when its endomorphisms form a one-dimensional space.

Characters. The character of \(V\) is the function \(\chi_V(g) = \operatorname{tr} \rho_V(g)\) on \(G\). Isomorphic representations have the same character, and the character of \(V \otimes W\) is the product \(\chi_V \chi_W\). For a finite group whose order is invertible in \(k\), averaging characters computes dimensions of morphism spaces:

\[\frac{1}{|G|} \sum_{g \in G} \chi_W(g)\,\chi_V(g^{-1}) = \dim_k \operatorname{Hom}_G(V, W),\]

where \(\operatorname{Hom}_G(V, W)\) is the space of morphisms from \(V\) to \(W\) in the category, that is, the equivariant linear maps, and the right side is read as an element of \(k\). Combined with Schur's lemma over an algebraically closed field, this gives the orthogonality of characters: for simple \(V\) and \(W\) the average of \(\chi_V(g)\chi_W(g^{-1})\) over \(G\) is \(1\) if \(V \cong W\) and \(0\) otherwise.

The category of all representations of \(G\) over \(k\), without the finiteness condition, contains this one as a full subcategory. It is equivalent to the category of modules over the group algebra \(k[G]\), a special case of the category of modules over a ring. A finite group can be recovered from its category of finite-dimensional representations together with the tensor product and the functor that forgets the action, as the group of automorphisms of that functor compatible with tensor products; this is the starting point of Tannakian reconstruction.

In Mathlib

Mathlib defines the category for an arbitrary ring \(R\) and monoid \(G\), as the category of actions of \(G\) on finitely generated \(R\)-modules; over a field, finitely generated modules are exactly the finite-dimensional vector spaces. An object is bundled: it carries its module and the monoid homomorphism from \(G\) to the endomorphisms of that module, which can be recovered from it, and over a commutative ring a representation on a finitely generated module can be packaged as an object. Over a commutative ring the morphisms between two objects are, as a module, the same as the morphisms between them in the category of all representations. Irreducible representations are the simple objects in the categorical sense, and the hypothesis on the characteristic is stated as invertibility (or nonvanishing) of \(|G|\) in \(k\). When \(R\) is a field and \(G\) a group, Mathlib records that every object has a dual through a right rigid structure, and the isomorphism between linear maps and \(V^* \otimes W\) above is a separate result.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibFDRep
Uses 4 · Used by 1
Statement usesRepresentation · Category · Finite-dimensionality · Linear map
Used bySchur's lemma (Linear representations)

DefinitionCharacter#

The character of a finite-dimensional representation of a group is the function that assigns to each group element the trace of the linear map by which it acts. It compresses a representation, a family of matrices, into a single scalar-valued function on the group, yet for finite groups over the complex numbers it loses nothing: two representations with the same character are isomorphic. Characters turn many questions about representations into calculations with sums over the group, and they are the main computational tool of the representation theory of finite groups.

Definition

Let \(G\) be a group, \(k\) a field, and \(V\) a finite-dimensional vector space over \(k\) on which \(G\) acts through a homomorphism \(\rho\) from \(G\) to the invertible linear maps of \(V\). The character of \(V\) is the function \(\chi_V \colon G \to k\) given by \(\chi_V(g) = \operatorname{tr} \rho(g)\), the trace of the linear map \(\rho(g)\). After choosing a basis of \(V\), \(\chi_V(g)\) is the sum of the diagonal entries of the matrix of \(\rho(g)\); since similar matrices have the same trace, the result does not depend on the basis. The definition uses only the multiplication of \(G\), so it applies equally to a monoid acting by linear maps that need not be invertible. The dimension of \(V\) is called the degree of the character.

Examples
  • One-dimensional representations. If \(V\) is a line, each \(\rho(g)\) is multiplication by a nonzero scalar, and \(\chi_V\) is the resulting homomorphism from \(G\) to the multiplicative group of \(k\). In particular the trivial representation on \(k\) has the constant character \(1\). For the cyclic group of order \(n\) generated by \(g\) and a complex \(n\)-th root of unity \(\zeta\), the rule \(g^j \mapsto \zeta^j\) is such a character.
  • Permutation representations. If \(G\) acts on a finite set \(X\), it permutes the standard basis of the space \(k^X\) of functions on \(X\). Each \(\rho(g)\) is then a permutation matrix, whose diagonal entries are \(1\) exactly at the points of \(X\) fixed by \(g\), so \(\chi(g)\) is the number of fixed points of \(g\), read in \(k\). For the regular representation, where \(G\) acts on itself by left multiplication, this gives \(\chi(1) = |G|\) and \(\chi(g) = 0\) for \(g \neq 1\).

The symmetric group on three letters. Over the complex numbers, the permutation group \(S_3\) has three conjugacy classes (the identity, the transpositions and the \(3\)-cycles) and three irreducible representations: the trivial one, the sign representation, and the two-dimensional representation on the plane of vectors in \(\mathbb{C}^3\) whose coordinates sum to \(0\). Their characters, listed class by class, are

\[\begin{array}{c|ccc} & 1 & (1\,2) & (1\,2\,3) \\ \hline \text{trivial} & 1 & 1 & 1 \\ \text{sign} & 1 & -1 & 1 \\ \text{standard} & 2 & 0 & -1 \end{array}\]

The permutation representation on \(\{1, 2, 3\}\) has character \((3, 1, 0)\), the sum of the trivial and standard characters, matching its decomposition into those two pieces.

Properties

Throughout, \(V\) and \(W\) are finite-dimensional representations of \(G\) over \(k\).

Orthogonality

Suppose now that \(G\) is finite and that its order \(|G|\) is invertible in \(k\), that is, the characteristic of \(k\) does not divide \(|G|\). Averaging a character over the group gives the dimension of the space of invariant vectors: \(\frac{1}{|G|} \sum_{g \in G} \chi_V(g)\) equals the dimension of the subspace of vectors fixed by all of \(G\). Applied to the space of linear maps from \(V\) to \(W\), this shows that \(\frac{1}{|G|} \sum_{g \in G} \chi_W(g)\,\chi_V(g^{-1})\) is the dimension of the space of \(G\)-equivariant linear maps from \(V\) to \(W\), both dimensions read in \(k\). If in addition \(k\) is algebraically closed and \(V\) and \(W\) are irreducible, then Schur's lemma makes this dimension \(1\) or \(0\), which gives the orthogonality of characters: \(\frac{1}{|G|} \sum_{g \in G} \chi_V(g)\,\chi_W(g^{-1})\) is \(1\) if \(V\) and \(W\) are isomorphic and \(0\) otherwise.

Over the complex numbers, the irreducible characters of a finite group form an orthonormal basis of the space of class functions, so their number equals the number of conjugacy classes. Their orthonormality, together with Maschke's theorem, is what makes the character determine the representation over the complex numbers. The irreducible representations and their characters are recorded in the character table of the group. The one-dimensional characters of any group are its homomorphisms to the multiplicative group of the field. For a finite abelian group, the one-dimensional complex characters take values in the unit circle and form the dual group of harmonic analysis.

In Mathlib

Mathlib defines the character for objects of the category of finite-dimensional representations over a field, with the group allowed to be any monoid; the results that use inverses assume a group, and the averaging and orthogonality results assume a finite group whose order is invertible in the field. The trace is the basis-free trace of a linear map, and the character takes values in the field itself, so dimensions appear as their images in the field: in positive characteristic they are known only modulo the characteristic. Irreducible representations are the simple objects of the category, and orthogonality is stated with \(g^{-1}\) in place of complex conjugation, which makes it valid over every algebraically closed field whose characteristic does not divide the order of the group. A parallel version, the character of a representation given as a homomorphism into the linear maps of a vector space, carries the same basic results.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibFDRep.character
Uses 5 · Used by 1
Statement usesGroup · Field · Linear map · Representation · Finite-dimensionality
Used byOrthogonality of characters

TheoremOrthogonality of characters#

The orthogonality of characters is the theorem that the characters of the irreducible representations of a finite group over the complex numbers (more generally, over an algebraically closed field whose characteristic does not divide the order of the group) form an orthonormal family for a natural pairing of functions on the group. It is the basic computational tool of character theory: it lets one decide whether a representation is irreducible, find how often each irreducible representation occurs in a given one, and bound the number of irreducible representations, all from a finite table of numbers.

Statement

Let \(G\) be a finite group and \(k\) an algebraically closed field whose characteristic does not divide the order \(|G|\), so that \(|G|\) is invertible in \(k\); the complex numbers are the main example. For functions \(\varphi, \psi \colon G \to k\) put

\[\langle \varphi, \psi \rangle = \frac{1}{|G|} \sum_{g \in G} \varphi(g)\,\psi(g^{-1}).\]

The substitution \(g \mapsto g^{-1}\) shows that this pairing is symmetric. If \(V\) and \(W\) are irreducible finite-dimensional representations of \(G\) over \(k\), with characters \(\chi_V\) and \(\chi_W\), then \(\langle \chi_V, \chi_W \rangle\) equals \(1\) if \(V\) and \(W\) are isomorphic and \(0\) otherwise.

Over the complex numbers the pairing can be written with complex conjugation. Each \(\rho(g)\) has finite order, so its eigenvalues are roots of unity, and the eigenvalues of \(\rho(g^{-1})\) are their inverses, which are their conjugates. Hence \(\chi(g^{-1}) = \overline{\chi(g)}\), and the theorem says that the irreducible characters are orthonormal for the Hermitian inner product \(\frac{1}{|G|}\sum_g \varphi(g)\overline{\psi(g)}\), which explains the name.

Examples
  • Cyclic groups. Let \(G\) be cyclic of order \(n\) with generator \(g\), and let \(\zeta = e^{2\pi i/n}\). For each \(j = 0, \dots, n-1\) the rule \(g^m \mapsto \zeta^{jm}\) is a one-dimensional representation, hence irreducible, and its character is \(\chi_j(g^m) = \zeta^{jm}\). Then \(\langle \chi_j, \chi_l \rangle = \frac1n \sum_{m=0}^{n-1} \zeta^{(j-l)m}\), a geometric sum that equals \(1\) when \(j = l\) and \(0\) otherwise, because \(\zeta^{j-l}\) is then an \(n\)th root of unity different from \(1\).
  • The symmetric group \(S_3\). Over \(\mathbb{C}\) it has three irreducible representations: the trivial one, the sign, and the two-dimensional standard representation on the vectors in \(\mathbb{C}^3\) with coordinate sum \(0\). On the identity, the three transpositions and the two 3-cycles their characters take the values \((1,1,1)\), \((1,-1,1)\) and \((2,0,-1)\). Every element of \(S_3\) is conjugate to its inverse, so all character values are real and \(\chi(g^{-1}) = \chi(g)\). For the standard character, \(\langle \chi, \chi \rangle = \frac16(4 + 3 \cdot 0 + 2 \cdot 1) = 1\), while its pairing with the trivial character is \(\frac16(2 + 0 - 2) = 0\).
Consequences
  • The general formula. For finite-dimensional representations \(V\) and \(W\), not necessarily irreducible, and any field \(k\) in which \(|G|\) is invertible, \(\langle \chi_W, \chi_V \rangle\) is the dimension of the space of \(G\)-equivariant linear maps from \(V\) to \(W\), read as an element of \(k\). Taking \(V\) to be the trivial one-dimensional representation, whose character is constantly \(1\), the average of \(\chi_W\) over \(G\) is the dimension of the subspace of vectors fixed by \(G\), again read in \(k\).
  • Linear independence. Under the hypotheses of the statement, characters are constant on conjugacy classes, since \(\chi_V(hgh^{-1}) = \chi_V(g)\) for all \(g, h\). If \(\chi_1, \dots, \chi_r\) are the characters of pairwise non-isomorphic irreducible representations and \(\sum_i a_i \chi_i = 0\), pairing with \(\chi_j\) gives \(a_j = 0\). So these characters are linearly independent in the space of class functions, whose dimension is the number of conjugacy classes, and \(G\) has at most that many irreducible representations up to isomorphism.
  • Multiplicities. Assume moreover that \(k\) has characteristic \(0\). By Maschke's theorem every finite-dimensional representation \(V\) is a direct sum \(W_1^{m_1} \oplus \cdots \oplus W_r^{m_r}\), where \(W_1, \dots, W_r\) is a full set of pairwise non-isomorphic irreducible representations and some \(m_j\) may be \(0\), and orthogonality gives \(m_j = \langle \chi_V, \chi_{W_j} \rangle\) and \(\langle \chi_V, \chi_V \rangle = \sum_j m_j^2\). Hence \(V\) is irreducible exactly when \(\langle \chi_V, \chi_V \rangle = 1\). The character determines every multiplicity \(m_j\), hence the isomorphism class, so two representations with the same character are isomorphic. For example, the permutation representation of \(S_3\) on \(\mathbb{C}^3\) has character \((3, 1, 0)\), the number of fixed points, so it is the trivial representation plus the standard one.
Proof

There are three steps. First, for any finite-dimensional representation \(\rho\) on \(U\), the operator \(e = \frac{1}{|G|}\sum_g \rho(g)\) is a projection of \(U\) onto the subspace \(U^G\) of fixed vectors. The trace of a projection is the dimension of its image (read in \(k\)), so the average of \(\chi_U\) equals \(\dim U^G\).

Second, the space of all linear maps from \(W\) to \(V\) is a representation, with \(g\) acting by \(f \mapsto \rho_V(g) \circ f \circ \rho_W(g)^{-1}\). Its character at \(g\) is \(\chi_W(g^{-1})\,\chi_V(g)\), and its fixed vectors are exactly the \(G\)-equivariant maps. The first step therefore gives \(\langle \chi_V, \chi_W \rangle = \dim \operatorname{Hom}_G(W, V)\).

Third, Schur's lemma over an algebraically closed field says that for irreducible \(V\) and \(W\) the space of \(G\)-equivariant maps between them has dimension \(1\) if they are isomorphic and \(0\) otherwise. Combining the second and third steps, \(\langle \chi_V, \chi_W \rangle = \dim \operatorname{Hom}_G(W, V)\) is \(1\) if \(W \cong V\), equivalently \(V \cong W\), and \(0\) otherwise.

The irreducible characters are not only orthonormal but span the space of class functions, so they form an orthonormal basis of the class functions, and the number of irreducible representations equals the number of conjugacy classes. Reading the character table by columns instead of rows gives the second orthogonality relation: over \(\mathbb{C}\), the sum of \(\chi(g)\overline{\chi(h)}\) over all irreducible characters \(\chi\) is the order of the centralizer of \(g\) when \(g\) and \(h\) are conjugate and \(0\) otherwise.

In Mathlib

Mathlib states the theorem for the bundled category of finite-dimensional representations of a group over a field. Irreducibility is expressed as being a simple object of that category, isomorphism means isomorphism in the category, and the condition on the characteristic is an assumption that the order of the group is invertible in the field. The pairing is the one above with \(g^{-1}\), with no complex conjugation, so it makes sense over any field, and the two sides are equal as elements of the field, the right side being its \(1\) or \(0\). Mathlib also has a version for irreducible representations on modules that are not bundled into a category, where finite-dimensionality is not assumed but follows from irreducibility. The general formula and the fixed-vector formula do not need the field to be algebraically closed; their right sides are dimensions cast into the field, so in positive characteristic they determine a dimension only modulo the characteristic.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibFDRep.char_orthonormal
Uses 6
Statement usesCharacter · Representation · Irreducible representation · Algebraically closed field · Characteristic of a ring
Proof usesSchur's lemma (Linear representations)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.