Die klare Sprache der Mathematik hat mich bereits als Jugendlicher genug begeistert, um mein Studienfach zu bestimmen. Heute sehe ich einen Grund für diese Begeisterung darin, dass eine genau festgelegte Sprache es ermöglicht sehr präzise über die Realität zu reden und damit diese Sprache selbst zu einer Antwort auf die Frage wird, was die grundlegenden Gesetzmäßigkeiten unserer Welt sind.
Der wichtigste Aspekt meiner Doktorarbeit ist für mich, dass sie zeigt, wie eine nur wenige Jahre alte, von Grund auf verschiedene mathematische Sprache in der Lage ist Konstruktionen der Geometrie zu vereinfachen. Die Sprache, die ich in meiner Arbeit verwendete, wird Modale Homotopietypentheorie genannt und hat es mir ermöglicht über aktuelle Forschungsgegenstände der reinen Mathematik in einer wesentlich intuitiveren und knapperen Art und Weise zu reden, als das bisher möglich war.
Einer der wichtigsten Unterschiede zur üblichen Mathematik ist der Umgang mit dem Konzept Gleichheit. Normalerweise wird Gleichheit als eine Aussage betrachtet: Sinnvolle Antworten auf die Frage, ob zwei Objekte gleich sind, sind etwa "Ja" oder "Nein". In der Homotopietypentheorie kann die Frage nach der Gleichheit zweier Objekte ein kompliziertes Objekt sein.
Ein Beispiel, um dieses Prinzip zu verdeutlichen ist der Satz "Diese zwei Blatt Papier sind gleich". Stellen Sie sich zwei identische DIN-A4-Blätter vor und machen Sie sich klar, warum wir in einer solchen Situation dieser Aussage zustimmen würden. Eine mögliche Antwort wäre, dass wir in Gedanken das eine Blatt Papier auf das andere schieben können, um so zu sehen, dass es sich um physikalische Objekte handelt, die sich nur durch ihre Lage im Raum unterschieden. Allerdings gibt es mehrere Möglichkeiten, die beiden Blätter ineinander zu überführen, weil es mehr als eine Bewegung gibt, die das erste auf das zweite Blatt schiebt. Wenn man die Symmetrien der Blätter benutzt, kann man leicht verschiedene Bewegungen durchführen: Ein direktes Aufeinanderschieben ist verschieden vom Schieben mit anschließendem Drehen um eine der Symmetrieachsen. Diese beiden Bewegungen können als verschiedene Gleichheiten zwischen den beiden Blättern gesehen werden!
Bereits Ende der Sechziger Jahre hat sich gezeigt, dass es in manchen Fällen sehr nützlich ist, diese zusätzlichen Gleichheiten, die durch Symmetrien gegeben sind, miteinzubeziehen. Damals wurden sogenannte Modulstacks eingesetzt, um Räume zu beschreiben, deren Punkte für Varianten eines geometrischen Objekts stehen. Gleichzeitig sollten Informationen über die Symmetrien der geometrischen Objekte und somit darüber, auf welche Arten manche Punkte sich selbst gleichen, erhalten bleiben. Obwohl der Einsatz dieses Prinzips damals sehr erfolgreich war, ist es heute nur in recht speziellen Mathematikerkreisen selbstverständlich diese Sichtweise zu beherrschen. Ich sehe den Grund darin, dass Modulstacks in der herkömmlichen mathematischen Sprache sehr schwierig zu beschreiben sind. Der Ausgangspunkt meiner Doktorarbeit war nun zu prüfen, ob sich dieses Problem durch den Gebrauch einer anderen Sprache, der Homotopietypentheorie, beheben lässt.
Ein Vorteil gegenüber der üblichen Herangehensweise an Probleme dieser Art ist, dass der erweiterte Begriff der Gleichheit sehr gut in die Sprache integriert ist. Eine Folge ist etwa, dass gleiche Objekte genau die gleichen Eigenschaften haben. Es ist ein Verdienst des letztes Jahr verstorbenen, berühmten Mathematikers Vladimir Voevodsky, gesehen zu haben, dass eine mächtige formale Sprache, eine sogenannte Typentheorie existiert, die diese erweiterte Gleichheit zulässt.
Eine konkrete Aufgabenstellung für meine Doktorarbeit bekam ich schließlich von Urs Schreiber, einem Mathematiker, der Probleme der theoretischen Physik mithilfe der sogenannten höheren Topostheorie löst. Das "höhere" in "höhere Topostheorie" bezieht sich auf eine Variante dieser Theorie, deren Sinn auch darin gesehen werden kann, ähnlich wie die Homotopietypentheorie, einen anderen Umgang mit dem Konzept Gleichheit umzusetzen. Allerdings ist dieser Aspekt nachträglich in die Topostheorie eingebaut und nicht von vornherein in die Sicht auf die Welt integriert.
Bereits 2011 wandte sich Urs an die junge Homotopietypentheoriegemeinde, mit der Idee seine abstrakten axiome, genannt Differentialkohäsion, in die Homotopietypentheorie zu übertragen. Aufgegriffen wurde diese Idee damals und später zumindest durch Mike Shulman und erst 2015 formulierte Urs unter anderen Vorschlägen die erwähnte Aufgabenstellung zu meiner Doktorarbeit.
In dieser gelang es mir in mehreren Fällen durch die speziellen Eigenschaften der Homotopietypentheorie herkömmliche mathematische Argumentationsketten wesentlich abzukürzen. Außerdem waren die neuen Argumente für in dieser Sprache geübte Mathematiker deutlich einfacher nachzuvollziehen. Inhaltlich ging es dabei um grundlegende Eigenschaften des Raumes, die bei einer intuitiven Vorstellung davon, was "Raum" ist, so selbstverständlich sind, dass es einem Leser ohne mathematische Ausbildung kaum zumutbar ist, sich eine Welt ohne diese Eigenschaften vorzustellen. Ich möchte deswegen gleich zum Ende meiner Arbeit springen, in dem sogenannte formale Scheiben eine große Rolle spielen.
In einer physikalischen Anwendung kann man die formalen Scheibe um einen Punkt im Raum als die Menge aller möglichen Geschwindigkeiten verstehen, die ein Partikel an diesem Punkt haben kann. Wenn der Raum ähnlich zum Raum in dem wir leben ist, werden sich die formalen Scheiben von Punkt zu Punkt nicht wesentlich unterscheiden - sie sind alle gleich. Hier interessiert vor allem die Frage, wie die formalen Scheiben zusammenhängen, oder wie sie sich gleichen. Im uns umgebenden Raum scheint es naheliegend, mögliche Geschwindigkeiten an verschiedenen Punkten des Raumes zu vergleichen, indem man den Raum so verschiebt, dass ein Punkt auf den anderen wandert und dabei die Geschwindigkeiten einfach mit verschiebt. Ähnlich wie in der klassischen Theorie sind die möglichen Räume in meinem Ansatz zunächst nur als Ansammlungen von Koordinatensystemen zu verstehen, in denen noch festgelegt werden kann, wie die formalen Scheiben miteinander zusammenhängen. Für alltagsnahe Situationen ist es gerechtfertigt zu sagen, dass es oft mehrere Möglichkeiten gibt, eine solche Wahl zu treffen. Diese Wahlen entsprechen genau den Möglichkeiten dem abstrakten Raum eine konkrete geometrische Form zu geben.
In Modaler Homotopietypentheorie ist es möglich, diese Wahl einer konkreten geometrischen Form als Frage über die Gleichheiten zwischen den formalen Scheiben des Raumes zu stellen. Die Gleichheiten zwischen den formalen Scheiben des Raumes, entsprechen im Beispiel den Möglichkeiten die Geschwindigkeiten an verschiedenen Punkten zu vergleichen. Mittels Urs Schreiber's "Höherer Cartan Geometrie", ist es möglich spezielle Teile dieser Gleichheiten mit konkreten geometrischen Formen des Raumes in Zusammenhang zu bringen. Im Beispiel könnte man etwa nach Gleichheiten fragen, die die Winkel zwischen Geschwindigkeiten erhalten. Durch die abstrakte Ausdrucksweise ist diese klassisch komplizierte Fragestellung nun wesentlich klarer und kann in vielen vollkommen neuen Situationen angewandt werden. So ist meine Formulierung etwa direkt auf die Algebraische Geometrie anwendbar, ein bedeutendes Teilgebiet der reinen Mathematik, das mit großem Erfolg geometrische Methoden einsetzt, um Probleme die beim Lösen von Gleichungen auftauchen, zu lösen. Allerdings ist durch die Abstraktion die Anwendbarkeit nicht einmal auf die Geometrie beschränkt.
Zum Abschluss möchte ich noch auf einen bisher unerwähnten bedeutenden Unterschied zwischen dem mathematischen Arbeiten in der Homotopietypentheorie und der üblichen Art, Mathematik zu betreiben, hinweisen: Homotopietypentheorie lässt es zu, die oben erwähnten mathematischen Inhalte mittels spezieller Software am Computer einzugeben und zu prüfen. In der üblichen mathematischen Sprache wäre ein derart computergestütztes Vordringen in die oben beschriebenen Inhalte undenkbar.
Alle zentralen Aussagen meiner Doktorarbeit wurden mittels der Programmiersprache Agda aufgeschrieben und geprüft. Dabei ging es mir weniger um den Nachweis der Korrektheit meiner Ergebnisse, sondern vielmehr darum interaktiv zu lernen, wie man in Homotopietypentheorie argumentiert. Weiter gab es durch die von der Software geforderte Präzision immer wieder Denkanstöße meine Mathematik umzuformulieren und klarer zu gestalten.
Ich wurde durch meine Erfahrungen damit davon überzeugt, dass die Mathematik viel von dieser Art Computer einzusetzen gewinnen kann. Neben der Möglichkeit, Resultate anderer interaktiv zu nutzen, bietet sie zusätzlich die Chance leichter über große Distanz mit anderen Mathematikern zusammenzuarbeiten. Außerdem könnte diese Art Mathematik zu betreiben die Einstiegshürden für Neulinge auf dem Gebiet senken, da man keinen Experten der Homotopietypentheorie braucht, um das eigene Verständnis zu testen.
Durch die Computernähe und den Typentheorieanteil ergab sich für mich die Möglichkeit aktuelle Forschungsideen mit Wissenschaftlern aus anderen Bereichen, sogar der Informatik, auszutauschen. Das gibt mir Hoffnung, dass meine Arbeit dazu beiträgt, die Ideen der reinen Mathematik mehr Menschen als einem kleinen Kreis von Spezialisten zugänglich zu machen.