Documentation

TauCeti.RepresentationTheory.CharacterTable.FiniteField

A finite field containing the roots of unity splits the centre of the group algebra #

Let G be a finite group and K a finite field whose characteristic does not divide |G| and whose multiplicative order kills G, that is g ^ |K| = g for every g : G -- equivalently, the exponent of G divides |K| - 1, so that K already contains the roots of unity that the eigenvalues of G need. This file proves that under exactly those hypotheses the centre of K[G] is split: it is K-algebra isomorphic to a product of copies of K, one for each conjugacy class of G.

The point is that K is not algebraically closed, so nothing forces the residue fields of Z(K[G]) to be K rather than proper extensions of it -- for some coefficient fields they can be proper extensions, and splitting can fail. What rules that out is the following trace argument, which is the whole content of the file.

For any u : K[G], the trace of the matrix M of left multiplication by u in the group basis is |G| times the coefficient of u at 1 (TauCeti.trace_leftMulMatrix_monoidAlgebra), and over a finite field Matrix.trace (M ^ |K|) = (Matrix.trace M) ^ |K| (FiniteField.trace_pow_card). Since a ^ |K| = a in K, the coefficient at 1 is unchanged by raising to the |K|-th power, once |G| is invertible. Now apply this to u = y * g⁻¹ for a central y: there (y * g⁻¹) ^ |K| = y ^ |K| * g⁻¹, because y is central and g⁻¹ ^ |K| = g⁻¹, so the identity compares the coefficients of y ^ |K| and of y at each g. Hence y ^ |K| = y.

A commutative ring on which the |K|-th power map is the identity is reduced, and a finite domain on which it is the identity is K itself; so the centre, being reduced and Artinian, is the product of its residue fields, all of which are K. Counting K-dimensions against the class-sum basis identifies the number of factors with the number of conjugacy classes.

This is the good-prime structure theorem of the Burnside--Dixon--Schneider algorithm, stated for a general finite coefficient field; the specialization to ZMod p at a good Dixon prime is TauCeti/RepresentationTheory/CharacterTable/Dixon/Structure.lean.

Main results #

References #

Frobenius fixes the centre #

source
theorem TauCeti.coeff_one_pow_card {K : Type u_1} {G : Type u_2} [Field K] [Fintype K] [Group G] [Finite G] (hG : ↑(Nat.card G) ≠ 0) (u : MonoidAlgebra K G) :
(u ^ Fintype.card K).coeff 1 = u.coeff 1

Raising to the |K|-th power fixes the coefficient at the identity. Over a finite field K whose characteristic does not divide |G|, the identity coefficient of u ^ |K| is that of u, for every u in the group algebra.

This is the trace identity tr (M ^ |K|) = (tr M) ^ |K| for the left regular matrix M of u, combined with a ^ |K| = a in K.

source
theorem TauCeti.pow_card_eq_self_of_mem_center {K : Type u_1} {G : Type u_2} [Field K] [Fintype K] [Group G] [Finite G] (hG : ↑(Nat.card G) ≠ 0) (hexp : ∀ (g : G), g ^ Fintype.card K = g) {y : MonoidAlgebra K G} (hy : y ∈ Subalgebra.center K (MonoidAlgebra K G)) :
y ^ Fintype.card K = y

The centre of the group algebra is fixed by the Frobenius of K. Let K be a finite field whose characteristic does not divide |G| and whose multiplicative order kills G, that is g ^ |K| = g for every g (equivalently, the exponent of G divides |K| - 1). Then every central element y of K[G] satisfies y ^ |K| = y.

The proof tests y against the group elements: (y * g⁻¹) ^ |K| = y ^ |K| * g⁻¹ because y is central and g⁻¹ is fixed by the |K|-th power map, so TauCeti.coeff_one_pow_card applied to y * g⁻¹ compares the coefficients of y ^ |K| and y at g.

The splitting of the centre #

source
instance TauCeti.instFiniteCenterMonoidAlgebra (K : Type u_1) (G : Type u_2) [CommRing K] [Finite K] [Group G] [Finite G] :
Finite ↥(Subalgebra.center K (MonoidAlgebra K G))

The centre of a finite group algebra over a finite coefficient ring is finite: it is a finitely generated module over a finite ring, by its class-sum basis.

source
instance TauCeti.instIsArtinianRingCenterMonoidAlgebra (K : Type u_1) (G : Type u_2) [CommRing K] [Group G] [Finite G] [IsArtinianRing K] :
IsArtinianRing ↥(Subalgebra.center K (MonoidAlgebra K G))

The centre of a finite group algebra over a finite Artinian commutative ring is Artinian.

source
theorem TauCeti.center_pow_card {K : Type u_1} {G : Type u_2} [Field K] [Fintype K] [Group G] [Finite G] (hG : ↑(Nat.card G) ≠ 0) (hexp : ∀ (g : G), g ^ Fintype.card K = g) (z : ↥(Subalgebra.center K (MonoidAlgebra K G))) :
z ^ Fintype.card K = z

The |K|-th power map is the identity on the centre of K[G], in the bundled form used by the structure theorem.

source
theorem TauCeti.isReduced_center {K : Type u_1} {G : Type u_2} [Field K] [Fintype K] [Group G] [Finite G] (hG : ↑(Nat.card G) ≠ 0) (hexp : ∀ (g : G), g ^ Fintype.card K = g) :
IsReduced ↥(Subalgebra.center K (MonoidAlgebra K G))

The centre of K[G] is reduced.

source
theorem TauCeti.algebraMap_center_quotient_bijective {K : Type u_1} {G : Type u_2} [Field K] [Fintype K] [Group G] [Finite G] (hG : ↑(Nat.card G) ≠ 0) (hexp : ∀ (g : G), g ^ Fintype.card K = g) (I : MaximalSpectrum ↥(Subalgebra.center K (MonoidAlgebra K G))) :
Function.Bijective ⇑(algebraMap K (↥(Subalgebra.center K (MonoidAlgebra K G)) ⧸ I.asIdeal))

Every residue field of the centre of K[G] is K itself. This is the sense in which K splits K[G]: no residue field of Z(K[G]) is a proper extension of K.

source
noncomputable def TauCeti.centerAlgEquivPi {K : Type u_1} {G : Type u_2} [Field K] [Fintype K] [Group G] [Finite G] (hG : ↑(Nat.card G) ≠ 0) (hexp : ∀ (g : G), g ^ Fintype.card K = g) :
↥(Subalgebra.center K (MonoidAlgebra K G)) ≃ₐ[K] MaximalSpectrum ↥(Subalgebra.center K (MonoidAlgebra K G)) → K

The centre of K[G] is split. For a finite field K whose characteristic does not divide |G| and whose multiplicative order kills G, the centre of K[G] is a product of copies of K, indexed by its own maximal ideals.

The centre is reduced, hence a product of its residue fields by Artinian structure theory, and each residue field is K by TauCeti.algebraMap_center_quotient_bijective.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.centerAlgEquivPi_apply {K : Type u_1} {G : Type u_2} [Field K] [Fintype K] [Group G] [Finite G] (hG : ↑(Nat.card G) ≠ 0) (hexp : ∀ (g : G), g ^ Fintype.card K = g) (z : ↥(Subalgebra.center K (MonoidAlgebra K G))) (I : MaximalSpectrum ↥(Subalgebra.center K (MonoidAlgebra K G))) :
    (centerAlgEquivPi hG hexp) z I = (AlgEquiv.ofBijective (Algebra.ofId K (↥(Subalgebra.center K (MonoidAlgebra K G)) ⧸ I.asIdeal)) ⋯).symm ((Ideal.Quotient.mk I.asIdeal) z)

    Evaluating TauCeti.centerAlgEquivPi at a maximal ideal is the quotient map followed by the inverse equivalence from that residue field to K.

    source
    theorem TauCeti.card_maximalSpectrum_center {K : Type u_1} {G : Type u_2} [Field K] [Fintype K] [Group G] [Finite G] (hG : ↑(Nat.card G) ≠ 0) (hexp : ∀ (g : G), g ^ Fintype.card K = g) :
    Nat.card (MaximalSpectrum ↥(Subalgebra.center K (MonoidAlgebra K G))) = Nat.card (ConjClasses G)

    The number of blocks is the number of conjugacy classes. Comparing K-dimensions in TauCeti.centerAlgEquivPi with the class-sum basis of the centre.

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

    The 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.