Dozent:
Prof. Immanuel Halupczok (Sprechzeiten: nach Vereinbarung)
- Statt eines Kurzskripts steht hier, wo im hott-Buch was zu finden ist.(27.1.)
- Am 20.12. findet die Übung schon um 14:30 statt (gleicher Raum).(18.12.)
- Am 13.12. fällt die Übung aus.(12.12.)
- Am 4.12. fällt die Vorlesung aus.(3.12.)
- Werbung: Für logik-interessierte Master-Studierende an der hhu gibt es ein Erasmus+-Programm an der Universität Paris Diderot. Hier ein paar Infos dazu. (14.11.)
- Der Übungsgruppentermin bleibt Fr, 15:30-16:30. (17.10.)
- Diese Seite befindet sich noch im Aufbau... (11.07.)
Vorlesung:
Mi, 16:30-18:30, Raum 25.22.00.74
Übungen:
Fr, 15:30-16:30, Raum 25.22.03.73
Beginn der Übungen in der 2. Semesterwoche
Anmeldung:
Bitte melden Sie sich im LSF zur Vorlesung an. (Zu den Übungen brauchen Sie sich nicht separat anzumelden.)
Hier geht's ins LSF: zur Vorlesung und zu den Übungen
Wie der Übungsbetrieb läuft, wird in der Vorlesung bekanntgegeben.
Um die Leistungspunkte für das Modul zu erhalten, müssen Sie eine mündliche Prüfung bestehen. Um an der Prüfung teilnehmen zu können, müssen Sie
die Zulassung erhalten. Weitere Details werden in der Vorlesung bekanntgegeben.
Um Mathematik vollständig zu formalisieren (und z.B. präzise zu definieren, was ein Beweis ist), verwendet man heutzutage
meistens die Mengenlehre (genauer: ZFC). Die Grundidee ist, dass die einzigen mathematischen Objekte, die man wirklich benötigt,
Mengen sind; alle anderen mathematische Objekte (Zahlen, Tupel, etc.) werden in geeigneter Weise durch Mengen kodiert.
Während dies gut geeignet ist, um Metamathematik zu betreiben (also z.B. um zu beweisen, dass etwas unbeweisbar ist), ist
Homotopietyptheorie eine neue Formalisierung der Mathematik, die näher an der mathematischen Praxis ist. Insbesondere unterscheidet sie sich folgendermaßen von ZFC:
- Während in der Mengenlehre eigentlich sinnlose Ausdrücke (wie z.B. $3 \cup \operatorname{Abb}(\frac12, (\{4\},5))$) oft wohldefiniert sind,
wird in der Homotopietyptheorie strikt zwischen verschiedenartigen mathematischen Objekten unterschieden.
-
In der Mengenlehre ist Gleichheit einfach eine Äquivalenzrelation. In Homotopietyptheorie wird Gleichheit durch ein komplizierteres Konzept ersetzt, dass den Bedürfnissen der Algebra angepasst ist: Während z.B. zwei Zahlen in der Tat einfach nur gleich oder ungleich sein können, ist Gleichheit bei Vektorräumen komplizierter: Ist $\mathbb{R}^2 \oplus \mathbb{R}^3$ wirklich gleich $\mathbb{R}^5$ oder nur isomorph dazu? Und: Wenn zwei Vektorräume isomorph sind, gibt es (meistens) viele verschiedene Isomorphismen.
In der Vorlesung werden wir die Homotopietyptheorie kennenlernen (so, dass wir Sätze und Beweise formal in ihr aufschreiben können), wir werden Anwendungsbeispiele aus der Algebra sehen, und wir werden (unter gewissen Voraussetzungen) beweisen, dass Homotopietyptheorie konsistent ist, d.h. dass man darin keine widersprüchlichen Dinge beweisen kann. Dazu wird das Gleichheitskonzept der Homotopietyptheorie innerhalb von "klassischer" Mathematik als Homotopie zwischen simplizialen Komplexen interpretiert.
