lean-graded-rings-supersymmetry

Stream: maths

[Tchsurvives]

https://github.com/eric-wieser/lean-graded-rings i came across @Eric Wieser and @Jujian Zhang 's work on graded rings and was very excited because I've been thinking of writing a supersymmetry computer algebra system to aid with physics calculations involving supersymmetry (which tend to be tedious). My plan is to write tactics to help manipulations. Eric and Jujian, what do you think about a mathlib library for Lie superalgebras? is mathlib ready for it?

https://mathoverflow.net/a/311237 mention of superalgebra in this thread

[Notification Bot]

This topic was moved here from #mathlib4 > lean-graded-rings-supersymmetry by Heather Macbeth.

[Eric Wieser]

Hi, I'm glad you found our paper exciting! I'm afraid I'm not familiar with graded Lie (super)algebras, but after a quick glance at the wikipedia pages I think they could be within reach.

[Eric Wieser]

A reasonable first target (after formalizing the axioms) would be to show that

Given any associative superalgebra $A$ one can define the supercommutator on homogeneous elements by

$[x,y] = xy - (-1)^{|x||y|}yx$

and then extending by linearity to all elements. The algebra $A$ together with the supercommutator then becomes a Lie superalgebra.

A related target that's on my TODO list is the tensor product of graded algebras; I think the challenges you'll face proving the above were similar to the ones I was facing here; both involve defining a bilinear operator pairwise on grades.

[Eric Wieser]

Note that @Oliver Nash is probably a better person to ask about Lie algebras!

[Oliver Nash]

Indeed, I'd be happy to answer any questions about Lie algebras in Mathlib and interested to see development of graded variants.