An exact checker for integer-valued character tables

The rational stage of the Dixon--Schneider algorithm produces integer central-character and ordinary character tables. This file specializes the coefficient-independent exact certificate from TauCeti.RepresentationTheory.CharacterTable.Dixon.ExactChecker to ℤ, where star is the identity, and preserves the integer-stage API used by the rational solver.

Main definitions

• TauCeti.ClassData.IsIntegerCharacterTableSpec: the exact numbered certificate over ℤ.
• TauCeti.ClassData.integerCharacterTableChecker: its executable Boolean checker.
• TauCeti.ClassData.complexTableOfInteger: cast and reindex an integer table into the type expected by TauCeti.IsCharacterTableSpec.

Main result

• TauCeti.ClassData.IsIntegerCharacterTableSpec.isCharacterTableSpec: a successful integer certificate yields the complex character-table specification.

@[reducible, inline]

abbrev TauCeti.ClassData.IsIntegerCharacterTableSpec {G : Type u} [Group G] [Fintype G] [DecidableEq G] (d : ClassData G) (omega table : Matrix (Fin d.numClasses) (Fin d.numClasses) ℤ) (degree : Fin d.numClasses → ℕ) : Prop

An exact character-table certificate specialized to integer entries.

Equations

• d.IsIntegerCharacterTableSpec omega table degree = d.IsExactCharacterTableSpec (fun (x : ℤ) => x) omega table degree

def TauCeti.ClassData.integerCharacterTableChecker {G : Type u} [Group G] [Fintype G] [DecidableEq G] (d : ClassData G) (omega table : Matrix (Fin d.numClasses) (Fin d.numClasses) ℤ) (degree : Fin d.numClasses → ℕ) : Bool

The executable Boolean checker for an integer central-character table, ordinary table, and their character degrees.

Equations

• d.integerCharacterTableChecker omega table degree = d.exactCharacterTableChecker (fun (x : ℤ) => x) omega table degree

@[simp]

theorem TauCeti.ClassData.integerCharacterTableChecker_eq_true_iff {G : Type u} [Group G] [Fintype G] [DecidableEq G] (d : ClassData G) (omega table : Matrix (Fin d.numClasses) (Fin d.numClasses) ℤ) (degree : Fin d.numClasses → ℕ) : d.integerCharacterTableChecker omega table degree = true ↔ d.IsIntegerCharacterTableSpec omega table degree

The Boolean integer checker succeeds precisely when the integer certificate holds.

noncomputable def TauCeti.ClassData.complexTableOfInteger {G : Type u} [Group G] [Fintype G] [DecidableEq G] (d : ClassData G) (table : Matrix (Fin d.numClasses) (Fin d.numClasses) ℤ) : Matrix (Fin (Nat.card (ConjClasses G))) (ConjClasses G) ℂ

Cast a numbered integer table to ℂ, reindexing its rows by the cardinality of the conjugacy classes and its columns by the conjugacy classes themselves.

Equations

• d.complexTableOfInteger table = d.reindexTableOfMap (⇑(Int.castRingHom ℂ)) table

@[simp]

theorem TauCeti.ClassData.complexTableOfInteger_apply {G : Type u} [Group G] [Fintype G] [DecidableEq G] (d : ClassData G) (table : Matrix (Fin d.numClasses) (Fin d.numClasses) ℤ) (i : Fin (Nat.card (ConjClasses G))) (C : ConjClasses G) : d.complexTableOfInteger table i C = ↑(table ((finCongr ⋯).symm i) (d.equivConjClasses.symm C))

The cast-and-reindexed integer table evaluated at arbitrary row and column indices.

theorem TauCeti.ClassData.complexTableOfInteger_apply_classOf {G : Type u} [Group G] [Fintype G] [DecidableEq G] (d : ClassData G) (table : Matrix (Fin d.numClasses) (Fin d.numClasses) ℤ) (i j : Fin d.numClasses) : d.complexTableOfInteger table ((finCongr ⋯) i) (d.classOf j) = ↑(table i j)

The cast-and-reindexed integer table evaluated at a numbered row and numbered class.

theorem TauCeti.ClassData.IsIntegerCharacterTableSpec.table_index_one {G : Type u} [Group G] [Fintype G] [DecidableEq G] {d : ClassData G} {omega table : Matrix (Fin d.numClasses) (Fin d.numClasses) ℤ} {degree : Fin d.numClasses → ℕ} (h : d.IsIntegerCharacterTableSpec omega table degree) (i : Fin d.numClasses) : table i (d.index 1) = ↑(degree i)

The identity column of a certified integer table is its supplied degree vector.

theorem TauCeti.ClassData.IsIntegerCharacterTableSpec.centralCharacterRow_complexTableOfInteger {G : Type u} [Group G] [Fintype G] [DecidableEq G] {d : ClassData G} {omega table : Matrix (Fin d.numClasses) (Fin d.numClasses) ℤ} {degree : Fin d.numClasses → ℕ} (h : d.IsIntegerCharacterTableSpec omega table degree) (i : Fin (Nat.card (ConjClasses G))) : centralCharacterRow (d.complexTableOfInteger table) i = d.reindexModularRow fun (j : Fin d.numClasses) => ↑(omega ((finCongr ⋯).symm i) j)

The normalized row of the cast ordinary table is the corresponding cast central-character row, with both transported from the numbering of d to conjugacy classes.

theorem TauCeti.ClassData.IsIntegerCharacterTableSpec.isCharacterTableSpec {G : Type u} [Group G] [Fintype G] [DecidableEq G] {d : ClassData G} {omega table : Matrix (Fin d.numClasses) (Fin d.numClasses) ℤ} {degree : Fin d.numClasses → ℕ} (h : d.IsIntegerCharacterTableSpec omega table degree) : IsCharacterTableSpec G (d.complexTableOfInteger table)

A certified integer table satisfies the complex character-table specification.