Mengdelære i homotopi typeteori

Har du lurt på hva fundamentet for matematikk er? Hvilke regler og aksiom starter vi fra for å så kunne gjøre all den matematikken vi er vant til? Da er du ikke alene. Siden starten av 1900-tallet har det etablerte fundamentet for matematikk vært noe som heter mengdelære. Men i løpet av 2000-tallet har en ny teori dukket opp: homotopi typeteori (HoTT).

HoTT er ganske ulikt mengdelære, og kan argumenteres for å ligne mer på slik som moderne matematikere faktisk tenker når de gjør matematikk. HoTT er dessuten naturlig godt egnet til å programmeres på en datamaskin. Dermed er det mulig å få en datamaskin til å verifisere korrektheten av et matematisk bevis i HoTT. Dette har gjort at HoTT idag er et populært og aktivt forskingsområde.

Et naturlig spørsmål som dukker opp er om vi kan sammenligne mengdelære og HoTT? En generell måte å sammenligne matematiske systemer er å se om man kan lage en modell av det ene systemet i det andre. Elisabeth undersøker i forskningen sin modeller av mengdelære i HoTT. Hun konstruerer modeller av flere varianter av mengdelære i HoTT. Slike modeller av mengdelære i HoTT betyr at alt som kan gjøres med den mengdelæren også kan gjøres i HoTT.

I sin avhandling viser Elisabeth at det er mulig å lage modeller av både velfundert (vanlig) og ikke-velfundert (mengdene kan være uendelig dype) mengdelære i HoTT. Hun bruker dessuten muligheten for høyere struktur som finnes i HoTT til å gi en generalisering av mengdelære. Det første nivået over vanlig mengdelære i denne generaliseringen gir en interessant kobling mellom multimengder (mengder som kan ha flere forekomster av samme element) og gruppoider (en viktig matematisk struktur).

Personalia

Elisabeth Stenholm (f. 1993) har en master i matematikk fra Stockholms Universitet (SU). Doktorgradsprosjektet ble gjennomført ved Institutt for Informatikk, Universitetet i Bergen (UiB). Hovedveilerere var Anders Mörtberg (SU) og Håkon Gylterud (UiB), og biveiledere Mikhail Barash (UiB) og Marc Bezem (UiB).