Representation Theory API Improvement (1?)

Stream: mathlib4

[Gareth Ma]

Recently I got into representation theory. I made a few threads in the past days of some difficulties I faced, e.g. here and here and here. I am trying to improve it, in particular by creating some API to convert between the categorical and "classical" (with G -> GL(V)) setups. I ran into a lot of problems, so I made them into a file, and any help on the sorrys would be great. I am very unfamiliar with algebra in Mathlib, so sorry for the horrible code. Here is the link.

As a consequence, the following can be proven, which was my original goal: rank 1 representations are irreducible/simple

image.png

[Winston Yin (尹維晨)]

Unrelated to the mathematics: I think FdRep should be called FDRep.

[Gareth Ma]

I can make a PR for that

[Gareth Ma]

I finished the main goal of my original question:

theorem Rep.isSimpleModule_iff_simple : IsSimpleModule k⟦G⟧ V.ρ.asModule ↔ Simple V :=
  ⟨fun _ ↦ simple_of_isSimpleModule, fun _ ↦ isSimpleModule_of_Simple⟩

Now I just have to translate the language also to FDRep, and it will be done. From there some of the missing "undergrad maths in Mathlib" , e.g.

Linear representations: irreducible representation, examples

and also

Representation theory of finite groups: representations of abelian groups, dual groups, Fourier transform for finite abelian groups, convolution, class function over a group, orthonormal basis of irreducible characters, examples of groups with small cardinality.

[Gareth Ma]

Proof found here. TLDR use more category theory

[Gareth Ma]

I find it quite confusing to keep track of all the defeq types. For example, a morphism M --> N between two ModuleCat R $R$-modules is defeq is to M ->_l[R] N ($R$-linear maps). On paper of course this is obvious, but when writing the Lean code the user kind of have to memorise that, and transfer between the two when needed. It also means exact? doesn't work 70% of the time. That's the point of the theorems like the one proven above, so that users don't have to think about these confusing things

[Dean Young]

You might also want to consult Johan Commelin about designing an API for his Dynkin diagrams, since he's demonstrating the classification theorem.

[Gareth Ma]

I have created some PRs related to representation theory now:

• #14140 FdRep is rigid (autonomous)
• #14309 FdRep -> FDRep as suggested by Winston above
• #14313 FdRep is a full subcategory of Rep

I think Kim is not too free currently so feel free to take over #14140 if you see this.
I have a few more results e.g. #14308 and also the isSimpleModule_iff_simple above.