Executable conjugacy-class data

The class-algebra theory of a finite group is indexed by ConjClasses G, a quotient type: perfect for stating theorems, useless for computing with, since nothing picks a representative of a class or orders the classes. The Burnside--Dixon--Schneider character-table algorithm needs both, because its input is the array of structure constants aᵢⱼₖ and its output is a table whose rows and columns are numbered.

This file supplies the missing numbering. A TauCeti.ClassData G is a list of elements of G, one from each conjugacy class; the two fields say that no two entries are conjugate and that every element of G is conjugate to an entry. From those two facts alone the whole indexing API follows: a representative d.rep i for each i : Fin d.numClasses, an inverse d.index g computed by a list search, and the equivalence d.equivConjClasses : Fin d.numClasses ≃ ConjClasses G that transports statements about ConjClasses G to the numbering. All of these are genuine defs: the numbering data itself asks only for [Group G], the searches computed from it for a decidable conjugacy relation, the classes as Finsets for [Fintype G], and TauCeti.ClassData.ofList builds class data from any list that meets every conjugacy class.

On top of the numbering the file gives the two computational objects the algorithm consumes: the structure constants d.structureConstant i j k, counted by a single scan of the i-th class rather than by the double scan of the definition, and the class-multiplication matrices d.classMultMatrix i over Fin d.numClasses. Both are proved equal to their ConjClasses-indexed counterparts TauCeti.structureConstant and TauCeti.classMultMatrix, so the theory built on the latter — in particular the eigenrow characterization of the central characters — applies verbatim to the computed data.

TauCeti.RepresentationTheory.CharacterTable.Dixon.ClassData.Dihedral works the dihedral group of order 8 as a closed instance of everything here.

Main definitions

• TauCeti.ClassData: a numbered list of conjugacy-class representatives of a group.
• TauCeti.ClassData.ofList: such a list, extracted from any list meeting every conjugacy class.
• TauCeti.ClassData.index, TauCeti.ClassData.rep: the numbering and its representatives.
• TauCeti.ClassData.equivConjClasses: the numbering as an equivalence with ConjClasses G.
• TauCeti.ClassData.rowsOfMap: the rows of a numbered matrix, mapped entrywise into another type.
• TauCeti.ClassData.reindexTableOfMap: map the entries of a numbered table and reindex it by the conjugacy classes.
• TauCeti.ClassData.classFinset, TauCeti.ClassData.classes: the i-th conjugacy class and the executable list of all conjugacy classes.
• TauCeti.ClassData.structureConstant, TauCeti.ClassData.structureConstantTable, TauCeti.ClassData.classMultMatrix: the single-scan structure constants, tabulated, and the matrices they assemble.

Main results

• TauCeti.ClassData.numClasses_eq_card_conjClasses: the numbering has the expected length.
• TauCeti.ClassData.exists_mem_classes, TauCeti.ClassData.pairwise_disjoint_classes: the executable list covers the group and its entries are pairwise disjoint.
• TauCeti.ClassData.sum_card_classFinset: the numbered classes partition the group.
• TauCeti.ClassData.structureConstant_eq and TauCeti.ClassData.classMultMatrix_eq_submatrix: the computed constants and matrices are the ones the theory uses, renumbered.

References

This implements the object ClassData and the executable structureConstant of Layer 6 of the character theory roadmap, the layer that makes the Burnside--Dixon--Schneider algorithm executable. The Fin-indexed family classFinset is what the class-multiplication matrices are indexed by, while classes packages the same family as the executable List (Finset G) requested there. See J. D. Dixon, High speed computation of group characters, Numer. Math. 10 (1967) 446-450.

structure TauCeti.ClassData (G : Type u_2) [Group G] : Type u_2

Executable conjugacy-class data for a group: a list reps containing exactly one element of each conjugacy class. The two fields are the two halves of "exactly one": distinct entries name distinct classes, and no class is missed. Carrying the data asks nothing of G beyond its group structure; a decidable conjugacy relation is what the searches computed from it need, and finiteness what turns the classes into Finsets.

The order of reps is the arbitrary but fixed numbering of the conjugacy classes that a computation indexes by; TauCeti.ClassData.equivConjClasses identifies it with ConjClasses G.

• reps : List G

  The chosen representatives, in the order that numbers the classes.

• pairwise_not_isConj : List.Pairwise (fun (x y : G) => ¬IsConj x y) self.reps

  Distinct representatives are not conjugate, so they name distinct classes.

• exists_isConj (g : G) : ∃ x ∈ self.reps, IsConj x g

  Every element of the group is conjugate to a representative, so no class is missed.

theorem TauCeti.ClassData.ext {G : Type u_1} [Group G] {d₁ d₂ : ClassData G} (h : d₁.reps = d₂.reps) : d₁ = d₂

Class data is determined by its representatives: the two remaining fields are proofs.

theorem TauCeti.ClassData.ext_iff {G : Type u_1} [Group G] {d₁ d₂ : ClassData G} : d₁ = d₂ ↔ d₁.reps = d₂.reps

def TauCeti.ClassData.ofList {G : Type u_1} [Group G] [DecidableRel IsConj] (l : List G) (hl : ∀ (g : G), ∃ x ∈ l, IsConj x g) : ClassData G

Class data extracted from a list l that meets every conjugacy class: keep an entry exactly when it is not conjugate to any entry kept from the part of l after it. Since List.pwFilter recurses from the right, this keeps the last representative of each class, in the order those representatives occur in l.

The hypothesis, rather than Finset.univ.toList, is what keeps this computable: Finset.toList is noncomputable, whereas a concrete finite group can supply concrete representatives.

Equations

• TauCeti.ClassData.ofList l hl = { reps := List.pwFilter (fun (x y : G) => ¬IsConj x y) l, pairwise_not_isConj := ⋯, exists_isConj := ⋯ }

@[simp]

theorem TauCeti.ClassData.reps_ofList {G : Type u_1} [Group G] [DecidableRel IsConj] (l : List G) (hl : ∀ (g : G), ∃ x ∈ l, IsConj x g) : (ofList l hl).reps = List.pwFilter (fun (x y : G) => ¬IsConj x y) l

The representatives extracted from l are the entries of l that are not conjugate to any later retained entry: the characteristic property of TauCeti.ClassData.ofList, so that a client never has to unfold the filtering itself.

@[instance_reducible]

noncomputable instance TauCeti.ClassData.instInhabitedOfFinite {G : Type u_1} [Group G] [Finite G] : Inhabited (ClassData G)

Every finite group has class data; the witness is noncomputable only because Finset.toList is.

Equations

• TauCeti.ClassData.instInhabitedOfFinite = { default := TauCeti.ClassData.ofList Finset.univ.toList ⋯ }

def TauCeti.ClassData.numClasses {G : Type u_1} [Group G] (d : ClassData G) : ℕ

The number of conjugacy classes of G, as numbered by d.

Equations

• d.numClasses = d.reps.length

def TauCeti.ClassData.rep {G : Type u_1} [Group G] (d : ClassData G) (i : Fin d.numClasses) : G

The chosen representative of the i-th conjugacy class.

Equations

• d.rep i = d.reps[↑i]

def TauCeti.ClassData.classOf {G : Type u_1} [Group G] (d : ClassData G) (i : Fin d.numClasses) : ConjClasses G

The i-th conjugacy class, as an element of ConjClasses G.

Equations

• d.classOf i = ConjClasses.mk (d.rep i)

theorem TauCeti.ClassData.classOf_eq_mk {G : Type u_1} [Group G] (d : ClassData G) (i : Fin d.numClasses) : d.classOf i = ConjClasses.mk (d.rep i)

The i-th class is the class of the i-th representative. This is not a simp lemma: it would rewrite past TauCeti.ClassData.classOf_index, which is the normal form wanted.

theorem TauCeti.ClassData.not_isConj_rep {G : Type u_1} [Group G] (d : ClassData G) {i j : Fin d.numClasses} (hij : i ≠ j) : ¬IsConj (d.rep i) (d.rep j)

Distinct numbers name distinct classes: the Fin-indexed reading of the pairwise_not_isConj field.

theorem TauCeti.ClassData.nodup_reps {G : Type u_1} [Group G] (d : ClassData G) : d.reps.Nodup

The representatives are distinct, conjugacy being reflexive.

Rows of a numbered matrix

def TauCeti.ClassData.rowsOfMap {G : Type u_1} [Group G] (d : ClassData G) {R : Type u_2} {S : Type u_3} [DecidableEq S] (f : R → S) (M : Matrix (Fin d.numClasses) (Fin d.numClasses) R) : Finset (Fin d.numClasses → S)

The rows of a numbered matrix, mapped entrywise by f and collected without an ordering.

Equations

• d.rowsOfMap f M = Finset.image (fun (i j : Fin d.numClasses) => f (M i j)) Finset.univ

@[simp]

theorem TauCeti.ClassData.mem_rowsOfMap_iff {G : Type u_1} [Group G] (d : ClassData G) {R : Type u_2} {S : Type u_3} [DecidableEq S] (f : R → S) (M : Matrix (Fin d.numClasses) (Fin d.numClasses) R) {a : Fin d.numClasses → S} : a ∈ d.rowsOfMap f M ↔ ∃ (i : Fin d.numClasses), (fun (j : Fin d.numClasses) => f (M i j)) = a

A row is displayed exactly when it is the mapped image of a matrix row.

def TauCeti.ClassData.index {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] (g : G) : Fin d.numClasses

The number of the conjugacy class of g, found by searching d.reps for a representative conjugate to g. The search succeeds because some representative is conjugate to g.

Equations

• d.index g = ⟨List.findIdx (fun (x : G) => decide (IsConj x g)) d.reps, ⋯⟩

theorem TauCeti.ClassData.isConj_rep_index {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] (g : G) : IsConj (d.rep (d.index g)) g

The representative found by TauCeti.ClassData.index is conjugate to g.

theorem TauCeti.ClassData.index_eq_iff {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] {g : G} {i : Fin d.numClasses} : d.index g = i ↔ IsConj (d.rep i) g

The numbering is characterized by conjugacy: g has number i exactly when it is conjugate to the i-th representative.

@[simp]

theorem TauCeti.ClassData.index_rep {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] (i : Fin d.numClasses) : d.index (d.rep i) = i

theorem TauCeti.ClassData.index_eq_index_iff {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] {g h : G} : d.index g = d.index h ↔ IsConj g h

Two elements get the same number exactly when they are conjugate.

@[simp]

theorem TauCeti.ClassData.classOf_index {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] (g : G) : d.classOf (d.index g) = ConjClasses.mk g

def TauCeti.ClassData.indexClass {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] (C : ConjClasses G) : Fin d.numClasses

The number of a conjugacy class: TauCeti.ClassData.index is constant on classes, so it descends to ConjClasses G.

Equations

• d.indexClass C = Quotient.liftOn C d.index ⋯

@[simp]

theorem TauCeti.ClassData.indexClass_mk {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] (g : G) : d.indexClass (ConjClasses.mk g) = d.index g

def TauCeti.ClassData.equivConjClasses {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] : Fin d.numClasses ≃ ConjClasses G

The numbering of the conjugacy classes is a bijection. The forward map sends a number to the class it names; the inverse is the computable search TauCeti.ClassData.index.

Equations

• d.equivConjClasses = { toFun := d.classOf, invFun := d.indexClass, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem TauCeti.ClassData.equivConjClasses_apply {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] (i : Fin d.numClasses) : d.equivConjClasses i = d.classOf i

@[simp]

theorem TauCeti.ClassData.equivConjClasses_symm_apply {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] (C : ConjClasses G) : d.equivConjClasses.symm C = d.indexClass C

theorem TauCeti.ClassData.numClasses_eq_card_conjClasses {G : Type u_1} [Group G] (d : ClassData G) : d.numClasses = Nat.card (ConjClasses G)

The numbering has the expected length: d.reps lists as many elements as G has conjugacy classes. The bijection is the one underlying TauCeti.ClassData.equivConjClasses, but it is exhibited here from the two fields directly, since the count itself needs neither a finite G nor a decidable conjugacy.

Reindexing numbered tables

noncomputable def TauCeti.ClassData.reindexTableOfMap {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] {R : Type u_2} {S : Type u_3} (f : R → S) (table : Matrix (Fin d.numClasses) (Fin d.numClasses) R) : Matrix (Fin (Nat.card (ConjClasses G))) (ConjClasses G) S

Map the entries of a numbered table with f, reindexing its rows by the cardinality of the conjugacy classes and its columns by the conjugacy classes themselves.

Equations

• d.reindexTableOfMap f table = (table.map f).submatrix ⇑(finCongr ⋯).symm ⇑d.equivConjClasses.symm

@[simp]

theorem TauCeti.ClassData.reindexTableOfMap_apply {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] {R : Type u_2} {S : Type u_3} (f : R → S) (table : Matrix (Fin d.numClasses) (Fin d.numClasses) R) (i : Fin (Nat.card (ConjClasses G))) (C : ConjClasses G) : d.reindexTableOfMap f table i C = f (table ((finCongr ⋯).symm i) (d.equivConjClasses.symm C))

The mapped and reindexed table, evaluated at arbitrary row and column indices.

theorem TauCeti.ClassData.reindexTableOfMap_apply_classOf {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] {R : Type u_2} {S : Type u_3} (f : R → S) (table : Matrix (Fin d.numClasses) (Fin d.numClasses) R) (i j : Fin d.numClasses) : d.reindexTableOfMap f table ((finCongr ⋯) i) (d.classOf j) = f (table i j)

The mapped and reindexed table evaluated at a numbered row and numbered class.

def TauCeti.ClassData.classFinset {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] [Fintype G] (i : Fin d.numClasses) : Finset G

The i-th conjugacy class, as a Finset of G.

Equations

• d.classFinset i = {g : G | d.index g = i}

@[simp]

theorem TauCeti.ClassData.mem_classFinset {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] [Fintype G] {i : Fin d.numClasses} {g : G} : g ∈ d.classFinset i ↔ d.index g = i

theorem TauCeti.ClassData.mem_classFinset_iff_isConj {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] [Fintype G] {i : Fin d.numClasses} {g : G} : g ∈ d.classFinset i ↔ IsConj (d.rep i) g

The i-th class consists of the elements conjugate to the i-th representative.

theorem TauCeti.ClassData.rep_mem_classFinset {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] [Fintype G] (i : Fin d.numClasses) : d.rep i ∈ d.classFinset i

The i-th representative lies in the i-th class.

theorem TauCeti.ClassData.coe_classFinset {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] [Fintype G] (i : Fin d.numClasses) : ↑(d.classFinset i) = (d.classOf i).carrier

The numbered class is the carrier of the class it names. This is the compatibility that lets the Finset be used in a computation and ConjClasses.carrier in a proof.

theorem TauCeti.ClassData.card_classFinset {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] [Fintype G] (i : Fin d.numClasses) : (d.classFinset i).card = Nat.card ↑(d.classOf i).carrier

The size of the i-th class is the size of the class it names.

theorem TauCeti.ClassData.disjoint_classFinset {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] [Fintype G] {i j : Fin d.numClasses} (hij : i ≠ j) : Disjoint (d.classFinset i) (d.classFinset j)

Distinct numbered classes are disjoint.

def TauCeti.ClassData.classes {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] [Fintype G] : List (Finset G)

The conjugacy classes, in the order determined by d.

Equations

• d.classes = List.map d.classFinset (List.finRange d.numClasses)

@[simp]

theorem TauCeti.ClassData.length_classes {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] [Fintype G] : d.classes.length = d.numClasses

There is one entry of classes for each class number.

@[simp]

theorem TauCeti.ClassData.getElem_classes {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] [Fintype G] (i : ℕ) (hi : i < d.classes.length) : d.classes[i] = d.classFinset ⟨i, ⋯⟩

Looking up the i-th entry of classes gives the i-th numbered class.

theorem TauCeti.ClassData.exists_mem_classes {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] [Fintype G] (g : G) : ∃ C ∈ d.classes, g ∈ C

The list classes covers every element of the group.

theorem TauCeti.ClassData.pairwise_disjoint_classes {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] [Fintype G] : List.Pairwise Disjoint d.classes

Distinct entries of classes are disjoint.

theorem TauCeti.ClassData.sum_card_classFinset {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] [Fintype G] : ∑ i : Fin d.numClasses, (d.classFinset i).card = Fintype.card G

The numbered classes partition the group: their sizes sum to |G|. This is the Fin-indexed reading of the class equation sum_conjClasses_card_eq_card.

def TauCeti.ClassData.structureConstant {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] [Fintype G] (i j k : Fin d.numClasses) : ℕ

The structure constant aᵢⱼₖ of the class algebra, computed by a single scan: it counts the elements x of the i-th class whose complementary factor x⁻¹ * gₖ lies in the j-th class, where gₖ is the k-th representative.

TauCeti.ClassData.structureConstant_eq identifies this with TauCeti.structureConstant, which counts the factorizations x * y = gₖ themselves.

Equations

• d.structureConstant i j k = {x ∈ d.classFinset i | d.index (x⁻¹ * d.rep k) = j}.card

def TauCeti.ClassData.classMultMatrix {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] [Fintype G] (i : Fin d.numClasses) : Matrix (Fin d.numClasses) (Fin d.numClasses) ℤ

The class-multiplication matrix Mᵢ of the i-th class, numbered by d. As in TauCeti.classMultMatrix, the entry (Mᵢ)ⱼₖ is aᵢₖⱼ; that transposed index order is what makes Mᵢ the matrix of multiplication by the i-th class sum on the centre of the group algebra, and so what makes the central-character rows left eigenvectors of the family.

Equations

• d.classMultMatrix i = Matrix.of fun (j k : Fin d.numClasses) => ↑(d.structureConstant i k j)

@[simp]

theorem TauCeti.ClassData.classMultMatrix_apply {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] [Fintype G] (i j k : Fin d.numClasses) : d.classMultMatrix i j k = ↑(d.structureConstant i k j)

def TauCeti.ClassData.structureConstantTable {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] [Fintype G] : List (List (List ℕ))

The structure constants of d, tabulated: the k-th entry of the j-th entry of the i-th entry is aᵢⱼₖ. This nested list is the whole input to the Dixon--Schneider algorithm for G, and, unlike the matrices it assembles, it can be compared with a literal by the kernel.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.ClassData.length_structureConstantTable {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] [Fintype G] : d.structureConstantTable.length = d.numClasses

@[simp]

theorem TauCeti.ClassData.getElem_structureConstantTable {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] [Fintype G] (i : ℕ) (hi : i < d.structureConstantTable.length) : d.structureConstantTable[i] = List.map (fun (j : Fin d.numClasses) => List.map (fun (k : Fin d.numClasses) => d.structureConstant ⟨i, ⋯⟩ j k) (List.finRange d.numClasses)) (List.finRange d.numClasses)

The i-th row of the table is the table of the structure constants with first index i. Together with List.getElem_map and List.getElem_finRange this reduces a lookup at any depth: in particular simp sends the depth-three entry d.structureConstantTable[i][j][k] to aᵢⱼₖ, so no separate entry lemma is needed.

theorem TauCeti.ClassData.getD_structureConstantTable {G : Type u_1} [Group G] (d : ClassData G) [DecidableRel IsConj] [Fintype G] (i j k : Fin d.numClasses) : ((d.structureConstantTable.getD ↑i []).getD ↑j []).getD (↑k) 0 = d.structureConstant i j k

Reading the tabulated structure constants at three valid indices recovers the corresponding computed structure constant. This getD form is convenient when a whole literal table is rewritten at once.

theorem TauCeti.ClassData.structureConstant_eq {G : Type u_1} [Group G] (d : ClassData G) [Fintype G] [DecidableEq G] (i j k : Fin d.numClasses) : d.structureConstant i j k = TauCeti.structureConstant (d.classOf i) (d.classOf j) (d.classOf k)

The computed structure constants are the structure constants: recording a factorization by its first factor matches the single scan with the double scan of the definition.

theorem TauCeti.ClassData.classMultMatrix_eq_submatrix {G : Type u_1} [Group G] (d : ClassData G) [Fintype G] [DecidableEq G] (i : Fin d.numClasses) : d.classMultMatrix i = (TauCeti.classMultMatrix (d.classOf i)).submatrix ⇑d.equivConjClasses ⇑d.equivConjClasses

The numbered class-multiplication matrix is a renumbering of the class-indexed one. Every statement about TauCeti.classMultMatrix therefore transports to the numbered family.

theorem TauCeti.ClassData.classMultMatrix_commute {G : Type u_1} [Group G] (d : ClassData G) [Fintype G] [DecidableEq G] (i j : Fin d.numClasses) : Commute (d.classMultMatrix i) (d.classMultMatrix j)

The numbered class-multiplication matrices commute pairwise, the centre of the group algebra being commutative.