Root system theory - Githubissues

leanprover-community / mathlib4

The math library of Lean 4

https://leanprover-community.github.io/mathlib4_docs

Apache License 2.0

1.18k stars 252 forks source link

Root system theory #10067

Open ocfnash opened 5 months ago

ocfnash commented 5 months ago

Mathlib contains a definition of root systems. We should develop this theory further including:

A root system induces a canonical non-degenerate bilinear form
The dual of a root system is a root system
Define the automorphism group, Weyl group
Define bases and prove they exist
Define positive roots
Cartan matrices
Classify root systems

ocfnash commented 5 months ago

I'm delighted to see some interest in this from @ScottCarnahan

Please feel free to split this issue up into smaller pieces!

ScottCarnahan commented 5 months ago

It looks like @DeeproChoudhury already has made some progress on this, so I'll try to work in an orthogonal direction.

My interest in this issue mostly comes from the infinite-dimensional setting, because the real roots of a Borcherds-Kac-Moody algebra form a root system in the mathlib4 sense minus the [Finite ι] hypothesis. There is an axiomatic treatment by Moody, Pianzola "On infinite root systems" Trans. AMS v.315 (1989). Anyway, I've started a branch where I removed finiteness from the basic lemmas, and I hope it doesn't make things too cumbersome if merged.

ocfnash commented 5 months ago

@ScottCarnahan Please do carry out this generalisation if you have the appetite, and ping me on the PR as soon as you are ready.

I don't really know the theory of infinite root systems and I would be extremely happy to learn it via Mathlib.