issue !4#10067: Root system theory

Stream: triage

[Random Issue Bot]

Today I chose issue 10067 for discussion!

Root system theory
Created by @Oliver Nash (@ocfnash) on 2024-01-28
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

[Random Issue Bot]

Today I chose issue 10067 for discussion!

Root system theory
Created by @Oliver Nash (@ocfnash) on 2024-01-28
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

[Scott Carnahan]

Yes, I am making slow progress.

[Kabelo Moiloa]

Scott Carnahan said:

Yes, I am making slow progress.

Dear Prof. Carnahan I (and surely all of us mathlib people) would love to see a public repository with your progress. I'm interested in formalising Lie theory as well and would not like to duplicate work if I can avoid it, and I'm sure that I'm not alone in that.

[Scott Carnahan]

@Kabelo Moiloa I'm afraid there is no repository. I do have a branch where I do experimentation, but it is just a mess of failed tries. Mathlib4's treatment of root systems is at a level of generality that is not treated in the literature, so I tend to add PRs after I've worked out new steps informally. I've been meaning to write up an informal outline of my eventual direction, but other work tends to get in the way.

[Oliver Nash]

Just to state the obvious: much of Scott’s work is already in Mathlib. It’s all under Mathlib.LinearAlgebra.RootSystem

[Kabelo Moiloa]

Scott Carnahan said:

Kabelo Moiloa I'm afraid there is no repository. I do have a branch where I do experimentation, but it is just a mess of failed tries. Mathlib4's treatment of root systems is at a level of generality that is not treated in the literature, so I tend to add PRs after I've worked out new steps informally. I've been meaning to write up an informal outline of my eventual direction, but other work tends to get in the way.

Phew, thanks for the response. I doubt then that reading a book like Lie Groups: Beyond an Introduction (link to publically available pdf) would be enough preperation to try to help out then. What do you think @Scott Carnahan?

[Scott Carnahan]

After the proper definitions surrounding simple roots are worked out, I think the classification of finite crystallographic root systems over a linearly ordered commutative ring should be open to standard treatments.

[Random Issue Bot]

Today I chose issue 10067 for discussion!

Root system theory
Created by @Oliver Nash (@ocfnash) on 2024-01-28
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

[Scott Carnahan]

Yes, still making progress!