Faithful tensor generation

The Burnside–Brauer theorem bounds the tensor powers needed to contain every irreducible complex representation of a finite group by the number of distinct values of a faithful character. The proof interpolates the indicator of the identity fibre of that character.

FDRep.exists_pos_finrank_hom_tensorPower proves the slightly stronger assertion that every nonzero finite-dimensional representation has a nonzero map into one of these tensor powers. For an irreducible source such a map is injective, so this is occurrence in an actual tensor power, not merely membership in a span of characters. The zero-fold tensor power is included; no positivity or irreducibility assumption on the faithful representation is needed.

The multiplicities mₙ = dim Hom_G(X, V^⊗n) are collected in the formal power series FDRep.tensorMultiplicitySeries V X = ∑ₙ mₙ zⁿ. Since mₙ = |G|⁻¹ ∑_g χ_V(g)ⁿ χ_X(g⁻¹), it is the finite sum of geometric series |G|⁻¹ ∑_g χ_X(g⁻¹) (1 - χ_V(g) z)⁻¹ (FDRep.tensorMultiplicitySeries_eq_characterFractions). Consequently it is a rational function: multiplied by Q(z) = ∏_a (1 - a z), the product over the distinct character values a, it becomes a polynomial of degree less than the number of values, and the multiplicities satisfy the linear recurrence whose characteristic polynomial is ∏_a (T - a). These identities hold over every field in which |G| is invertible, with the multiplicities read in that field.

For a faithful representation of positive dimension d, interpolating the identity fibre after multiplying by Tᴮ shows that every window [B, B + r) of r consecutive exponents, r the number of character values, contains a tensor power into which a given nonzero representation maps nontrivially (FDRep.exists_mem_Ico_pos_finrank_hom_tensorPower). This gives the sharp positive-power bound 1 ≤ n ≤ r and occurrence in arbitrarily large tensor powers, so that the tensor-multiplicity series has infinitely many nonzero coefficients.

References

• I. M. Isaacs, Character Theory of Finite Groups, Theorem 4.3.
• B. Steinberg, On the Burnside–Brauer–Steinberg theorem, arXiv:1409.7632, Introduction and Remark 1.

The construction uses Mathlib's Lagrange.basis and the finite-order trace criterion Representation.char_eq_finrank_iff.

noncomputable def FDRep.characterValues {k : Type u} {G : Type v} [Field k] [Monoid G] [Finite G] (V : FDRep k G) : Finset k

The distinct values of the character, without a choice of conjugacy representatives.

@[simp]

theorem FDRep.mem_characterValues {k : Type u} {G : Type v} [Field k] [Monoid G] [Finite G] (V : FDRep k G) (z : k) : z ∈ V.characterValues ↔ ∃ (g : G), V.character g = z

theorem FDRep.characterValues_eq_image {k : Type u} {G : Type v} [Field k] [Monoid G] [Finite G] [Fintype G] [DecidableEq k] (V : FDRep k G) : V.characterValues = Finset.image V.character Finset.univ

Character values are the image of the character on all group elements.

noncomputable def FDRep.characterValueCount {k : Type u} {G : Type v} [Field k] [Monoid G] [Finite G] (V : FDRep k G) : ℕ

The number of distinct values of a character.

@[simp]

theorem FDRep.card_characterValues {k : Type u} {G : Type v} [Field k] [Monoid G] [Finite G] (V : FDRep k G) : V.characterValues.card = V.characterValueCount

theorem FDRep.characterValueCount_pos {k : Type u} {G : Type v} [Field k] [Monoid G] [Finite G] (V : FDRep k G) : 0 < V.characterValueCount

A character has at least one value, even on the zero representation.

theorem FDRep.characterValues_eq_of_iso {k : Type u} {G : Type v} [Field k] [Monoid G] [Finite G] (V : FDRep k G) {W : FDRep k G} (e : V ≅ W) : V.characterValues = W.characterValues

Isomorphic representations have the same character values.

theorem FDRep.characterValueCount_eq_of_iso {k : Type u} {G : Type v} [Field k] [Monoid G] [Finite G] (V : FDRep k G) {W : FDRep k G} (e : V ≅ W) : V.characterValueCount = W.characterValueCount

Isomorphism does not change the number of character values.

noncomputable def FDRep.characterInterpolator {k : Type u} {G : Type v} [Field k] [Monoid G] [Finite G] (V : FDRep k G) : Polynomial k

The Lagrange polynomial isolating the character value at the identity.

@[simp]

theorem FDRep.natDegree_characterInterpolator {k : Type u} {G : Type v} [Field k] [Monoid G] [Finite G] (V : FDRep k G) : V.characterInterpolator.natDegree = V.characterValueCount - 1

The interpolator has degree one less than the number of distinct character values.

theorem FDRep.eval_characterInterpolator_eq_sum {k : Type u} {G : Type v} [Field k] [Monoid G] [Finite G] (V : FDRep k G) (x : k) : Polynomial.eval x V.characterInterpolator = ∑ n ∈ Finset.range V.characterValueCount, V.characterInterpolator.coeff n * x ^ n

The coefficient expansion of the interpolator, including its constant term.

theorem FDRep.eval_characterInterpolator {k : Type u} {G : Type v} [Field k] [Monoid G] [Finite G] [DecidableEq k] (V : FDRep k G) (g : G) : Polynomial.eval (V.character g) V.characterInterpolator = if V.character g = V.character 1 then 1 else 0

Evaluation of the interpolator detects the identity's character value.

noncomputable def FDRep.tensorMultiplicityDenominator {k : Type u} {G : Type v} [Field k] [Monoid G] [Finite G] (V : FDRep k G) : Polynomial k

The polynomial Q(z) = ∏_a (1 - a z) over the distinct character values a. It clears the denominators of the tensor-multiplicity series; a zero character value contributes the factor 1.

theorem FDRep.tensorMultiplicityDenominator_def {k : Type u} {G : Type v} [Field k] [Monoid G] [Finite G] (V : FDRep k G) : V.tensorMultiplicityDenominator = ∏ a ∈ V.characterValues, (1 - Polynomial.C a * Polynomial.X)

@[simp]

theorem FDRep.coeff_zero_tensorMultiplicityDenominator {k : Type u} {G : Type v} [Field k] [Monoid G] [Finite G] (V : FDRep k G) : V.tensorMultiplicityDenominator.coeff 0 = 1

The denominator has constant term one.

theorem FDRep.natDegree_tensorMultiplicityDenominator_le {k : Type u} {G : Type v} [Field k] [Monoid G] [Finite G] (V : FDRep k G) : V.tensorMultiplicityDenominator.natDegree ≤ V.characterValueCount

The denominator has degree at most the number of character values.

theorem FDRep.characterValues_eq_image_toConjClasses {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [DecidableEq k] (V : FDRep k G) [Fintype (ConjClasses G)] : V.characterValues = Finset.image (TauCeti.ClassFunction.toConjClasses (TauCeti.ClassFunction.ofFDRep V)) Finset.univ

Character values may equally be enumerated over conjugacy classes.

theorem FDRep.characterValueCount_le_card_conjClasses {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] (V : FDRep k G) : V.characterValueCount ≤ Nat.card (ConjClasses G)

The number of character values is at most the number of conjugacy classes.

noncomputable def FDRep.tensorMultiplicitySeries {k : Type u} {G : Type v} [Field k] [Monoid G] (V X : FDRep k G) : PowerSeries k

The generating series ∑ₙ dim Hom_G(X, V^⊗n) zⁿ of the multiplicities of X in the tensor powers of V, with the dimensions read in k.

@[simp]

theorem FDRep.coeff_tensorMultiplicitySeries {k : Type u} {G : Type v} [Field k] [Monoid G] (V X : FDRep k G) (n : ℕ) : (PowerSeries.coeff n) (V.tensorMultiplicitySeries X) = ↑(Module.finrank k (X ⟶ V.tensorPower n))

theorem FDRep.tensorMultiplicitySeries_congr {k : Type u} {G : Type v} [Field k] [Monoid G] {V V' X X' : FDRep k G} (e : V ≅ V') (f : X ≅ X') : V.tensorMultiplicitySeries X = V'.tensorMultiplicitySeries X'

The tensor-multiplicity series depends on V and X only up to isomorphism.

noncomputable def FDRep.tensorMultiplicityNumerator {k : Type u} {G : Type v} [Field k] [Group G] [Fintype G] (V X : FDRep k G) : Polynomial k

The numerator N_X(z) = |G|⁻¹ ∑_g χ_X(g⁻¹) ∏_{a ≠ χ_V(g)} (1 - a z) of the tensor-multiplicity series, the products running over the distinct character values of V.

theorem FDRep.tensorMultiplicityNumerator_def {k : Type u} {G : Type v} [Field k] [Group G] [Fintype G] [DecidableEq k] (V X : FDRep k G) : V.tensorMultiplicityNumerator X = Polynomial.C (↑(Nat.card G))⁻¹ * ∑ g : G, Polynomial.C (X.character g⁻¹) * ∏ a ∈ V.characterValues.erase (V.character g), (1 - Polynomial.C a * Polynomial.X)

theorem FDRep.natDegree_tensorMultiplicityNumerator_lt {k : Type u} {G : Type v} [Field k] [Group G] [Fintype G] (V X : FDRep k G) : (V.tensorMultiplicityNumerator X).natDegree < V.characterValueCount

The numerator has degree less than the number of character values.

theorem FDRep.sum_coeff_mul_finrank_hom_tensorPower_add {k : Type u} {G : Type v} [Field k] [Group G] [Fintype G] [Invertible ↑(Nat.card G)] (V X : FDRep k G) (P : Polynomial k) (n : ℕ) : ∑ j ∈ Finset.range (P.natDegree + 1), P.coeff j * ↑(Module.finrank k (X ⟶ V.tensorPower (n + j))) = (↑(Nat.card G))⁻¹ * ∑ g : G, V.character g ^ n * Polynomial.eval (V.character g) P * X.character g⁻¹

Coefficient–pairing interchange. Pairing χ_Vⁿ · P(χ_V) against χ_X computes the combination ∑ⱼ P.coeff j · dim Hom_G(X, V^⊗(n + j)) of tensor multiplicities, for every polynomial P.

theorem FDRep.tensorMultiplicitySeries_eq_characterFractions {k : Type u} {G : Type v} [Field k] [Group G] [Fintype G] [Invertible ↑(Nat.card G)] (V X : FDRep k G) : V.tensorMultiplicitySeries X = PowerSeries.C (↑(Nat.card G))⁻¹ * ∑ g : G, PowerSeries.C (X.character g⁻¹) * (1 - PowerSeries.C (V.character g) * PowerSeries.X)⁻¹

The character-fraction identity. The tensor-multiplicity series is |G|⁻¹ ∑_g χ_X(g⁻¹) (1 - χ_V(g) z)⁻¹, each factor inverted as a formal power series with constant coefficient one; the n-th coefficient is |G|⁻¹ ∑_g χ_V(g)ⁿ χ_X(g⁻¹), with χ_V(g)⁰ = 1 also when χ_V(g) = 0.

theorem FDRep.tensorMultiplicityDenominator_mul_tensorMultiplicitySeries {k : Type u} {G : Type v} [Field k] [Group G] [Fintype G] [Invertible ↑(Nat.card G)] (V X : FDRep k G) : ↑V.tensorMultiplicityDenominator * V.tensorMultiplicitySeries X = ↑(V.tensorMultiplicityNumerator X)

Rationality of the tensor-multiplicity series. Q(z) F_X(z) = N_X(z).

theorem FDRep.sum_coeff_nodal_mul_finrank_hom_tensorPower_add_eq_zero {k : Type u} {G : Type v} [Field k] [Group G] [Finite G] [Invertible ↑(Nat.card G)] (V X : FDRep k G) (n : ℕ) : ∑ j ∈ Finset.range (V.characterValueCount + 1), (Lagrange.nodal V.characterValues id).coeff j * ↑(Module.finrank k (X ⟶ V.tensorPower (n + j))) = 0

The linear recurrence of tensor multiplicities. If ∏_a (T - a) = ∑ⱼ cⱼ Tʲ, the product running over the distinct character values of V, then ∑ⱼ cⱼ m_{n+j} = 0 for every n, where mₙ = dim Hom_G(X, V^⊗n).

theorem FDRep.eval_characterInterpolator_of_injective {G : Type v} [Group G] [Finite G] [DecidableEq G] (V : FDRep ℂ G) (hV : Function.Injective ⇑V.ρ) (g : G) : Polynomial.eval (V.character g) V.characterInterpolator = if g = 1 then 1 else 0

For a faithful complex representation the interpolator is the indicator of the identity.

theorem FDRep.exists_pos_finrank_hom_tensorPower {G : Type v} [Group G] [Finite G] (V X : FDRep ℂ G) (hV : Function.Injective ⇑V.ρ) (hX : 0 < Module.finrank ℂ ↑X.V) : ∃ n < V.characterValueCount, 0 < Module.finrank ℂ (X ⟶ V.tensorPower n)

Burnside–Brauer faithful tensor generation. Every nonzero finite-dimensional complex representation has a nonzero map into a tensor power of a faithful representation, with exponent strictly smaller than the number of its distinct character values. In particular every irreducible occurs among these tensor powers.

theorem FDRep.exists_pos_finrank_hom_tensorPower_lt_card_conjClasses {G : Type v} [Group G] [Finite G] (V X : FDRep ℂ G) (hV : Function.Injective ⇑V.ρ) (hX : 0 < Module.finrank ℂ ↑X.V) : ∃ n < Nat.card (ConjClasses G), 0 < Module.finrank ℂ (X ⟶ V.tensorPower n)

Burnside–Brauer, conjugacy-class bound. Every nonzero finite-dimensional complex representation has a nonzero map into a tensor power of a faithful representation, with exponent strictly smaller than the number of conjugacy classes.

theorem FDRep.exists_mono_tensorPower {G : Type v} [Group G] [Finite G] (V X : FDRep ℂ G) [CategoryTheory.Simple X] (hV : Function.Injective ⇑V.ρ) : ∃ n < V.characterValueCount, ∃ (f : X ⟶ V.tensorPower n), CategoryTheory.Mono f

Every irreducible complex representation embeds into one of the first tensor powers of a faithful representation.

theorem FDRep.exists_mem_Ico_pos_finrank_hom_tensorPower {G : Type v} [Group G] [Finite G] (V X : FDRep ℂ G) (hV : Function.Injective ⇑V.ρ) (hd : 0 < Module.finrank ℂ ↑V.V) (hX : 0 < Module.finrank ℂ ↑X.V) (B : ℕ) : ∃ n ∈ Set.Ico B (B + V.characterValueCount), 0 < Module.finrank ℂ (X ⟶ V.tensorPower n)

Tensor generation in every window. For a faithful complex representation V of positive dimension, every nonzero X has a nonzero map into V^⊗n for some n in each window [B, B + r) of r consecutive exponents, where r is the number of character values of V.

theorem FDRep.exists_positive_tensorPower_le_valueCount {G : Type v} [Group G] [Finite G] (V X : FDRep ℂ G) (hV : Function.Injective ⇑V.ρ) (hd : 0 < Module.finrank ℂ ↑V.V) (hX : 0 < Module.finrank ℂ ↑X.V) : ∃ (n : ℕ), 0 < n ∧ n ≤ V.characterValueCount ∧ 0 < Module.finrank ℂ (X ⟶ V.tensorPower n)

The sharp positive-power bound. For a faithful complex representation V of positive dimension, every nonzero X has a nonzero map into some positive tensor power V^⊗n with n at most the number of character values of V. Positivity of dim V is necessary: the zero representation of the trivial group is faithful, and all its positive tensor powers vanish.

theorem FDRep.arbitrarily_large_tensorPowers {G : Type v} [Group G] [Finite G] (V X : FDRep ℂ G) (hV : Function.Injective ⇑V.ρ) (hd : 0 < Module.finrank ℂ ↑V.V) (hX : 0 < Module.finrank ℂ ↑X.V) (B : ℕ) : ∃ (n : ℕ), B ≤ n ∧ 0 < Module.finrank ℂ (X ⟶ V.tensorPower n)

Arbitrarily large tensor powers. For a faithful complex representation V of positive dimension, every nonzero X has nonzero maps into arbitrarily large tensor powers of V, so the tensor-multiplicity series of X has infinitely many nonzero coefficients.