← All papers
Formalizing Geometric Algebra in Lean
cs.LO
Oct 7, 2021 · v2
TL;DR
Formalizes Clifford/Geometric algebras in Lean 3 using a basis-free universal property approach.
Abstract
This paper explores formalizing Geometric (or Clifford) algebras into the Lean 3 theorem prover, building upon mathlib. We formalize the multivectors as the quotient of the tensor algebra by a suitable relation, which provides the ring structure automatically, then establish the universal property of the Clifford algebra. Our approach does not require a choice of basis, distinguishing it from existing formalizations in other theorem provers. We show how operations and structure such as involutions, versors, and the Z_2-grading can be defined using the universal property alone, and how to recover an induction principle for proving statements about these definitions.
Problem
Geometric (Clifford) algebras are important in physics and geometry but had not been formalized in a basis-free manner in a theorem prover.
Approach
The authors formalize Geometric algebras in Lean 3 building on mathlib. Multivectors are defined as the quotient of the tensor algebra by a suitable relation, giving the ring structure automatically. The universal property is established and used to define operations such as involutions, versors, and the Z_2-grading without choosing a basis.
Results
A basis-free formalization of Clifford algebras in Lean is achieved, distinguishing it from prior formalizations in other provers. An induction principle for proving statements about definitions via the universal property is recovered.