Project Idea: Representations of Finite Group

Stream: LFTCM 2024

[Eduardo Venturini]

We want to develop the representation theory of finite groups / finite dimensional algebras.
In particular, we want to prove that

$$|G| = \sum_{\rho} n_{\rho}^2$$

where the sum is over the irreducible representations of G and n_{\rho} is the dimension of the representation.

[Eduardo Venturini]

Roadmap:

• [ ] Every finite dimensional representation is direct sum of irreducible representations (k closed field, char k not divides |G|), starting from "MonoidAlgebra.Submodule.exists_isCompl"
• [ ] Characters scalar product

Bonus:

• [ ] Find (or prove) Artin-Wedderburn

[Eduardo Venturini]

Old conversation: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Representation.20Theory

[Eduardo Venturini]

Notes: Introduction_to_representation_theory.pdf
Other notes: Linear_Representations_of_Finite_Groups-Jean_Pierre_Serre.pdf

[Eduardo Venturini]

We are in the library

[Eduardo Venturini]

Repository: https://github.com/leanprover-community/mathlib4/tree/LFTCM24-finite-group-representations

[Notification Bot]

Alessandro Iraci has marked this topic as resolved.

[Notification Bot]

Alessandro Iraci has marked this topic as unresolved.

[Notification Bot]

This topic was moved here from #LFTCM 2024 > Project Idea: Respresentations of Finite Group by Riccardo Brasca.

[Peiran Wu]

Is there a live discussion about this project right now?

[Filippo A. E. Nuccio]

Yes, in a room near the Library. Where are you?

[Amelia Livingston]

I will join you guys in about ten minutes, are you still in a room near the library?

[Alessandro Iraci]

We're right at the entrance!

[Amelia Livingston]

I've just pushed a file Mathlib.Algebra.DirectSum.SumLEquivProd full of stuff that should be moved to other files and which has an isomorphism between a direct sum indexed by a sum type & a product of direct sums, i.e.

noncomputable def sumLEquivProd
    [∀ (i : ια), AddCommMonoid (α i)] [∀ i : ιβ, AddCommMonoid (β i)]
    [∀ (i : ια), Module k (α i)] [∀ i : ιβ, Module k (β i)] :
    (⨁ (i : ια ⊕ ιβ), Sum.elim α β i) ≃ₗ[k] (⨁ i : ια, α i) × (⨁ i : ιβ, β i) := ...

at the end, which is hopefully what was needed for decomposition into irreducibles

[David Ang]

@Peiran Wu this might be very useful for the torsion stuff you're doing...

[Amelia Livingston]

@Alessandro Iraci also did great work towards showing that the characters of the irreduble reps form a basis of the class functions - it is my fault we ran out of time to mention this, but I just thought it should be highlighted :smile:

[Alessandro Iraci]

@Amelia Livingston's contribution was invaluable! I would still be stuck dealing with casts without her help. :sweat_smile: