The virtual-character lattice

The characters of the finite-dimensional representations of a monoid G over a field k are closed under addition, the character of a direct sum being the sum of the characters, but in general not under negation: over ℂ a character takes the positive value dim V at 1. The additive subgroup of G → k they generate, TauCeti.virtualCharacters k G, is the virtual-character lattice: its elements are the virtual characters of G, the differences of genuine characters.

It is an additive subgroup rather than a subring, but it is closed under the pointwise product (TauCeti.mul_mem_virtualCharacters), because the pointwise product of two characters is the character of the tensor product, and it contains the constant function 1, the character of the trivial representation.

Over an algebraically closed field in which |G| is invertible, and for G a finite group, the lattice is pinned down completely: it is the ℤ-span of the finitely many irreducible characters (TauCeti.virtualCharacters_eq_closure_irreducibleCharacters), which are a basis of the class functions. Every character is even a ℕ-combination of them, because its coefficient against χᵢ is the dimension of an intertwiner space. Consequently the character pairing takes integer values on the lattice: pairing two integer combinations of the irreducible characters gives the dot product of their integer coefficients. That integrality is what makes the classical norm-1 test work — a virtual character of norm 1 is, up to sign, an irreducible character.

Over a field of characteristic zero that is not algebraically closed the irreducible characters need not be orthonormal, but the norm-1 test survives in the form that realizes representations over a smaller field: writing a virtual character as χ_A - χ_B and cancelling the summands that A and B share, a virtual character of norm 1 and natural degree is the character of a simple representation whose endomorphisms are the scalars (TauCeti.exists_simple_character_eq_of_characterPairing_self_eq_one). This is how an irreducible complex character that is an integer combination of characters of representations over a subfield K of ℂ is seen to be the character of a representation over K.

Main definitions

• TauCeti.virtualCharacters: the virtual-character lattice of G over k.

Main results

• TauCeti.mem_virtualCharacters_iff_exists_eq_character_sub_character: the virtual characters are exactly the differences of two characters, with TauCeti.exists_eq_character_sub_character its forward direction.
• TauCeti.mul_mem_virtualCharacters and TauCeti.one_mem_virtualCharacters: the lattice is closed under the pointwise product and contains the constant 1.
• TauCeti.comp_mem_virtualCharacters: pulling back along a monoid homomorphism preserves virtual characters.
• TauCeti.virtualCharacters_le_classFunction: a virtual character is a class function, and TauCeti.conj_apply_of_mem_virtualCharacters: over ℂ inverting the argument conjugates the value, conj (f g) = f g⁻¹.
• TauCeti.character_eq_sum_nsmul_irreducibleCharacter: a character is the sum of the irreducible characters weighted by their multiplicities, and TauCeti.virtualCharacters_eq_closure_irreducibleCharacters: the lattice is the ℤ-span of the irreducible characters, with TauCeti.mem_virtualCharacters_iff its elementwise form.
• TauCeti.mem_of_mem_span_of_mem_virtualCharacters: a virtual character that is a ℤ[ζ]-combination of elements of a subgroup of the lattice is an integer combination of them, and more generally for any subring of k retracting additively onto ℤ.
• TauCeti.characterPairing_eq_intCast_sum and TauCeti.exists_characterPairing_eq_intCast: the character pairing is integer-valued on the lattice, computed by the dot product of the integer coefficients.
• TauCeti.exists_eq_irreducibleCharacter_or_neg: a virtual character of norm 1 is ± an irreducible character, and TauCeti.mem_irreducibleCharacters_of_characterPairing_self_eq_one fixes the sign when its degree is a natural number.
• TauCeti.exists_simple_character_eq_of_characterPairing_self_eq_one: over any field of characteristic zero, a virtual character of norm 1 and natural degree is the character of a simple representation whose endomorphisms are the scalars.
• TauCeti.natCard_nsmul_mem_span_irreducibleCharacters: |G| times a class function with values in a subring A containing the character values is an A-combination of the irreducible characters.

Implementation notes

The lattice is generated by the characters of the bundled representations FDRep k G, which makes closure under the pointwise product immediate from FDRep.char_tensor. The set TauCeti.irreducibleCharacters, by contrast, is cut out by representations on the coordinate spaces Fin n → k; FDRep.of mediates between the two, and nothing is lost, since the character of an irreducible representation on an arbitrary finite-dimensional space already lies in TauCeti.irreducibleCharacters.

Following the roadmap, the lattice is an AddSubgroup (G → k) and not a Subring (G → k): the additive structure is what the integrality arguments downstream use, and closure under the pointwise product is recorded as the lemma TauCeti.mul_mem_virtualCharacters rather than built into the interface. The coefficients in TauCeti.mem_virtualCharacters_iff are genuine integers, the scalars (c i : k) appearing only because the ambient module is a k-module; they are determined by the element only in characteristic zero, since in positive characteristic the cast ℤ → k is not injective.

References

This is the virtual-character-lattice item of Layer 3 of the character theory roadmap and the virtualCharacters target of Layer 6 of the induction and restriction roadmap. See I. M. Isaacs, Character Theory of Finite Groups (1976), Chapter 2 and Lemma 4.7, or J.-P. Serre, Linear Representations of Finite Groups (1977), Sections 2.5 and 9. The norm-1 test over an arbitrary field of characteristic zero is the argument of Serre, Section 12.3 (realizability over cyclotomic fields), and of Isaacs, Chapter 10.

def TauCeti.virtualCharacters (k : Type u) (G : Type v) [Field k] [Monoid G] : AddSubgroup (G → k)

The virtual-character lattice of G over k: the additive subgroup of G → k generated by the characters of the finite-dimensional representations of G.

Its elements, the virtual characters, are the differences of genuine characters: characters are closed under addition, so an integer combination of them is a difference of two of them.

Equations

• TauCeti.virtualCharacters k G = AddSubgroup.closure (Set.range FDRep.character)

@[simp]

theorem TauCeti.character_mem_virtualCharacters {k : Type u} {G : Type v} [Field k] [Monoid G] (V : FDRep k G) : V.character ∈ virtualCharacters k G

A character is a virtual character.

theorem TauCeti.virtualCharacters_le {k : Type u} {G : Type v} [Field k] [Monoid G] {H : AddSubgroup (G → k)} (h : ∀ (V : FDRep k G), V.character ∈ H) : virtualCharacters k G ≤ H

The generation principle for the virtual-character lattice: an additive subgroup of G → k containing every character contains every virtual character.

theorem TauCeti.exists_eq_character_sub_character {k : Type u} {G : Type v} [Field k] [Monoid G] {f : G → k} (hf : f ∈ virtualCharacters k G) : ∃ (A : FDRep k G) (B : FDRep k G), f = A.character - B.character

A virtual character is a difference of two characters: the characters are closed under addition, the character of a direct sum being the sum of the characters, so an integer combination of characters is the character of one representation minus that of another.

theorem TauCeti.mem_virtualCharacters_iff_exists_eq_character_sub_character {k : Type u} {G : Type v} [Field k] [Monoid G] {f : G → k} : f ∈ virtualCharacters k G ↔ ∃ (A : FDRep k G) (B : FDRep k G), f = A.character - B.character

A function G → k is a virtual character exactly when it is a difference of two characters. This holds over any field and for any monoid G, unlike the description TauCeti.mem_virtualCharacters_iff as an integer combination of irreducible characters.

theorem TauCeti.mul_mem_virtualCharacters {k : Type u} {G : Type v} [Field k] [Monoid G] {f g : G → k} (hf : f ∈ virtualCharacters k G) (hg : g ∈ virtualCharacters k G) : f * g ∈ virtualCharacters k G

The virtual-character lattice is closed under the pointwise product. The product of two characters is the character of the tensor product, and multiplication by a fixed function is additive, so the property propagates through the additive generation of the lattice.

The lattice is nevertheless kept as an AddSubgroup: multiplicativity is recorded by this lemma rather than by bundling the carrier as a Subring (G → k), the additive interface being the one the roadmap prescribes.

@[simp]

theorem TauCeti.one_mem_virtualCharacters {k : Type u} {G : Type v} [Field k] [Monoid G] : 1 ∈ virtualCharacters k G

The constant function 1 is a virtual character, being the character of the trivial one-dimensional representation.

theorem TauCeti.comp_mem_virtualCharacters {k : Type u} {G : Type v} [Field k] [Monoid G] {H : Type w} [Monoid H] (φ : H →* G) {f : G → k} (hf : f ∈ virtualCharacters k G) : f ∘ ⇑φ ∈ virtualCharacters k H

Pulling back along a monoid homomorphism preserves virtual characters. The pullback f ∘ φ of a character along φ : H →* G is the character of the representation restricted along φ, Mathlib's Action.res, and pullback is additive, so the property propagates through the additive generation of the lattice. Restriction to a subgroup and inflation from a quotient are the two instances.

theorem TauCeti.comp_mem_span_virtualCharacters {k : Type u} {G : Type v} [Field k] [Monoid G] (A : Subring k) {H : Type w} [Monoid H] (φ : H →* G) {f : G → k} (hf : f ∈ Submodule.span ↥A ↑(virtualCharacters k G)) : f ∘ ⇑φ ∈ Submodule.span ↥A ↑(virtualCharacters k H)

Pulling back along a monoid homomorphism preserves A-combinations of virtual characters, for any subring A of k: pullback is A-linear and, by TauCeti.comp_mem_virtualCharacters, carries virtual characters to virtual characters.

theorem TauCeti.virtualCharacters_le_classFunction {k : Type u} {G : Type v} [Field k] [Group G] : virtualCharacters k G ≤ (ClassFunction k G).toAddSubgroup

The virtual-character lattice is contained in the class functions: a virtual character is constant on conjugacy classes, being an integer combination of characters, each of which is.

Applied to a hypothesis hf : f ∈ virtualCharacters k G this gives f ∈ ClassFunction k G.

theorem TauCeti.conj_apply_of_mem_virtualCharacters {G : Type v} [Group G] [Finite G] {f : G → ℂ} (hf : f ∈ virtualCharacters ℂ G) (g : G) : (starRingEnd ℂ) (f g) = f g⁻¹

Over ℂ, inverting the argument conjugates the value of a virtual character of a finite group: conj (f g) = f g⁻¹. This holds for genuine characters (FDRep.conj_char), and both sides are additive in f.

This is not a simp lemma: TauCeti.character_mem_virtualCharacters and TauCeti.irreducibleCharacter_mem_virtualCharacters discharge its hypothesis, so as a conditional simp lemma it fires on the characters themselves and makes the more specific FDRep.conj_char and TauCeti.conj_irreducibleCharacter redundant, which the simpNF linter rejects.

theorem TauCeti.irreducibleCharacters_subset_range {k : Type u} {G : Type v} [Field k] [Group G] : irreducibleCharacters k G ⊆ Set.range FDRep.character

Every irreducible character is the character of a bundled representation, hence generates the virtual-character lattice.

theorem TauCeti.character_eq_sum_nsmul_irreducibleCharacter {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [IsAlgClosed k] [Invertible ↑(Nat.card G)] (V : FDRep k G) : V.character = ∑ i : Fin (Nat.card (ConjClasses G)), Module.finrank k (Representation.IntertwiningMap V.ρ (irreducibleRepresentation k i)) • irreducibleCharacter k i

A character is the sum of the irreducible characters weighted by their multiplicities. The coefficient of χᵢ in the expansion of χ_V in the basis of irreducible characters is the pairing ⟨χᵢ, χ_V⟩, which is the dimension of the space of intertwiners V → Vᵢ, so the coefficients are natural numbers: the multiplicities with which the irreducibles occur in V.

theorem TauCeti.character_mem_closure_irreducibleCharacters {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [IsAlgClosed k] [Invertible ↑(Nat.card G)] (V : FDRep k G) : V.character ∈ AddSubgroup.closure (irreducibleCharacters k G)

Every character lies in the ℤ-span of the irreducible characters, its multiplicities being natural numbers.

theorem TauCeti.virtualCharacters_eq_closure_irreducibleCharacters {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [IsAlgClosed k] [Invertible ↑(Nat.card G)] : virtualCharacters k G = AddSubgroup.closure (irreducibleCharacters k G)

The virtual-character lattice is the ℤ-span of the irreducible characters. One inclusion is that every character expands over the irreducible characters with natural-number coefficients; the other is that an irreducible character is a character.

@[simp]

theorem TauCeti.irreducibleCharacter_mem_virtualCharacters {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [IsAlgClosed k] [Invertible ↑(Nat.card G)] (i : Fin (Nat.card (ConjClasses G))) : irreducibleCharacter k i ∈ virtualCharacters k G

An irreducible character is a virtual character.

theorem TauCeti.range_irreducibleCharacter {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [IsAlgClosed k] [Invertible ↑(Nat.card G)] : Set.range (irreducibleCharacter k) = irreducibleCharacters k G

The enumerated irreducible characters exhaust the irreducible characters.

theorem TauCeti.mem_virtualCharacters_iff {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [IsAlgClosed k] [Invertible ↑(Nat.card G)] {f : G → k} : f ∈ virtualCharacters k G ↔ ∃ (c : Fin (Nat.card (ConjClasses G)) → ℤ), f = ∑ i : Fin (Nat.card (ConjClasses G)), ↑(c i) • irreducibleCharacter k i

A function G → k is a virtual character exactly when it is an integer combination of the irreducible characters.

The coefficients c are genuine integers, but they are pinned down by f only in characteristic zero: what the irreducible characters determine are the scalars (c i : k), and in positive characteristic the cast ℤ → k is not injective.

theorem TauCeti.mem_of_mem_span_of_mem_virtualCharacters {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [IsAlgClosed k] [Invertible ↑(Nat.card G)] (A : Subring k) (t : ↥A →+ ℤ) (ht : t 1 = 1) {V : AddSubgroup (G → k)} (hV : V ≤ virtualCharacters k G) {f : G → k} (hf : f ∈ virtualCharacters k G) (hfA : f ∈ Submodule.span ↥A ↑V) : f ∈ V

Virtual characters descend from A-coefficients to integer coefficients. Let A be a subring of k admitting an additive map t : A → ℤ with t 1 = 1, such as ℤ[ζ] for a root of unity ζ in characteristic zero (PowerBasis.exists_linearMap_apply_one). If V is an additive subgroup of the virtual characters, then a virtual character that is an A-linear combination of elements of V already lies in V: Submodule.span A V ∩ R(G) = V.

theorem TauCeti.natCard_nsmul_mem_span_irreducibleCharacters {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [IsAlgClosed k] [Invertible ↑(Nat.card G)] (A : Subring k) {f : G → k} (hf : f ∈ ClassFunction k G) (hfA : ∀ (g : G), f g ∈ A) (hA : ∀ (i : Fin (Nat.card (ConjClasses G))) (g : G), irreducibleCharacter k i g ∈ A) : Nat.card G • f ∈ Submodule.span (↥A) (irreducibleCharacters k G)

A class function with values in a subring A is, once multiplied by |G|, an A-combination of the irreducible characters, provided A contains the values of the irreducible characters: the coefficient of χᵢ in |G| • f is the group sum ∑ g, χᵢ(g) f(g⁻¹).

This is the expansion of a class function in the basis of irreducible characters with the division by |G| in the character pairing cleared, so that only the ring operations of A are needed. It is the integrality input of Brauer's induction theorem.

theorem TauCeti.characterPairing_eq_intCast_sum {k : Type u} {G : Type v} [Field k] [Group G] [Fintype G] [IsAlgClosed k] [Invertible ↑(Nat.card G)] {f₁ f₂ : ↥(ClassFunction k G)} {c d : Fin (Nat.card (ConjClasses G)) → ℤ} (h₁ : ↑f₁ = ∑ i : Fin (Nat.card (ConjClasses G)), ↑(c i) • irreducibleCharacter k i) (h₂ : ↑f₂ = ∑ i : Fin (Nat.card (ConjClasses G)), ↑(d i) • irreducibleCharacter k i) : (ClassFunction.characterPairing f₁) f₂ = ↑(∑ i : Fin (Nat.card (ConjClasses G)), c i * d i)

The character pairing of two virtual characters is the dot product of their integer coefficients. The irreducible characters are orthonormal, so pairing two integer combinations of them multiplies the coefficients termwise.

theorem TauCeti.exists_characterPairing_eq_intCast {k : Type u} {G : Type v} [Field k] [Group G] [Fintype G] [IsAlgClosed k] [Invertible ↑(Nat.card G)] {f₁ f₂ : ↥(ClassFunction k G)} (h₁ : ↑f₁ ∈ virtualCharacters k G) (h₂ : ↑f₂ ∈ virtualCharacters k G) : ∃ (n : ℤ), (ClassFunction.characterPairing f₁) f₂ = ↑n

The character pairing is integer-valued on the virtual-character lattice.

theorem TauCeti.exists_eq_irreducibleCharacter_or_neg {k : Type u} {G : Type v} [Field k] [Group G] [Fintype G] [IsAlgClosed k] [CharZero k] [Invertible ↑(Nat.card G)] {f : ↥(ClassFunction k G)} (hf : ↑f ∈ virtualCharacters k G) (hnorm : (ClassFunction.characterPairing f) f = 1) : ∃ (i : Fin (Nat.card (ConjClasses G))), ↑f = irreducibleCharacter k i ∨ ↑f = -irreducibleCharacter k i

A virtual character of norm 1 is ± an irreducible character. Writing the virtual character as ∑ᵢ cᵢ χᵢ with integer coefficients, its norm is ∑ᵢ cᵢ²; a sum of squares of integers is 1 only when a single coefficient is ±1 and the rest vanish.

This is the norm-1 classification of virtual characters: the conclusion is genuinely a sign ambiguity, since -χᵢ also has norm 1 and is not itself an irreducible character. It specializes to the usual irreducibility test only for a genuine character, where the coefficients are non-negative and so the negative case cannot occur. It is the tool behind the exceptional-character arguments of Frobenius's theorem.

theorem TauCeti.mem_irreducibleCharacters_of_characterPairing_self_eq_one {k : Type u} {G : Type v} [Field k] [Group G] [Fintype G] [IsAlgClosed k] [CharZero k] [Invertible ↑(Nat.card G)] {f : ↥(ClassFunction k G)} (hf : ↑f ∈ virtualCharacters k G) (hnorm : (ClassFunction.characterPairing f) f = 1) {n : ℕ} (hn : ↑f 1 = ↑n) : ↑f ∈ irreducibleCharacters k G

A virtual character of norm 1 whose degree is a natural number is an irreducible character. By TauCeti.exists_eq_irreducibleCharacter_or_neg it is ±χ, and -χ is excluded: its degree -χ(1) is negative, so it is not the image of a natural number.

theorem TauCeti.exists_simple_character_eq_of_characterPairing_self_eq_one {k : Type u} {G : Type v} [Field k] [Group G] [Fintype G] [CharZero k] {f : ↥(ClassFunction k G)} (hf : ↑f ∈ virtualCharacters k G) (hnorm : (ClassFunction.characterPairing f) f = 1) {n : ℕ} (hn : ↑f 1 = ↑n) : ∃ (V : FDRep k G), CategoryTheory.Simple V ∧ Module.finrank k (V ⟶ V) = 1 ∧ V.character = ↑f

A virtual character of norm 1 and natural degree is the character of an absolutely irreducible representation, over any field of characteristic zero. If f is an integer combination of characters of representations of G over k, with ⟨f, f⟩ = 1 and f 1 a natural number, then f is the character of a simple object V of FDRep k G whose equivariant endomorphisms are the scalars.

Over an algebraically closed field this is TauCeti.mem_irreducibleCharacters_of_characterPairing_self_eq_one. Over a general field the irreducible characters need not be orthonormal (the rotation representation of ℤ/3 on ℝ² is irreducible of norm 2), so instead f = χ_A - χ_B is reduced by cancelling common summands of A and B until no nonzero intertwiner B → A is left; then ⟨f, f⟩ = dim End(A) + dim End(B) forces one of A, B to be zero and the other to have one-dimensional endomorphism algebra, and the degree rules out A = 0.

This is the step that turns a character identity over a subfield k of ℂ into the realizability over k of an irreducible complex representation.