Home
New phds

Warning message

There has not been added a translated version of this content. You can either try searching or go to the "area" home page to see if you can find the information there
Ny doktorgrad

Formalisering av teorem i kategoriteori

Stefano Piceghello disputerer 3.12.2021 for ph.d.-graden ved Universitetet i Bergen med avhandlingen "Coherence for Monoidal and Symmetric Monoidal Groupoids in Homotopy Type Theory".

Main content

Matematikk handler om abstrakte strukturer og objekt, og utforskningen av egenskapene og sammenhengene deres; man utfører slike utforskninger ved å bruke bevis. Til forskjell fra andre vitenskapelige fagområder – hvor bevis oppnås ved empirisk utforsking – er et matematisk bevis et logisk argument som gjennom en rekke deduktive steg fører til nye påstander ut fra de man allerede kjenner. Grunnlagene for matematikk studerer de mange ulike logiske systemene som gjør det mulig å gjennomføre et bevis.

Homotopi-typeteori (HoTT) har oppstått i de siste årene som et grunnlag for matematikk. HoTT ble utviklet som en variant av andre typeteorier, men den skiller seg ut takket være den innovative måten begrepet matematisk likhet blir handtert på: Et bevis på at a=b er det samme som en sti fra a til b. I HoTT er «typer» de primitive begrepene; de beskriver både objekter og påstander. Matematiske bevis blir bygget opp som syntaktiske uttrykk inni teorien, og disse kan sjekkes ved bruk av spesielle dataprogramvarer. Denne prosessen kalles «formalisering».

I avhandlingen brukes programvaren Coq for å formalisere noen setninger i kategoriteori, et fagfelt som forener mange andre matematiske områder ved å skaffe et språk som på en generell måte kan beskrive objektene fra en teori (de som f.eks. har en viss struktur) og transformasjonene mellom dem. Kategoriteori oppsto som et abstrakt fagfelt, men kan også anvendes innen informatikk.

Setningene vi fokuserer på er HoTT-oversettelser av koherensteorem for monoidale og symmetriske monoidale kategorier. Disse står i nær sammenheng med utforskningen av matematiske rom med en operasjon som «opp til homotopi» oppfyller assosiativitet og kommutativitet, dvs. rom hvor man kan tegne en linje fra (a+b)+c til a+(b+c), og fra a+b til b+a. Disse linjene danner egne figurer: Koherensteoremene handler om hvordan disse figurene kan dekomponeres i basisenheter.

Personalia

Stefano Piceghello (født i 1990 i Padova, Italia) fullførte en Bachelorgrad i matematikk ved Universitetet i Padova i 2012 og en Mastergrad i matematikk ved Universitetet i Bergen i 2015 med en masteroppgave om logaritmisk Hochschildhomologi. Deretter ble han ansatt som stipendiat ved Universitetet i Bergen med Bjørn Ian Dundas (Matematisk institutt) og Marc Bezem (Institutt for informatikk) som veiledere.