Isomorphism classes of irreducible representations

Stream: mathlib4

[Ryan Smith]

I'm trying to learn lean by formalizing Burnsides theorem and that led me to looking at how lean formalizes representations. For a given group G and field k we have the type FDRep k G, as well as a notion of what it means for a particular representation to be Irreducible, but does lean understand the concept of an isomorphism class of irreducible representations?

In an ideal world we would have both a type for an isomorphism class and also the ability to get a representative of that class for doing something concrete.

I originally came upon this question because I was trying to sum over all of the irreducible complex representations of a group when I realized that there was a lot being done implicitly with such a sum.

[Aaron Liu]

I guess isomorphism classes would be docs#CategoryTheory.Skeleton

[Aaron Liu]

the way to get a representative is docs#CategoryTheory.fromSkeleton

[Ryan Smith]

In lean it looks like irreducible representations are not called that and are instead called simple objects in the category theory sense of the word. I guess the question then is can I take the skeleton of the subcategory of simple objects from FDRep k G and how would I do that?

[Joël Riou]

The type of isomorphism classes of simple objects in a category C can be obtained as follows:

import Mathlib.CategoryTheory.Simple

namespace CategoryTheory

open Limits

variable (C : Type*) [Category C] [HasZeroMorphisms C]

def isSimpleObject : ObjectProperty C := fun X ↦ Simple X

#check Skeleton (isSimpleObject C).FullSubcategory

end CategoryTheory

[Ryan Smith]

Thank you! As far as I can see we don't have any notion of a character table for a group so this is a good start

[Junyan Xu]

We know the isomorphism classes of objects in a monoidal category form a monoid, and if the category is braided monoidal then it's commutatiave: CategoryTheory.Skeleton.instCommMonoid and it's used to define the Picard group of a commutative ring in #25337. It seems no one has done the counterpart for additive categories, where you get an Add(Comm)Monoid, and additive+monoidal should yield Semiring. (Side note: I've been working on some AddLocalization API that produces the "Grothendieck ring" from this: #28468)

[Ryan Smith]

That gives us the category of isomorphism classes of irreducible representations of a group G, but its still a category and not even a set yet correct? It is true that it is a finite set, but that's not obvious without proving something.

Is defining a category for isomorphism classes the wrong way to go about this if we eventually want to be able to talk about the (finite) set of elements of the skeleton of the subcategory of irreducible representations? The character table of a finite group is finite since there are only finitely many conjugacy classes and only finitely many irreducible representation isomorphism classes, but by starting with something so big are we making everything difficult?

Put another way, we eventually need to be able to talk about a finite set of representatives of isomorphism classes.

[Junyan Xu]

You can use docs#isotypicComponents to index the irreducible representations (= simple modules), and if necessary choose one simple submodule from each component. It recently landed in mathlib that the number of isotypic components of a Noetherian module is finite: docs#instFiniteElemSubmoduleIsotypicComponentsOfIsNoetherian, and a semisimple ring (e.g. the group ring k[G] with gcd(#G, char k)=1) as a module over itself is Noetherian.

[Artie Khovanov]

@Ryan Smith well, you should prove the underlying type of the category has finitely many elements, which yes you probably do prove by constructing a finite set of reps and showing every irrep is isomorphic to something in that finite set.

[Junyan Xu]

My feeling is that you don't need to invoke any category theory library to prove Burnside's theorem ...

[Artie Khovanov]

idk how "type of objects up to isomorphism" is defined elsewhere in the library
is it just a big quotient?

[Kevin Buzzard]

Junyan Xu said:

My feeling is that you don't need to invoke any category theory library to prove Burnside's theorem ...

right -- why not use docs#Representation instead of fighting with category theory?

[Ryan Smith]

How would you put this together then? We would take the isotypic components of the group ring, use this to argue that the set is finite, coerce each submodule to be a module in its own right, use the Representation machinery to get an instance of FDRep from each module, then finally form the indexed sum of characters we need for the standard proof?

[Antoine Chambert-Loir]

I'd like that we go back to the first message in the thread and clarify several points:

• You want to prove Burnside's theorem, presumably its the theorem that groups of order $p^aq^b$ (for two prime numbers $p$ and $q$) are solvable. Is this correct?

• There are several proofs of that theorem. What is the one that you intend to follow? From what reference?

• Famously, the initial one used character theory. A sketch of a modern proof along these lines is presented on the Wikipedia page that I linked above. It uses character theory at two points which seem absent from mathlib:

1. The orthogonality relation given by docs#FDRep.char_orthonormal is not the one that is needed, one needs the other one, summing over all finite dimensional representations. And it seems that this result is absent from mathlib.

2. It is also required to know that the chosen character has some (nonobvious) divisibility property.

• There are other proofs of Burnside's theorem, purely group-theoretical, and it may be an interesting challenge to prove them in mathlib. This would require less advanced technology and — I expect — enrich mathlib with results about objects such as the Fitting subgroup of a group.

[Anatole Dedecker]

I don't think I'm on topic, but when we will eventually define the irreducible dual of a (topological) group, I think what we should do is first define the abstract object (e.g as a skeleton) which naturally lives one universe higher, then prove that it is docs#Small, and then define the actual irreducible dual as the docs#Shrink of this abstract object.
We could of course live with it being higher in the universe tower, but I think the proof of smallness is easy enough that we may as well do it.

[Yaël Dillies]

Just letting you know that I am very interested in getting non-commutative Fourier analysis off the ground since this is appearing in my research, and that would involve defining the dual of a group.

[Ryan Smith]

I've never looked over the pure group theory version, my understanding is that it is a rather nontrivial and involved argument. Part of why I was trying the character theory version was to learn lean better in order to do something useful for FLT eventually. I'd consider a pure group theoretic version, I haven't done much with mathlib's group theory formalization so that has value too. Wikipedia links several research articles for the group theoretic version of Burnside; do you know of any friendlier expositions to judge what would be required?

[Kevin Buzzard]

I think that what we need with representation theory is for someone to do the basics (eg character table is a square) before we can think about the char theory proof of Burnside. This is not a very well-developed part of the library right now

[Antoine Chambert-Loir]

What could be helpful is that “we” furnish a proof_wanted version of the definitions and theorems that are requested. (The group is finite and the field is supposed to be algebraically closed and its characteristic prime to the cardinality of the group.)

• define the “set of irreducible characters” : (function which is the character of some finite dimensional irreducible representation). There might be a universe issue here, but it will resolve by itself.
• Prove that this set is a basis of the vector space of central functions
• Conclude that this set is finite, with cardinality the number of conjugacy classes of the group
• Prove that the regular representation decomposes as a direct sum of irreducible representations, each with multiplicity 1.

[Ryan Smith]

I think the "set of irreducible characters" is the real sticking point here. I may be losing momentum on this theorem; it seemed like a good first project but it's running into a lot of issues I don't know how to resolve to lean. Is the best way to define the set of irreducible characters to take the skeleton of the subcategory of finite dimensional CG modules? Is that machinery unnecessary?

[Kenny Lau]

it doesn't seem necessary because it seems like each character is a function G -> C?

[Kenny Lau]

(note you said "character")

[Kenny Lau]

Ryan Smith said:

I may be losing momentum on this theorem; it seemed like a good first project but it's running into a lot of issues I don't know how to resolve to lean

I think working with this is a very good way to internalise the universe issues into your brain, assuming you're at least interested in that

[Robert Maxton]

Yaël Dillies said:

Just letting you know that I am very interested in getting non-commutative Fourier analysis off the ground since this is appearing in my research, and that would involve defining the dual of a group.

Speaking as a physicist who somewhat suspects that he'll need noncommutative harmonic analysis for his upcoming research, I would also be very interested in contributing whatever I can here!

[Kevin Buzzard]

Making definitions is much harder than proving theorems, especially for beginners. A good beginner project is to prove a theorem where every definition you need in the proof is already in lean. Representation theory has loads of holes at the minute.

[Kenny Lau]

to this end, does that mean we should store unfinished files somewhere so that beginners can pick up from an easier spot?