Smooth manifolds and types to sets for linear algebra in Isabelle/HOL

Abstract

We formalize the definition and basic properties of smooth manifolds in Isabelle/HOL. Concepts covered include partition of unity, tangent and cotangent spaces, and the fundamental theorem for line integrals. We also construct some concrete manifolds such as spheres and projective spaces. The formalization makes extensive use of the existing libraries for topology and analysis. The existing library for linear algebra is not flexible enough for our needs. We therefore set up the first systematic and large scale application of ``types to sets''. It allows us to automatically transform the existing (type based) library of linear algebra to one with explicit carrier sets.