Induced representation

Stream: Is there code for X?

[Gareth Ma]

Does the notion of induced representation exist? If not, would it be correct to define it via its universal property?

[Gareth Ma]

Okay hmm I don't think I'll take on the task of defining it since I am not confident enough in my categorical understanding of rep theory. However, it seems the correct definition should be a proposition Induced p1 p2 that says p2 is induced from p1. Then you can prove the usual explicit construction satisfies it, and also prove the universal property of induced reps to show it's unique. Then of course the key remaining thing is to prove it's adjoint to the restriction functor Action.res, i.e. the Frobenius reciprocity

[Kim Morrison]

It would be great to have this!

[Kevin Buzzard]

I would argue that the main problem with this question is that we have three definitions of representation (docs#Representation, docs#Rep and docs#FDRep) so it's not even clear (to me) what the question is asking right now.

[Adam Topaz]

Don’t forget to add to that list docs#Module plus docs#MonoidAlgebra

[Adam Topaz]

Presumably that would make the induced representation trivial to define

[Gareth Ma]

My understanding is we should deal with Rep

[Gareth Ma]

FDRep is a subcategory of Rep anyways so we should keep it no problem, and Representation is an unbundled version of a Rep, which I think we should keep but possibly name it better :thinking:

[Gareth Ma]

Adam Topaz said:

Presumably that would make the induced representation trivial to define

I tried last night defining it as k[G] otimes_{k[H]} V, but couldn’t figure out how to convince Lean how to make k[G] a k[H]-module. I think it’s a definition somewhere and not an instance, but I couldn’t find it

[Loris Parisot]

Hi ! I was wondering if someone finally managed to define induced representations (I didn't start a new topic because I saw that this one was already existing) ?

[Kevin Buzzard]

There are probably lots of different ways to do this because right now there are lots of different ways to talk about a representation of a group :-( @Johan Commelin did you ever make any sense of this?

[Edison Xie]

after we develop theories about tensor product over non-comm rings k[G] modules should be the way to do? @Kevin Buzzard

[Edison Xie]

Also it would be easy to just define the induced module as tensoring k[G] and M over k[H]

[Antoine Chambert-Loir]

You could define the “coinduced” representation, $Hom_{k[H]}(k[G], V)$ which, iianm, is usually as good.

[Kevin Buzzard]

Basically this question is not well defined until someone suggests (a) the domain of definition and (b) a formal statement of the hypotheses needed in order to define the induced representation.

[Junyan Xu]

I tried last night defining it as k[G] otimes_{k[H]} V, but couldn’t figure out how to convince Lean how to make k[G] a k[H]-module. I think it’s a definition somewhere and not an instance, but I couldn’t find it

You can use Module.compHom which is used in ModuleCat.extendScalars via ModuleCat.restrictScalars if you track it down.
In any case tensor product needs to be generalize to the noncommutative setting, and potentially semilinearized; I wonder whether that could/should be done simultaneously with @Anatole Dedecker's #24208 which makes a different generalization.
Now that the APIs for isotypic components and Wedderburn--Artin are ready, I might develop some semisimple representation theory of finite groups subsequently, so there will be motivation for induced representations :)

[Sophie Morel]

Antoine Chambert-Loir said:

You could define the “coinduced” representation, $Hom_{k[H]}(k[G], V)$ which, iianm, is usually as good.

If you want Frobenius reciprocity (and he does want it), then the coinduced representation is not as good, as it is naturally a right adjoint and not a left adjoint. You'd need to prove somehow that then induced and coinduced representations are isomorphic if H is of finite index in G.

[Johan Commelin]

Kevin Buzzard said:

There are probably lots of different ways to do this because right now there are lots of different ways to talk about a representation of a group :-( Johan Commelin did you ever make any sense of this?

Sorry, haven't been able to make progress in the past week.