Group algebra over finite groups

Stream: Is there code for X?

[Utensil Song]

I'm looking for Group algebra over finite groups in Mathlib, so far with little luck. Specifically, I need to naturally write the following in Lean:

(1) Let $G$ be a commutative finite group $\mathbb{Z}_3 =\left\langle e, f, g : e^2=fg=e,f^2=g, g^2=f \right\rangle$

(2) For $x, y, z \in \mathbb{R}$, let $A$ be the real group algebra of $\mathbb{R}\mathbb{Z}_3 = \left\langle xe + yf + zg : x, y, z \in \mathbb{R}, e, f, g \in \mathbb{Z}_3 \right\rangle$

(3) $\mathbb{R}\mathbb{Z}_3$ is isomorphic (as an algebra) to the direct sum of $\mathbb{R}$ and $\mathbb{C}$, denoted $\mathbb{R}\mathbb{Z}_3 \cong \mathbb{R} + \mathbb{C}$.

[Utensil Song]

(4) To see (3), we take $e + f + g$ as a generator for the real subalgebra $\mathbb{R}$, where $(e + f + g)/3$ acts as the real number 1, denoted $\mathbb{R} = \left\langle e + f + g : (e + f + g)/3 = 1\right\rangle$, and take $2e − f − g$ and $f − g$ as generators for $\mathbb{C}$, where $(2e − f − g)/3$ acts as the complex number 1, denoted $\mathbb{C} = \left\langle 2e − f − g, f − g : (2e − f − g)/3 = 1, \frac{f-g}{\sqrt{3}} = i\right\rangle$

[Utensil Song]

(5) Let's fast-forward to that adjoining an automorphism $f$ of order 3 to the quaternion group $\mathbb{Q}_8$, identifying $e = 1$ and $g = f^{−1}$, and adding in the new rules $if = fj, jf = fk$ , to get the binary tetrahedral group, denoted $2T = \left\langle q,qf, qg : q \in \mathbb{Q}_8 = \left\langle e, i, j, k : \dots \right\rangle, f^3=e, g=f^{-1}, if = fj, jf = fk \right\rangle$.

(6) By identifying quaternions $w := (−1 + i + j + k)/2$ with $f$ and $v := (−1 − i − j − k)/2$ with $g$ in (5), we obtain a group algebra that can be decompsed to $\mathbb{R} + \mathbb{C} + M_3(\mathbb{R}) + \mathbb{H} + M_2(\mathbb{C})$.

[Utensil Song]

Note that the above involves talking about a finite group in its generators/generating sets, then the group algebra also in generators then decompose it into subalgebras, also the ability of identifying generators, adjoining generators and adding new rules in an ad hoc way to create a new group, then obtain a group algebra. It also includes some made-up notations mimicking the set notations for this.

I can't really figure out how much of the infrastructure is available in Mathlib to support all of these, any help or pointer are greatly appreciated. :pray:

(Zulip can't send them all in one message, so I split them)

[Kevin Buzzard]

Group rings (for general groups, not just finite, and even for general monoids) are docs#MonoidAlgebra . The cyclic group of order 3 is either Multiplicative (ZMod 3) if you want a concrete type or (G : Type) [Fintype G] (h : Fintype.card G = 3) [IsCyclic G] if you want an abstract one. For (3/4) I would just write down $\R$-algebra homomorphisms in both directions and check they're inverse bijections by checking on a basis. I don't follow (5), if e=1 then the group law is multiplication so g=f-1 is nonsense (it's meaningless in G and false in k[G]). What group are you attempting to define here? Q_8 x C_3 or something else?

[Utensil Song]

Thanks for the hint on docs#MonoidAlgebra , I might have become trusting the result of moogle too much and didn't resort to plain mathlib doc/src search.

[Utensil Song]

Sorry, g=f-1 is a typo and should be g=f^{-1} (fixed in the original post)

[Utensil Song]

The emphasis is that I wish to be able to talk about them with explicit generating sets, and only choosing the Z3/Q8/2T groups to demonstrate the usefulness of doing so in informal math.

[Utensil Song]

What group are you attempting to define here? Q_8 x C_3 or something else?

Yes, IIUC, $2\mathrm {T} =\mathrm {Q}_8 \rtimes \mathrm {C} _{3}$.

[Utensil Song]

docs#DihedralGroup and docs#QuaternionGroup taught me that if I want to talk about generators I should use inductive types, but this way is less free when making connections between groups, particularly when following reasoning like in the original post which is a slightly rewritten excerpt from a paper discussing 2T group algebra and the relation with simpler groups.

[Utensil Song]

For (3/4) I would just write down R-algebra homomorphisms in both directions and check they're inverse bijections by checking on a basis.

Yes, this is something I imagine mathlib would do, but for something like $\mathbb{R} + \mathbb{C} + M_3(\mathbb{R}) + \mathbb{H} + M_2(\mathbb{C})$ it becomes verbose and scattered quickly. I wish to write that it decompoese to that in one go, then proving all the homomorphisms by identifying the generators and leaving the rest to automatic machinery. I don't know if there is anything like these, maybe for other areas, in mathlib?

[Kevin Buzzard]

If $G$ is a finite group then working out the group algebra $\mathbb{C}[G]$ is equivalent to working out the representation theory of $G$ (this is doable), and working out $\mathbb{R}[G]$ is equivalent to working out the representation theory of $G$ and also a bunch of Schur indices or whatever they're called. This would involve developing a bunch of theory which AFAIK isn't there yet (but which wouldn't be too hard to do in this case, there are tricks which work over the reals). You could then do $\R[Q_8\times C_3]=\R[C_3][Q_8]=(\R\oplus\mathbb{C})[Q_8]=\mathbb{C}[Q_8]\oplus\R[Q_8].$ But I suspect that whatever way you choose you'll be forced to do some pretty messy calculations.

[Utensil Song]

Indeed, these are very helpful clues (that I can work out slowly), this way also feels natural to me. Maybe I don't really need to talk about generators in this case.