Formalising the Van Kampen Theorem for Directed Topology

Directed topology is a fairly new field of mathematics with applications in concurrency. It extends the concept of a topological space by adding a notion of directedness in which directed paths play a very important role. There are direction preserving maps between directed spaces called directed maps. A special case of these is a directed path homotopy that transforms one directed path into another. Using these deformations, directed paths are partitioned into equivalence classes and a special category, the fundamental category, can be linked to a directed space. In this thesis we will explain these definitions and present a special theorem: a directed version of the Van Kampen Theorem. This theorem allows the calculation of fundamental categories by combining local knowledge about paths. Our main contribution is the formalization of this material using the Lean proof assistant and we show how we have implemented this.

Leiden University Student Repository

Documents

In Collections

Formalising the Van Kampen Theorem for Directed Topology