Character Table

Results named in Tau Ceti's TauCeti.RepresentationTheory.CharacterTable modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremBurnside's `pᵃqᵇ` theorem #

a finite group of order pᵃqᵇ, for primes p and q, is solvable.

TauCeti.isSolvable_of_card_eq_prime_pow_mul_prime_pow.{u} {G : Type u} [Group G] [Finite G]
  {p q : ℕ} (hp : Nat.Prime p) (hq : Nat.Prime q) {a b : ℕ} (h : Nat.card G = p ^ a * q ^ b) :
  Group.IsSolvable G

Lean

Formalized in Tau Ceti as TauCeti.isSolvable_of_card_eq_prime_pow_mul_prime_pow.

Other forms

Burnside's pᵃqᵇ theorem, in the form the induction runs in. Formalized in Tau Ceti as TauCeti.isSolvable_of_card_dvd_prime_pow_mul_prime_pow.

TauCeti.isSolvable_of_card_dvd_prime_pow_mul_prime_pow.{u} {G : Type u} [Group G] [Finite G]
  {p q : ℕ} (hp : Nat.Prime p) (hq : Nat.Prime q) {a b : ℕ} (h : Nat.card G ∣ p ^ a * q ^ b) :
  Group.IsSolvable G

Sources

LeanTauCeti.isSolvable_of_card_eq_prime_pow_mul_prime_pow · TauCeti.isSolvable_of_card_dvd_prime_pow_mul_prime_pow

Uses 1

Proof usesBurnside's vanishing theorem

TheoremBurnside's vanishing theorem #

If the conjugacy class of g has size coprime to the degree of an irreducible complex representation ρ, then its character either vanishes at g or attains there the maximum absolute value χ(1) that any character value can have.

The average χ(g) / χ(1) is an algebraic integer (Representation.isIntegral_char_div_finrank) and χ(g) is a sum of χ(1) roots of unity, so Kronecker's theorem leaves no other possibility.

Representation.char_eq_zero_or_norm_char_eq_finrank.{u_1, u_2} {G : Type u_1} {V : Type u_2}
  [Group G] [Finite G] [AddCommGroup V] [_root_.Module ℂ V] [FiniteDimensional ℂ V]
  (ρ : Representation ℂ G V) [ρ.IsIrreducible] {g : G}
  (h : (Nat.card ↑(ConjClasses.mk g).carrier).Coprime (Module.finrank ℂ V)) :
  ρ.character g = 0 ∨ ‖ρ.character g‖ = ↑(Module.finrank ℂ V)

Lean

Formalized in Tau Ceti as Representation.char_eq_zero_or_norm_char_eq_finrank.

Other forms

Burnside's vanishing theorem, for a bundled finite-dimensional complex representation. Formalized in Tau Ceti as FDRep.char_eq_zero_or_norm_char_eq_finrank.

FDRep.char_eq_zero_or_norm_char_eq_finrank.{u_1} {G : Type u_1} [Group G] [Finite G] (X : FDRep ℂ G)
  [Representation.IsIrreducible X.ρ] {g : G}
  (h : (Nat.card ↑(ConjClasses.mk g).carrier).Coprime (Module.finrank ℂ ↑X.V)) :
  X.character g = 0 ∨ ‖X.character g‖ = ↑(Module.finrank ℂ ↑X.V)

Burnside's vanishing theorem, scalar form, for a bundled finite-dimensional complex representation. Formalized in Tau Ceti as FDRep.char_eq_zero_or_exists_apply_eq_smul.

FDRep.char_eq_zero_or_exists_apply_eq_smul.{u_1} {G : Type u_1} [Group G] [Finite G] (X : FDRep ℂ G)
  [Representation.IsIrreducible X.ρ] {g : G}
  (h : (Nat.card ↑(ConjClasses.mk g).carrier).Coprime (Module.finrank ℂ ↑X.V)) :
  X.character g = 0 ∨ ∃ μ, X.ρ g = μ • 1

Burnside's vanishing theorem, scalar form (Isaacs, Theorem 3.8). Formalized in Tau Ceti as Representation.char_eq_zero_or_exists_apply_eq_smul.

Representation.char_eq_zero_or_exists_apply_eq_smul.{u_1, u_2} {G : Type u_1} {V : Type u_2}
  [Group G] [Finite G] [AddCommGroup V] [_root_.Module ℂ V] [FiniteDimensional ℂ V]
  (ρ : Representation ℂ G V) [ρ.IsIrreducible] {g : G}
  (h : (Nat.card ↑(ConjClasses.mk g).carrier).Coprime (Module.finrank ℂ V)) :
  ρ.character g = 0 ∨ ∃ μ, ρ g = μ • 1

Sources

LeanRepresentation.char_eq_zero_or_norm_char_eq_finrank · FDRep.char_eq_zero_or_norm_char_eq_finrank · FDRep.char_eq_zero_or_exists_apply_eq_smul · Representation.char_eq_zero_or_exists_apply_eq_smul

Uses 1 · Used by 1

Proof usesSchur's lemma, vanishing form

Used byBurnside's pᵃqᵇ theorem

TheoremBurnside–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.

FDRep.exists_pos_finrank_hom_tensorPower_lt_card_conjClasses.{v} {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)

Lean

Formalized in Tau Ceti as FDRep.exists_pos_finrank_hom_tensorPower_lt_card_conjClasses.

Sources

LeanFDRep.exists_pos_finrank_hom_tensorPower_lt_card_conjClasses

TheoremDixon's size bound in the shape the residue window asks for #

An integer of absolute value at most ⌊√|G|⌋ lies strictly inside the window of half-width p / 2, since 2⌊√|G|⌋ < p.

TauCeti.IsGoodDixonPrime.two_mul_natAbs_lt_of_natAbs_le_sqrt.{u_1} {G : Type u_1} [Group G] {p : ℕ}
  (hp : TauCeti.IsGoodDixonPrime G p) {z : ℤ} (hz : z.natAbs ≤ (Nat.card G).sqrt) : 2 * z.natAbs < p

Lean

Formalized in Tau Ceti as TauCeti.IsGoodDixonPrime.two_mul_natAbs_lt_of_natAbs_le_sqrt.

Sources

LeanTauCeti.IsGoodDixonPrime.two_mul_natAbs_lt_of_natAbs_le_sqrt

TheoremThe Frobenius formula #

The number of triples (x, y, z) with x ∈ C₀, y ∈ C₁, z ∈ C∞ and z * y * x = 1 is

(|C₀| · |C₁| · |C∞| / |G|) · ∑_χ χ(C₀) χ(C₁) χ(C∞) / χ(1),

the sum running over the irreducible characters of G.

TauCeti.card_productOneTriples_eq_sum_characterTable.{u, v} {k : Type u} {G : Type v} [Field k]
  [IsAlgClosed k] [CharZero k] [Group G] [Fintype G] [DecidableEq G] [Invertible ↑(Nat.card G)]
  (C0 C1 Cinf : ConjClasses G) :
  ↑(TauCeti.productOneTriples C0 C1 Cinf).card =
    ↑(Nat.card ↑C0.carrier) * ↑(Nat.card ↑C1.carrier) * ↑(Nat.card ↑Cinf.carrier) / ↑(Nat.card G) *
      ∑ l,
        TauCeti.characterTable k G l C0 * TauCeti.characterTable k G l C1 *
            TauCeti.characterTable k G l Cinf /
          ↑(TauCeti.characterDegree k l)

Lean

Formalized in Tau Ceti as TauCeti.card_productOneTriples_eq_sum_characterTable.

Sources

LeanTauCeti.card_productOneTriples_eq_sum_characterTable

Uses 1

Proof usesSchur's lemma, vanishing form

TheoremThe Frobenius-Schur trichotomy #

The indicator of an irreducible representation over an algebraically closed field of characteristic zero takes only the values 1, 0 and -1.

TauCeti.Representation.frobeniusSchurIndicator_eq_one_or_eq_zero_or_eq_neg_one.{v, w} {k : Type}
  {G : Type v} {V : Type w} [Field k] [CharZero k] [IsAlgClosed k] [Group G] [Fintype G]
  [AddCommGroup V] [_root_.Module k V] [FiniteDimensional k V] (ρ : Representation k G V)
  [ρ.IsIrreducible] :
  TauCeti.Representation.frobeniusSchurIndicator ρ = 1 ∨
    TauCeti.Representation.frobeniusSchurIndicator ρ = 0 ∨
      TauCeti.Representation.frobeniusSchurIndicator ρ = -1

Lean

Formalized in Tau Ceti as TauCeti.Representation.frobeniusSchurIndicator_eq_one_or_eq_zero_or_eq_neg_one.

Sources

LeanTauCeti.Representation.frobeniusSchurIndicator_eq_one_or_eq_zero_or_eq_neg_one

TheoremThe good-prime structure theorem #

At a good Dixon prime the centre of ZMod p [G] is the algebra of ZMod p-valued functions on the conjugacy classes of G.

This is what guarantees that the class-multiplication matrices are simultaneously diagonalizable over ZMod p with exactly r distinct common eigenrows, so that the eigenvector search of the Burnside--Dixon--Schneider algorithm terminates in one-dimensional common eigenspaces, with no bad-prime merging of distinct central characters.

TauCeti.IsGoodDixonPrime.nonempty_center_algEquiv_conjClasses.{u_1} {G : Type u_1} [Group G] {p : ℕ}
  (hp : TauCeti.IsGoodDixonPrime G p) :
  Nonempty
    (↥(Subalgebra.center (ZMod p) (MonoidAlgebra (ZMod p) G)) ≃ₐ[ZMod p] ConjClasses G → ZMod p)

Lean

Formalized in Tau Ceti as TauCeti.IsGoodDixonPrime.nonempty_center_algEquiv_conjClasses.

Sources

LeanTauCeti.IsGoodDixonPrime.nonempty_center_algEquiv_conjClasses

Uses 1

Proof usesThe good-splitting structure theorem for a finite coefficient field

TheoremThe good-splitting structure theorem for a finite coefficient field #

The centre of K[G] is K-algebra isomorphic to the functions on the conjugacy classes of G.

The indexing is by cardinality only: the canonical indexing of the factors is by the maximal ideals of the centre (TauCeti.centerAlgEquivPi), which TauCeti.card_maximalSpectrum_center counts.

TauCeti.nonempty_center_algEquiv_conjClasses.{u_1, u_2} {K : Type u_1} {G : Type u_2} [Field K]
  [Fintype K] [Group G] [Finite G] (hexp : ∀ (g : G), g ^ Fintype.card K = g) :
  Nonempty (↥(Subalgebra.center K (MonoidAlgebra K G)) ≃ₐ[K] ConjClasses G → K)

Lean

Formalized in Tau Ceti as TauCeti.nonempty_center_algEquiv_conjClasses.

Sources

LeanTauCeti.nonempty_center_algEquiv_conjClasses

Used by 1

Used byThe good-prime structure theorem

TheoremMaschke's theorem at a good Dixon prime #

the modular group algebra ZMod p [G] is a semisimple ring.

TauCeti.IsGoodDixonPrime.isSemisimpleRing.{u_1} {G : Type u_1} [Group G] {p : ℕ}
  (hp : TauCeti.IsGoodDixonPrime G p) : IsSemisimpleRing (MonoidAlgebra (ZMod p) G)

Lean

Formalized in Tau Ceti as TauCeti.IsGoodDixonPrime.isSemisimpleRing.

Sources

LeanTauCeti.IsGoodDixonPrime.isSemisimpleRing

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

Character Table

TheoremBurnside's pᵃqᵇ theorem#

Lean

Other forms

Sources

TheoremBurnside's vanishing theorem#

Lean

Other forms

Sources

TheoremBurnside–Brauer, conjugacy-class bound#

Lean

Sources

TheoremDixon's size bound in the shape the residue window asks for#

Lean

Sources

TheoremThe Frobenius formula#

Lean

Sources

TheoremThe Frobenius-Schur trichotomy#

Lean

Sources

TheoremThe good-prime structure theorem#

Lean

Sources

TheoremThe good-splitting structure theorem for a finite coefficient field#

Lean

Sources

TheoremMaschke's theorem at a good Dixon prime#

Lean

Sources

TheoremBurnside's `pᵃqᵇ` theorem #

TheoremBurnside's vanishing theorem #

TheoremBurnside–Brauer, conjugacy-class bound #

TheoremDixon's size bound in the shape the residue window asks for #

TheoremThe Frobenius formula #

TheoremThe Frobenius-Schur trichotomy #

TheoremThe good-prime structure theorem #

TheoremThe good-splitting structure theorem for a finite coefficient field #

TheoremMaschke's theorem at a good Dixon prime #