Documentation

TauCeti.RepresentationTheory.CharacterTable.Kernel

The kernel of a complex character #

A representation ρ of a group has a kernel, the subgroup ρ.ker of the elements acting as the identity, and it is normal because it is the kernel of a homomorphism. The character sees that kernel: for a finite-dimensional complex representation and an element g of finite order,

g ∈ ρ.ker ↔ ρ.character g = ρ.character 1,

so the kernel is read off the character alone. That equivalence is the content of this file (Representation.mem_ker_iff_char_eq and its FDRep form FDRep.mem_ker_iff_char_eq), together with the consequence that the locus where a whole family of characters takes its value at the identity is the common kernel of that family (FDRep.coe_iInf_ker), a normal subgroup by FDRep.normal_iInf_ker (TauCeti/RepresentationTheory/FDRep.lean, that normality needing no characters).

One direction is immediate: if ρ g is the identity then its trace is finrank ℂ V. The other is not, and it is where the analysis enters. The eigenvalues of ρ g are roots of unity, so each has real part at most 1; the character value is those eigenvalues summed with the dimensions of the eigenspaces as weights, and those dimensions add up to finrank ℂ V. Attaining the value finrank ℂ V therefore forces every eigenvalue to have real part 1, hence to be 1, and ρ g is diagonalizable, so it is the identity. That argument is carried out for a bare endomorphism in Module.End.trace_eq_finrank_iff; here it is only transported to representations and characters.

Finite order is exactly what the statement needs, and it is all that is assumed here. For an element of infinite order there is no constraint on the eigenvalues of ρ g, and the character can take the value finrank ℂ V without ρ g being the identity: the representation of ℤ on ℂ² sending n to the unipotent matrix with off-diagonal entry n has character constantly 2, while no nonzero n acts as the identity. The statements are therefore given first for an element with g ^ n = 1, where the hypothesis is explicit, then for one of finite order; the statements about the whole kernel assume IsMulTorsion G, which a finite group satisfies by isOfFinOrder_of_finite.

The restriction to ℂ is inherited from Module.End.trace_eq_finrank_iff, and is one of proof rather than of substance: the equivalence holds over any field of characteristic zero, the eigenvalues generating a cyclotomic subfield of the algebraic closure that embeds into ℂ. What the proof compares are the real parts of the eigenvalues, which is what such an embedding buys; the descent along one is not carried out, and ℂ is where the character theory downstream of this file works.

The kernel description turns a character computation into a normal subgroup, as used in the character-theoretic proof of Frobenius's theorem. The exceptional characters of TauCeti/RepresentationTheory/Induction/ExceptionalCharacter.lean are irreducible characters of G, and the classical argument exhibits the Frobenius kernel TauCeti.frobeniusKernel as their common kernel; FDRep.coe_iInf_ker and FDRep.normal_iInf_ker are the generic half of that step, saying that such a common kernel is cut out by character equations and is a normal subgroup.

Main statements #

References #

source
theorem Representation.char_eq_finrank_iff_of_pow_eq_one {G : Type v} {V : Type w} [Monoid G] [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] (ρ : Representation ℂ G V) {g : G} {n : ℕ} (hn : n ≠ 0) (hg : g ^ n = 1) :
ρ.character g = ↑(Module.finrank ℂ V) ↔ ρ g = 1

A complex character attains its degree exactly on the elements acting as the identity. Stated for an element with g ^ n = 1; Representation.char_eq_finrank_iff is the form for an element of finite order.

source
theorem Representation.char_eq_finrank_iff {G : Type v} {V : Type w} [Monoid G] [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] (ρ : Representation ℂ G V) {g : G} (hg : IsOfFinOrder g) :
ρ.character g = ↑(Module.finrank ℂ V) ↔ ρ g = 1

A complex character attains its degree at an element of finite order exactly when that element acts as the identity.

source
theorem Representation.mem_ker_iff_char_eq {G : Type v} {V : Type w} [Group G] [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] (ρ : Representation ℂ G V) {g : G} (hg : IsOfFinOrder g) :
g ∈ MonoidHom.ker ρ ↔ ρ.character g = ρ.character 1

The kernel of a complex representation is read off its character: an element of finite order acts as the identity exactly when the character takes at it the value it takes at the identity.

source
theorem FDRep.mem_ker_iff_char_eq {G : Type u} [Group G] (V : FDRep ℂ G) {g : G} (hg : IsOfFinOrder g) :
g ∈ V.ρ.ker ↔ V.character g = V.character 1

The kernel of a finite-dimensional complex representation is read off its character: an element g of finite order acts as the identity exactly when the character takes at g the value it takes at the identity.

source
theorem FDRep.coe_ker {G : Type u} [Group G] (V : FDRep ℂ G) (hG : IsMulTorsion G) :
↑V.ρ.ker = {g : G | V.character g = V.character 1}

The kernel of a finite-dimensional complex representation of a torsion group, as the set of elements at which the character takes its value at the identity.

source
theorem FDRep.ker_eq_ker_of_char_eq {G : Type u} [Group G] (hG : IsMulTorsion G) {V W : FDRep ℂ G} (h : V.character = W.character) :
V.ρ.ker = W.ρ.ker

Representations with the same character have the same kernel. The kernel depends on the representation only through its character, being cut out by the character values.

source
theorem FDRep.ker_eq_top_iff {G : Type u} [Group G] (V : FDRep ℂ G) (hG : IsMulTorsion G) :
V.ρ.ker = ⊤ ↔ ∀ (g : G), V.character g = V.character 1

A representation of a torsion group is trivial exactly when its character is constant.

source
theorem FDRep.ker_eq_bot_iff {G : Type u} [Group G] (V : FDRep ℂ G) (hG : IsMulTorsion G) :
V.ρ.ker = ⊥ ↔ ∀ (g : G), V.character g = V.character 1 → g = 1

A representation of a torsion group is faithful exactly when its character detects the identity.

source
theorem FDRep.coe_iInf_ker {G : Type u} [Group G] {ι : Type u_1} (W : ι → FDRep ℂ G) (hG : IsMulTorsion G) :
↑(⨅ (i : ι), (W i).ρ.ker) = {g : G | ∀ (i : ι), (W i).character g = (W i).character 1}

The common kernel of a family of representations, as a set of character equations. An element lies in it exactly when every character of the family takes at it the value it takes at the identity. Together with FDRep.normal_iInf_ker this is how a character computation produces a normal subgroup.