A Construction of the Lie Algebra of a Lie Group in Isabelle/HOL

TL;DR

The paper presents a comprehensive Isabelle/HOL formalisation of differential geometry concepts—smooth vector fields, tangent bundles, the diffeomorphism group, and Lie groups—culminating in a construction of the Lie algebra of a Lie group from left-invariant vector fields. It employs a locale-based, type-class-centric approach to manage complex structures within simple type theory, and establishes a tight connection between vector fields and derivations on $C^ ablafty(M)$. Concrete models, such as $({\mathbb R}^n, +)$ and $GL(n,\mathbb{R})$, demonstrate the method’s viability, while transfer and Type-to-Sets tooling mitigate representational and interoperability challenges. The work advances mechanised differential geometry in Isabelle/HOL and lays the groundwork for future extensions in advanced mathematics and natural science formalisation, including potential applications in physics.

Abstract

This paper describes a formal theory of smooth vector fields, Lie groups and the Lie algebra of a Lie group in the theorem prover Isabelle. Lie groups are abstract structures that are composable, invertible and differentiable. They are pervasive as models of continuous transformations and symmetries in areas from theoretical particle physics, where they underpin gauge theories such as the Standard Model, to the study of differential equations and robotics. Formalisation of mathematics in an interactive theorem prover, such as Isabelle, provides strong correctness guarantees by expressing definitions and theorems in a logic that can be checked by a computer. Many libraries of formalised mathematics lack significant development of textbook material beyond undergraduate level, and this contribution to mathematics in Isabelle aims to reduce that gap, particularly in differential geometry. We comment on representational choices and challenges faced when integrating complex formalisations, such as smoothness of vector fields, with the restrictions of the simple type theory of HOL. This contribution paves the way for extensions both in advanced mathematics, and in formalisations in natural science.

Figures (2)

• Figure 1: Differentiability of $f\colon M \to M'$ is defined using the Euclidean function $\psi \circ f \circ \phi^{-1}$. Chart (co)domains are drawn in dashed lines. See def:diff.
• Figure 2: Let the type implement ${\mathord{\mathbb R}}^n$. Let $\psi$ be a chart of $M$ with domain $U$, and consider inclusions $\iota : U \hookrightarrow M$ and $\kappa : \psi(U) \hookrightarrow {\mathord{\mathbb R}}^n$. Then the push-forward maps $d\iota$, $d\kappa$ and $d\psi$ are linear isomorphisms of tangent spaces. The directional derivative $\nabla: y \mapsto (y \cdot { \left.\nulldelimiterspace \nabla \newline \right|_{x} })$ implements the isomorphism between Euclidean space and its tangent space at $x$.

Theorems & Definitions (6)

• Definition 2.1: Differentiability on Manifolds; Diffeomorphism
• Definition 2.2: Push-forward
• Definition 3.1
• Definition 3.2
• Theorem 3.1: lee2012
• Definition 4.1: Lie algebra