coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Bruno Le Floch <blflatex AT gmail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Classification of simple Lie algebras
- Date: Mon, 1 Jan 2018 16:18:14 -0500
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=blflatex AT gmail.com; spf=Pass smtp.mailfrom=blflatex AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f178.google.com
- Ironport-phdr: 9a23:LVKfwhCzgICRxPjBqtraUyQJP3N1i/DPJgcQr6AfoPdwSPvyrsbcNUDSrc9gkEXOFd2Cra4c0qyO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUmTaxe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoJNyM3/n/UhMJ+gq1Urw6uqRNkzo7IYoyYLuZycr/TcN4YQ2dKQ8ZfVzZGAoO5d4YCEvABPfter4n6ulAAqwWxDhSsCuPrzT9Hmn/21rA93us6FQHG0gggEMgSsHvKo9T4L6gSUeWvw6nJyTXPde9Z2TD46IXRdB0qvP+CXbV1ccXLyEkvERvIj1uRqYzmPjOVzvoCvHWa7+V6T+6vjHQnqw5prji128cgkI/JhoYNxlDL9CV53IY1JcCjR0JhfdGkF55QuieHPIV1WsMvW39ktDo+x7EcupO2fDIGxIo5yxLDcfCLboqF7xH7WOuTLzp0nm9pdbawihqo70Ss0PDwW82p3FtMsyFLiMPDtmoX2BzW8sWHSuVy/kOm2TuX0gDc8OBEIUQtmarCKJ4t3qc8lpQOvUnBHSL6gkr2jKiRdkUr/uin9f7rbanhpp+ZL4N0iwf+PboymsGnH+g0LgwDU3KY9Om8zrHv41P1TKlQgvErkKTUs4jWJcEBqa64Bw9V3Jwj6xG6Dzq+y9sYmXcHLFZfdxKbkYfoNErDIP/9DfilglSslC1nyOzBPr3kGpnNNGTMkK/9fbZh7E5R0BY8zddG555NFr4BJO/zVVTqudzDDh45NhS0zPz9BNV80IMeQ2OPDbWDPKPcq1/brt4oduKLfcoevCv3A/kj/f/ny3EjynEHeqz894EKbnfwOvkuDUGeanqk1t0FH2MDogcuZOPvgVyGFzVUYiDhDOoH+jgnBdf+Xs/4TYe3jenZ0Q==
Hello, and happy new year,
Has the classification of (semi-)simple Lie algebras [1] and their root
systems been formalized in Coq?
Googling only gave the page "Formalizing 100 Theorems" [2], which lists
this among problems it does not track. Are there current efforts in
this direction? The classification boils down to a combinatorial
question about matrices of integers, then to a classification of certain
graphs and trees. Where can I learn of existing libraries to manipulate
such objects?
Unimportant background: to prove some property of representations of
simple Lie algebras, we had to perform a somewhat tedious case by case
analysis (doable by hand), which we have started formalizing in Coq [3].
For now we are using the classification of simple Lie algebras (and
their weights and roots) as a black box since it is well established.
However, that increases chances of typos or bugs in the code listing
various conditions on weights of each Lie algebra.
Thanks in advance for any information,
Best regards,
Bruno
[1]: https://en.wikipedia.org/wiki/Semisimple_Lie_algebra
[2]: http://www.cs.ru.nl/~freek/100/
[3]: https://github.com/blefloch/lie-algebra-w0
(Admittedly the code is ugly: I started learning Coq a month ago.)
- [Coq-Club] Classification of simple Lie algebras, Bruno Le Floch, 01/01/2018
- Re: [Coq-Club] Classification of simple Lie algebras, Cyril Cohen, 01/11/2018
- Re: [Coq-Club] Classification of simple Lie algebras, Florent Hivert, 01/11/2018
- Re: [Coq-Club] Classification of simple Lie algebras, Bruno Le Floch, 01/14/2018
- Re: [Coq-Club] Classification of simple Lie algebras, Florent Hivert, 01/11/2018
- Re: [Coq-Club] Classification of simple Lie algebras, Cyril Cohen, 01/11/2018
Archive powered by MHonArc 2.6.18.