Common eigenrows of the class-multiplication matrices #
For a finite group G the class sums K_C are a k-basis of the centre Z(k[G])
(TauCeti.classSumBasis), and the class-multiplication matrices Mᵢ
(TauCeti.classMultMatrix) record multiplication by K_{Cᵢ} in that basis. This file identifies
the normalized common left eigenvectors of the family {Mᵢ} — those taking the value 1 at
the class of 1 — in the row/ᵥ* convention pinned by TauCeti.classMultMatrix, with the
k-algebra homomorphisms out of the centre.
Everything rests on the coordinate identity K_{Cᵢ} K_{Cⱼ} = ∑ₖ aᵢⱼₖ K_{Cₖ} inside the centre,
which is TauCeti.classSumCenter_mul.
TauCeti.IsClassEigenrow vsaysv ᵥ* Mᵢ = v Cᵢ • vfor every classCᵢ(TauCeti.isClassEigenrow_def), andTauCeti.isClassEigenrow_iffunwinds it to the scalar identity∑ₖ aᵢⱼₖ v Cₖ = v Cᵢ * v Cⱼ.TauCeti.isClassEigenrow_of_forall_exists_smul: for a normalizedvthe eigenvalues need not be guessed — being a common left eigenvector at all forces them to be the values ofv.TauCeti.isClassEigenrow_classSumRow: the values of an algebra homomorphismφ : Z(k[G]) →ₐ[k] kon the class sums form such an eigenrow.TauCeti.eigenrowAlgHom: conversely, a common left eigenrowvnormalized byv (ConjClasses.mk 1) = 1extends from the class-sum basis to an algebra homomorphism.TauCeti.isClassEigenrow_iff_exists_algHomandTauCeti.algHomEquivEigenrowpackage the two directions as an equivalence betweenZ(k[G]) →ₐ[k] kand the normalized common left eigenrows.TauCeti.card_normalized_isClassEigenrow_of_nonempty_center_algEquiv: once the centre is split into coordinates, there are exactly as many normalized common left eigenrows as conjugacy classes, because the algebra homomorphisms out of a finite power ofkare its coordinate evaluations (Pi.evalAlgHomEquiv).
The normalization cannot be dropped: TauCeti.isClassEigenrow_zero shows 0 is an eigenrow, while
TauCeti.classSumRow_mk_one shows every row of an algebra homomorphism is normalized. Over a ring
without zero divisors it never has to be checked for a row that is not identically zero:
TauCeti.IsClassEigenrow.mk_one_eq_one shows that under NoZeroDivisors k every nonzero eigenrow
already satisfies v (ConjClasses.mk 1) = 1.
Nothing here uses representation theory: the statement is about the class algebra alone, so it holds
over any commutative ring k. In the Burnside--Dixon--Schneider algorithm it is the step that turns
a computed common eigenrow of the (integer, hence reducible mod p) matrices Mᵢ back into a
central character; that identification of the algebra homomorphisms with the central characters of
the irreducible representations is a separate statement, belonging to the layer that constructs
central characters.
References #
This is the milestone normalized_eigenrow_iff_algHom of Layer 5 of the
character theory roadmap
and its
suggested declarations,
stated over a general commutative ring and with the algebra homomorphism produced as a def.
The row of values of an algebra homomorphism out of the centre of k[G] on the class sums.
Equations
- TauCeti.classSumRow φ C = φ (TauCeti.classSumCenter C)
Instances For
The class sum of the class of 1 is the unit of the centre, so every algebra homomorphism
takes the value 1 there: the row of an algebra homomorphism is normalized.
An algebra homomorphism out of the centre of k[G] is determined by its values on the class
sums, because those are a basis.
A function on the conjugacy classes of G is a common left eigenrow of the
class-multiplication matrices when, for every class Cᵢ, it is a left eigenvector of
classMultMatrix Cᵢ with eigenvalue its own value at Cᵢ.
The row/ᵥ* orientation is the one pinned by TauCeti.classMultMatrix; the transposed matrix would
be needed for the column/*ᵥ convention.
Equations
- TauCeti.IsClassEigenrow v = ∀ (Cᵢ : ConjClasses G), Matrix.vecMul v ((TauCeti.classMultMatrix Cᵢ).map Int.cast) = v Cᵢ • v
Instances For
TauCeti.IsClassEigenrow restated in its defining vector form, for consumers that want the
literal eigenvector equation without unfolding the definition.
Acting with a class-multiplication matrix on a row vector from the left contracts the row against the structure constants.
The eigenrow condition, unwound into the scalar identity
∑ₖ aᵢⱼₖ v Cₖ = v Cᵢ * v Cⱼ on the structure constants.
The zero row is a common left eigenrow. This is why the correspondence with algebra
homomorphisms needs the normalization v (ConjClasses.mk 1) = 1.
The value of a common left eigenrow at the class of 1 acts as an identity on the row: the
class-multiplication matrix at the class of 1 is the identity matrix.
Over a ring without zero divisors, a nonzero common left eigenrow is automatically
normalized: its value at the class of 1 is 1.
The eigenvalue of a normalized common left eigenvector is forced. If v takes the value 1
at the class of 1 and v ᵥ* Mᵢ = c • v for some scalar c, then c = v Cᵢ: evaluating at the
class of 1 reads the eigenvalue off the row.
A normalized common left eigenvector of the class-multiplication matrices is an eigenrow. Only the existence of some eigenvalue for each matrix has to be checked; the normalization forces it to be the row's own value.
The values of an algebra homomorphism on the class sums form a common left eigenrow. This
is the coordinate identity TauCeti.classSumCenter_mul pushed through φ.
The algebra homomorphism attached to a normalized common left eigenrow: the linear extension
of v along the class-sum basis. Multiplicativity is the eigenrow condition read through the
coordinate identity, and it is unital because the class sum at the class of 1 is 1.
Equations
- TauCeti.eigenrowAlgHom hv₁ hv = AlgHom.ofLinearMap ((TauCeti.classSumBasis.constr k) v) ⋯ ⋯
Instances For
Normalized common left eigenrows are exactly the class-algebra homomorphisms. A function v
on the conjugacy classes with v (ConjClasses.mk 1) = 1 is a common left eigenvector of every
class-multiplication matrix, with eigenvalue v Cᵢ at Cᵢ, if and only if it is the row of values
of a k-algebra homomorphism Z(k[G]) →ₐ[k] k on the class sums.
The algebra homomorphisms out of the centre of k[G] are the normalized common left
eigenrows of the class-multiplication matrices, bundled as an equivalence: a homomorphism goes to
its row of values on the class sums, and a row extends linearly along the class-sum basis.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A split centre has as many normalized common left eigenrows as conjugacy classes. If the
centre of k[G] is k-algebra isomorphic to the algebra of k-valued functions on the conjugacy
classes, transporting the coordinate evaluations of that product decomposition gives a
non-canonical bijection between those two types. The bijection records only their cardinalities and
does not associate a specified eigenrow to a given conjugacy class.
The hypothesis is what makes the count come out: over a field that fails to split the centre some
of the characters of Z(k[G]) take values in proper extensions of k instead, and are invisible
to a search carried out over k. It holds over an algebraically closed field in which |G| is
invertible, and — the case the Burnside--Dixon--Schneider algorithm runs in — over a finite field
K with char K ∤ |G| and g ^ |K| = g (TauCeti.nonempty_center_algEquiv_conjClasses).
A split centre has as many normalized common left eigenrows as G has conjugacy classes,
the cardinality form of TauCeti.nonempty_conjClasses_equiv_normalized_isClassEigenrow.
This is the count the Burnside--Dixon--Schneider eigenvector search needs in order to know that it
has found every central character. Over an algebraically closed field in which |G| is invertible
the same count could be derived as a special case here. The existing theorem
TauCeti.card_normalized_isClassEigenrow is retained because it is a by-product of the finer
TauCeti.finEquivEigenrow, which matches the eigenrows with the irreducible representations of
G, rather than merely counting them.