Oliver Nash
ABSTRACT
Lie algebras are an important class of algebras which arise throughout mathematics and physics. We report on the formalisation of Lie algebras in Lean's Mathlib library. Although basic knowledge of Lie theory will benefit the reader, none is assumed; the intention is that the overall themes will be accessible even to readers unfamiliar with Lie theory.
Particular attention is paid to the construction of the classical and exceptional Lie algebras. Thanks to these constructions, it is possible to state the classification theorem for finite-dimensional semisimple Lie algebras over an algebraically closed field of characteristic zero.
In addition to the focus on Lie theory, we also aim to highlight the unity of Mathlib. To this end, we include examples of achievements made possible only by leaning on several branches of the library simultaneously.
- J. F. Adams. 1996. Lectures on exceptional Lie groups. University of Chicago Press, Chicago, IL. isbn:0-226-00526-7; 0-226-00527-5 With a foreword by J. Peter May, Edited by Zafer Mahmud and Mamoru MimuraGoogle Scholar
- Edward Ayers. 2021. Widgets: interactive output in VSCode. In Lean Together 2021, January 4–7, 2021. https://leanprover-community.github.io/lt2021/schedule.htmlGoogle Scholar
- John Baez and John Huerta. 2010. The algebra of grand unified theories. Bull. Amer. Math. Soc. (N.S.), 47, 3 (2010), 483–552. issn:0273-0979 https://doi.org/10.1090/S0273-0979-10-01294-2 Google ScholarCross Ref
- Anthony Bordg and Nicolò Cavalleri. 2021. Elements of Differential Geometry in Lean: A Report for Mathematicians. CoRR, abs/2108.00484 (2021), arXiv:2108.00484. arxiv:2108.00484Google Scholar
- Nicolas Bourbaki. 1998. Lie groups and Lie algebras. Chapters 1–3. Springer-Verlag, Berlin. isbn:3-540-64242-0 Translated from the French, Reprint of the 1989 English translationGoogle Scholar
- Nicolas Bourbaki. 2002. Lie groups and Lie algebras. Chapters 4–6. Springer-Verlag, Berlin. isbn:3-540-42650-7 Translated from the 1968 French original by Andrew PressleyGoogle Scholar
- Nicolas Bourbaki. 2005. Lie groups and Lie algebras. Chapters 7–9. Springer-Verlag, Berlin. isbn:3-540-43405-4 Translated from the 1975 and 1982 French originals by Andrew PressleyGoogle Scholar
- Mario Carneiro. 2019. The Type Theory of Lean. arxiv:https://github.com/digama0/lean-type-theory/releases. Master thesisGoogle Scholar
- Élie Cartan. 1894. Sur la structure des groupes de transformations finis et continus. Librairie Nony, 1–156. https://archive.org/details/surlastructured00bourgoog/page/n8/mode/2upGoogle Scholar
- A. J. Coleman. 1989. The greatest mathematical paper of all time. Math. Intelligencer, 11, 3 (1989), 29–38. issn:0343-6993 https://doi.org/10.1007/BF03025189 Google ScholarCross Ref
- José Figueroa-O’Farrill. 2008. A geometric construction of the exceptional Lie algebras F_4 and E_8. Comm. Math. Phys., 283, 3 (2008), 663–674. issn:0010-3616 https://doi.org/10.1007/s00220-008-0581-7 Google ScholarCross Ref
- Meinolf Geck. 2017. On the construction of semisimple Lie algebras and Chevalley groups. Proc. Amer. Math. Soc., 145, 8 (2017), 3233–3247. issn:0002-9939 https://doi.org/10.1090/proc/13600 Google ScholarCross Ref
- Wilhelm Killing. 1888. Die Zusammensetzung der stetigen endlichen Transformations-gruppen. Math. Ann., 31, 2 (1888), 252–290. issn:0025-5831 https://doi.org/10.1007/BF01211904 Google ScholarCross Ref
- Wilhelm Killing. 1888. Die Zusammensetzung der stetigen endlichen Transformationsgruppen. Math. Ann., 33, 1 (1888), 1–48. issn:0025-5831 https://doi.org/10.1007/BF01444109 Google ScholarCross Ref
- Wilhelm Killing. 1889. Die Zusammensetzung der stetigen endlichen Transformations-gruppen. Math. Ann., 34, 1 (1889), 57–122. issn:0025-5831 https://doi.org/10.1007/BF01446792 Google ScholarCross Ref
- Bruno Le Floch and Ilia Smilga. 2018. Action of Weyl group on zero-weight space. C. R. Math. Acad. Sci. Paris, 356, 8 (2018), 852–858. issn:1631-073X https://doi.org/10.1016/j.crma.2018.06.005 Google ScholarCross Ref
- Sophus Lie. 1880. Theorie der Transformationsgruppen I. Math. Ann., 16, 4 (1880), 441–528. issn:0025-5831 https://doi.org/10.1007/BF01446218 Google ScholarCross Ref
- Mathoverflow. 2021. Is the natural map from the free Lie algebra to the free associative algebra injective? In MathOverflow 2021. https://mathoverflow.net/questions/396680Google Scholar
- Jean-Pierre Serre. 1987. Complex semisimple Lie algebras. Springer-Verlag, New York. isbn:0-387-96569-6 https://doi.org/10.1007/978-1-4757-3910-7 Translated from the French by G. A. Jones Google ScholarCross Ref
- The mathlib community. 2020. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020. 367–381. https://doi.org/10.1145/3372885.3373824 Google ScholarDigital Library
- J. Tits. 1966. Algèbres alternatives, algèbres de Jordan et algèbres de Lie exceptionnelles. I. Construction. Nederl. Akad. Wetensch. Proc. Ser. A 69 = Indag. Math., 28 (1966), 223–237.Google Scholar
- Marc A. A. van Leeuwen, Arjeh M. Cohen, and Bert Lisser. 2000. LiE, A package for Lie Group Computations. Computer Algebra Nederland, Amsterdam. isbn:90-74116-02-7 http://wwwmathlabo.univ-poitiers.fr/~maavl/LiE/Google Scholar
- E. B. Vinberg. 2005. Construction of the exceptional simple Lie algebras. In Lie groups and invariant theory (Amer. Math. Soc. Transl. Ser. 2, Vol. 213). Amer. Math. Soc., Providence, RI, 241–242. https://doi.org/10.1090/trans2/213/15 Translated from Trudy Sem. Vekt. Tenz. Anal. 13 (1966), 7–9 Google ScholarCross Ref
- Eric Wieser. 2021. Scalar actions in Lean’s mathlib. CoRR, abs/2108.10700 (2021), arXiv:2108.10700. arxiv:2108.10700Google Scholar
Index Terms
- Formalising lie algebras
Recommendations
Modal MTL-algebras
A modal MTL-algebra is an algebra in the variety generated by the modal MTL-chains-linearly ordered commutative, bounded, integral, residuated lattices equipped with a unary order-preserving operation. Reverse modal MTL-algebras can be defined similarly ...
EQ-algebras from the point of view of generalized algebras with fuzzy equalities
EQ-algebras introduced by Novak are algebras of truth values for a higher-order fuzzy logic (fuzzy type theory). In this paper, the compatibility of multiplication w.r.t. the fuzzy equality in an arbitrary EQ-algebra is examined. Particularly, an ...
Differential (Lie) algebras from a functorial point of view
It is well-known that any associative algebra becomes a Lie algebra under the commutator bracket. This relation is actually functorial, and this functor, as any algebraic functor, is known to admit a left adjoint, namely the universal enveloping algebra ...
Comments