Amy Needham

Stream: new members

[Amy Needham]

Hello!
I'm Amy, I'm a master's (part III) student at Cambridge, mostly interested in group theory
I've been somewhat aware of lean for a couple years now (originally through finding the natural numbers game), but as I've found myself with surprisingly little to do over this Christmas break, I thought I might take a deeper look at lean (and hopefully eventually add some more group theory to Mathlib)
I'm slowly working my way through Functional Programming in Lean, so we'll see where this goes

[Kevin Buzzard]

Now would be a perfect time to do some of the basics in undergraduate representation theory! We have all the definitions but very few of the theorems.

[Jireh Loreaux]

#mil might be more suited for you than #fpil, given your background. Not that #fpil is by any means a bad thing to read, it's great and well-written. It just might not be the ideal on-ramp for you.

[Kevin Buzzard]

If you are a mathematician who wants to know about what's going on under the hood then #tpil might be more appropriate than #fpil

[Amy Needham]

Ah!
Thank you for the recommendation (both of book, and the note about representation theory - I'm a little surprised, but it's definitely something that sounds interesting to do)
!

[Kevin Buzzard]

Definitions are difficult in formalization and it took the community a long time to decide what the exact definition of Representation should be, but we have finally decided. I'm thinking about continuous representations for the FLT project and am running into all sorts of holes. We got the definition of subrepresentation literally last week in #31554 (upstreamed from FLT) -- this is why I'm saying that it's a perfect time to start thinking about the basic theory. The next step is probably IsIrreducibleRepresentation \rho, defined to mean IsSimpleOrder (Subrepresentation \rho), and then proofs of things like 1-dimensional representations are irreducible etc.

[Jireh Loreaux]

Kevin, can you point me to the discussion about docs#Representation ? I looked there expecting to see something different based on your comments, but what I found is precisely what I expected. Is the issue that we were worried about V →ₗ[k] V having two different Mul instances and that we should use a type synonym instead?

[Andrew Yang]

Here is the previous discussion. Basically the question was how much should we be bundling things.
#maths > Representation Theory @ 💬

[Yaël Dillies]

Hey @Amy Needham, former Part III student here. If you're interested in formalising representation theory, I will soon start a project to formalise the Fourier theory of compact groups.

[Yaël Dillies]

(in fact, it'll be more general, but the greater generality isn't really famous)

[Kevin Buzzard]

This breaks into two different questions -- compact connected groups (which needs analysis) and finite groups (which needs completely different techniques)