Our formalisation of Lie Groups and Algebras has been published in the Archive of Formal Proof
Abstract
Lie Groups are formalised as locales, building on the AFP theory of Smooth Manifolds. We formalise the diffeomorphism group of a manifold, and the action of a Lie group on a manifold. The general linear group is shown to be a Lie group by proving properties of the determinant, and matrix inverses. We also develop a theory of smooth vector fields on a manifold , defined as smooth maps from the manifold to its tangent bundle . We employ a shortcut that avoids difficulties in defining the tangent bundle as a manifold, but which still leads to vector fields with the properties one would expect. We then construct the Lie algebra of a Lie group as an algebra of left-invariant smooth vector fields.
Schmoetten R. and Fleuriot J. D. (2024). Lie Groups and Algebras. Archive of Formal Proofs. ISSN: 2150-914x.