Searching for modular central-character rows

The Dixon--Schneider algorithm applies simultaneous left-eigenvector search to the class- multiplication matrices. This file makes that specialization executable for TauCeti.ClassData: TauCeti.ClassData.centralCharacterSearch searches the transposed numbered class matrices, and hence returns eigenvalue tuples rather than arbitrarily scaled eigenvectors.

The main correctness theorem, TauCeti.ClassData.mem_centralCharacterSearch, identifies the output exactly with normalized common eigenrows. The normalization is not imposed by an extra filter. Multiplication by the identity class forces its eigenvalue to be 1, and evaluating the other eigenvector equations in the identity coordinate shows that every returned eigenvalue tuple is the unique normalization of its common eigenvector.

This is the bridge between the generic finite-field search in TauCeti.LinearAlgebra.Matrix.JointEigenvalueSearch and the reduced central-character table in the Dixon--Schneider pipeline. Nothing here counts the output. Under a general splitting hypothesis the count is TauCeti.ClassData.card_centralCharacterSearch; its good-prime specialization is TauCeti.ClassData.card_centralCharacterSearch_of_isGoodDixonPrime.

Main definitions

• TauCeti.ClassData.modularClassMatrix: a numbered integral class matrix reduced into a field.
• TauCeti.ClassData.IsModularEigenrow: the numbered common-eigenrow condition.
• TauCeti.ClassData.reindexModularRow: transport from numbered rows to conjugacy-class rows, bundled on the normalized eigenrows as TauCeti.ClassData.modularEigenrowEquiv.
• TauCeti.ClassData.centralCharacterSearch: the executable simultaneous eigenvalue search.

Main results

• TauCeti.ClassData.modularClassMatrix_eq_submatrix: the numbered modular matrices are a renumbering of the class-indexed ones, so their theory transports.
• TauCeti.ClassData.IsModularEigenrow.map: ring homomorphisms preserve modular eigenrows.
• TauCeti.ClassData.modularClassMatrix_index_one: the identity-class matrix is the identity.
• TauCeti.ClassData.vecMul_modularClassMatrix_apply_index_one: the identity coordinate of v ᵥ* Mᵢ is v i.
• TauCeti.ClassData.mem_centralCharacterSearch: search membership is exactly the normalized common-eigenrow condition.
• TauCeti.ClassData.mem_centralCharacterSearch_iff_exists_algHom: a searched tuple is exactly the row of an algebra homomorphism out of the modular centre.

References

This advances Layer 6, "The eigenvector search", of the character theory roadmap.

• J. D. Dixon, High speed computation of group characters, Numerische Mathematik 10 (1967), 446--450.
• G. Schneider, Dixon's character table algorithm revisited, J. Symbolic Comput. 9 (1990), 601--606.

def TauCeti.ClassData.modularClassMatrix {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (d : ClassData G) {F : Type u_2} [CommRing F] (i : Fin d.numClasses) : Matrix (Fin d.numClasses) (Fin d.numClasses) F

The i-th numbered class-multiplication matrix, reduced from ℤ into F.

Equations

• d.modularClassMatrix i = (d.classMultMatrix i).map Int.cast

@[simp]

theorem TauCeti.ClassData.modularClassMatrix_apply {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (d : ClassData G) {F : Type u_2} [CommRing F] (i j k : Fin d.numClasses) : d.modularClassMatrix i j k = ↑(d.structureConstant i k j)

theorem TauCeti.ClassData.modularClassMatrix_eq_submatrix {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (d : ClassData G) {F : Type u_2} [CommRing F] (i : Fin d.numClasses) : d.modularClassMatrix i = ((TauCeti.classMultMatrix (d.classOf i)).map Int.cast).submatrix ⇑d.equivConjClasses ⇑d.equivConjClasses

The numbered modular class matrix is a renumbering of the class-indexed one. This is TauCeti.ClassData.classMultMatrix_eq_submatrix pushed through the reduction map, and is what transports the class-indexed matrix API to the numbered family.

def TauCeti.ClassData.IsModularEigenrow {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (d : ClassData G) {F : Type u_2} [CommRing F] (v : Fin d.numClasses → F) : Prop

A numbered row is a common left eigenrow when its eigenvalue for the i-th class matrix is its own i-th entry.

Equations

• d.IsModularEigenrow v = ∀ (i : Fin d.numClasses), Matrix.vecMul v (d.modularClassMatrix i) = v i • v

theorem TauCeti.ClassData.isModularEigenrow_def {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (d : ClassData G) {F : Type u_2} [CommRing F] (v : Fin d.numClasses → F) : d.IsModularEigenrow v ↔ ∀ (i : Fin d.numClasses), Matrix.vecMul v (d.modularClassMatrix i) = v i • v

TauCeti.ClassData.IsModularEigenrow restated in its defining vector form, for consumers that want the literal eigenvector equation without unfolding the definition.

def TauCeti.ClassData.reindexModularRow {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (d : ClassData G) {F : Type u_2} (v : Fin d.numClasses → F) : ConjClasses G → F

Transport a numbered row along the numbering equivalence to a row indexed by conjugacy classes.

Equations

• d.reindexModularRow v = v ∘ ⇑d.equivConjClasses.symm

@[simp]

theorem TauCeti.ClassData.reindexModularRow_classOf {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (d : ClassData G) {F : Type u_2} (v : Fin d.numClasses → F) (i : Fin d.numClasses) : d.reindexModularRow v (d.classOf i) = v i

theorem TauCeti.ClassData.isModularEigenrow_iff {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (d : ClassData G) {F : Type u_2} [CommRing F] (v : Fin d.numClasses → F) : d.IsModularEigenrow v ↔ ∀ (i j : Fin d.numClasses), ∑ k : Fin d.numClasses, ↑(d.structureConstant i j k) * v k = v i * v j

The numbered eigenrow condition in scalar structure-constant form.

theorem TauCeti.ClassData.IsModularEigenrow.map {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] {F : Type u_2} [CommRing F] {d : ClassData G} {S : Type u_3} [CommRing S] {v : Fin d.numClasses → F} (h : d.IsModularEigenrow v) (f : F →+* S) : d.IsModularEigenrow fun (j : Fin d.numClasses) => f (v j)

A common eigenrow remains a common eigenrow after applying a ring homomorphism entrywise.

theorem TauCeti.ClassData.isModularEigenrow_iff_isClassEigenrow {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (d : ClassData G) {F : Type u_2} [CommRing F] (v : Fin d.numClasses → F) : d.IsModularEigenrow v ↔ IsClassEigenrow (d.reindexModularRow v)

Renumbering identifies the executable numbered eigenrow condition with the class-indexed TauCeti.IsClassEigenrow predicate used by the class-algebra API.

def TauCeti.ClassData.modularEigenrowEquiv {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (d : ClassData G) {F : Type u_2} [CommRing F] : { a : Fin d.numClasses → F // a (d.index 1) = 1 ∧ d.IsModularEigenrow a } ≃ { v : ConjClasses G → F // v (ConjClasses.mk 1) = 1 ∧ IsClassEigenrow v }

Renumbering matches the normalized numbered eigenrows with the normalized class-indexed ones, bundling TauCeti.ClassData.reindexModularRow and TauCeti.ClassData.isModularEigenrow_iff_isClassEigenrow as an equivalence. It is what carries a count of the class-indexed eigenrows over to the output of the executable search.

Equations

• d.modularEigenrowEquiv = (d.equivConjClasses.arrowCongr (Equiv.refl F)).subtypeEquiv ⋯

@[simp]

theorem TauCeti.ClassData.coe_modularEigenrowEquiv {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (d : ClassData G) {F : Type u_2} [CommRing F] (a : { a : Fin d.numClasses → F // a (d.index 1) = 1 ∧ d.IsModularEigenrow a }) : ↑(d.modularEigenrowEquiv a) = d.reindexModularRow ↑a

@[simp]

theorem TauCeti.ClassData.modularEigenrowEquiv_symm_apply {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (d : ClassData G) {F : Type u_2} [CommRing F] (v : { v : ConjClasses G → F // v (ConjClasses.mk 1) = 1 ∧ IsClassEigenrow v }) (i : Fin d.numClasses) : ↑(d.modularEigenrowEquiv.symm v) i = ↑v (d.classOf i)

Applying the inverse renumbering equivalence at a numbered class recovers the corresponding class-indexed entry.

@[simp]

theorem TauCeti.ClassData.modularClassMatrix_index_one {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (d : ClassData G) {F : Type u_2} [CommRing F] : d.modularClassMatrix (d.index 1) = 1

The numbered modular class matrix belonging to the identity conjugacy class is the identity matrix. This is TauCeti.classMultMatrix_mk_one, renumbered.

theorem TauCeti.ClassData.vecMul_modularClassMatrix_apply_index_one {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (d : ClassData G) {F : Type u_2} [CommRing F] (v : Fin d.numClasses → F) (i : Fin d.numClasses) : Matrix.vecMul v (d.modularClassMatrix i) (d.index 1) = v i

The identity coordinate of v ᵥ* Mᵢ is v i. This coordinate is what turns the eigenvalues found by simultaneous search into a canonically normalized eigenrow. It is TauCeti.vecMul_classMultMatrix_apply at the class of 1, renumbered.

def TauCeti.ClassData.centralCharacterSearch {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (d : ClassData G) {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] : Finset (Fin d.numClasses → F)

Search for the simultaneous left-eigenvalue tuples of the numbered modular class matrices.

The generic search is a column-eigenvector search, so the family is transposed here. The output is a Finset, making this definition directly executable for ZMod p and other finite fields.

Equations

• d.centralCharacterSearch = TauCeti.jointEigenvalueSearch fun (i : Fin d.numClasses) => (d.modularClassMatrix i).transpose

theorem TauCeti.ClassData.apply_index_one_eq_one_of_mem_centralCharacterSearch {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (d : ClassData G) {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] {a : Fin d.numClasses → F} (ha : a ∈ d.centralCharacterSearch) : a (d.index 1) = 1

A tuple returned by TauCeti.ClassData.centralCharacterSearch is normalized at the identity class.

theorem TauCeti.ClassData.isModularEigenrow_of_mem_centralCharacterSearch {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (d : ClassData G) {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] {a : Fin d.numClasses → F} (ha : a ∈ d.centralCharacterSearch) : d.IsModularEigenrow a

Every tuple returned by the search satisfies the numbered common-eigenrow equations.

@[simp]

theorem TauCeti.ClassData.mem_centralCharacterSearch {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (d : ClassData G) {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] {a : Fin d.numClasses → F} : a ∈ d.centralCharacterSearch ↔ a (d.index 1) = 1 ∧ d.IsModularEigenrow a

Correctness of the modular central-character search. A tuple occurs exactly when it is a normalized common left eigenrow of the numbered class-multiplication matrices.

The forward implication is the normalization argument: any nonzero common eigenvector has a nonzero identity coordinate, and division by that coordinate gives the eigenvalue tuple. The reverse implication feeds the row itself to the generic common-eigenvector search.

theorem TauCeti.ClassData.mem_centralCharacterSearch_iff_exists_algHom {G : Type u_1} [Group G] [Fintype G] [DecidableEq G] (d : ClassData G) {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] {a : Fin d.numClasses → F} : a ∈ d.centralCharacterSearch ↔ ∃ (φ : ↥(Subalgebra.center F (MonoidAlgebra F G)) →ₐ[F] F), ∀ (i : Fin d.numClasses), φ (classSumCenter (d.classOf i)) = a i

The searched rows are exactly the modular central characters. Membership in the executable search is equivalent to being the values on numbered class sums of an algebra homomorphism from the centre of F[G] to F.

This statement does not require the good-prime hypothesis. The exact count under a general splitting hypothesis is TauCeti.ClassData.card_centralCharacterSearch; at a good Dixon prime it is TauCeti.ClassData.card_centralCharacterSearch_of_isGoodDixonPrime.