Jump to content
$(function(){PrimeFaces.cw("Dialog","citationDialog",{id:"formSmash:upper:j_idt219",widgetVar:"citationDialog",width:"800",height:"600"});});
$(function(){PrimeFaces.cw("ImageSwitch","widget_formSmash_j_idt1070",{id:"formSmash:j_idt1070",widgetVar:"widget_formSmash_j_idt1070",fx:"fade",speed:500,timeout:8000},"imageswitch");});
#### Open Access in DiVA

####

#### Search in DiVA

##### By author/editor

Zeuner, Max
##### By organisation

Department of Mathematics
On the subject

Algebra and LogicComputer Sciences
#### Search outside of DiVA

GoogleGoogle Scholar$(function(){PrimeFaces.cw('Chart','widget_formSmash_j_idt1280_0_downloads',{id:'formSmash:j_idt1280:0:downloads',type:'bar',responsive:true,data:[[26]],title:"Downloads of File (FULLTEXT01)",axes:{yaxis: {label:"",min:0,max:30,renderer:$.jqplot.LinearAxisRenderer,tickOptions:{angle:0}},xaxis: {label:"",renderer:$.jqplot.CategoryAxisRenderer,tickOptions:{angle:-90}}},series:[{label:'diva2:1882334'}],ticks:["Sep -24"],orientation:"vertical",barMargin:100,datatip:true,datatipFormat:"<span style=\"display:none;\">%2$d</span><span>%2$d</span>"},'charts');}); Total: 26 downloads$(function(){PrimeFaces.cw("OverlayPanel","widget_formSmash_j_idt1283",{id:"formSmash:j_idt1283",widgetVar:"widget_formSmash_j_idt1283",target:"formSmash:downloadLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade"});}); findCitings = function() {PrimeFaces.ab({s:"formSmash:j_idt1285",f:"formSmash",u:"formSmash:citings",pa:arguments[0]});};$(function() {findCitings();}); $(function(){PrimeFaces.cw('Chart','widget_formSmash_visits',{id:'formSmash:visits',type:'bar',responsive:true,data:[[313]],title:"Visits for this publication",axes:{yaxis: {label:"",min:0,max:320,renderer:$.jqplot.LinearAxisRenderer,tickOptions:{angle:0}},xaxis: {label:"",renderer:$.jqplot.CategoryAxisRenderer,tickOptions:{angle:-90}}},series:[{label:'diva2:1882334'}],ticks:["Sep -24"],orientation:"vertical",barMargin:100,datatip:true,datatipFormat:"<span style=\"display:none;\">%2$d</span><span>%2$d</span>"},'charts');}); Total: 313 hits
$(function(){PrimeFaces.cw("Dialog","citationDialog",{id:"formSmash:lower:j_idt1394",widgetVar:"citationDialog",width:"800",height:"600"});});

CiteExport$(function(){PrimeFaces.cw("TieredMenu","widget_formSmash_upper_j_idt196",{id:"formSmash:upper:j_idt196",widgetVar:"widget_formSmash_upper_j_idt196",autoDisplay:true,overlay:true,my:"left top",at:"left bottom",trigger:"formSmash:upper:exportLink",triggerEvent:"click"});}); $(function(){PrimeFaces.cw("OverlayPanel","widget_formSmash_upper_j_idt198_j_idt202",{id:"formSmash:upper:j_idt198:j_idt202",widgetVar:"widget_formSmash_upper_j_idt198_j_idt202",target:"formSmash:upper:j_idt198:permLink",showEffect:"blind",hideEffect:"fade",my:"right top",at:"right bottom",showCloseIcon:true});});

Univalent Constructive Algebraic Geometry: Foundations and FormalizationsPrimeFaces.cw("AccordionPanel","widget_formSmash_some",{id:"formSmash:some",widgetVar:"widget_formSmash_some",multiple:true}); PrimeFaces.cw("AccordionPanel","widget_formSmash_all",{id:"formSmash:all",widgetVar:"widget_formSmash_all",multiple:true});
function selectAll()
{
var panelSome = $(PrimeFaces.escapeClientId("formSmash:some"));
var panelAll = $(PrimeFaces.escapeClientId("formSmash:all"));
panelAll.toggle();
toggleList(panelSome.get(0).childNodes, panelAll);
toggleList(panelAll.get(0).childNodes, panelAll);
}
/*Toggling the list of authorPanel nodes according to the toggling of the closeable second panel */
function toggleList(childList, panel)
{
var panelWasOpen = (panel.get(0).style.display == 'none');
// console.log('panel was open ' + panelWasOpen);
for (var c = 0; c < childList.length; c++) {
if (childList[c].classList.contains('authorPanel')) {
clickNode(panelWasOpen, childList[c]);
}
}
}
/*nodes have styleClass ui-corner-top if they are expanded and ui-corner-all if they are collapsed */
function clickNode(collapse, child)
{
if (collapse && child.classList.contains('ui-corner-top')) {
// console.log('collapse');
child.click();
}
if (!collapse && child.classList.contains('ui-corner-all')) {
// console.log('expand');
child.click();
}
}
2024 (English)Doctoral thesis, comprehensive summary (Other academic)
##### Abstract [en]

##### Place, publisher, year, edition, pages

Stockholm: Department of Mathematics, Stockholm University , 2024. , p. 25
##### Keywords [en]

Homotopy Type Theory and Univalent Foundations, Agda, Cubical Agda, Constructive Mathematics, Schemes, Algebraic Geometry
##### National Category

Algebra and Logic Computer Sciences
##### Research subject

Computational Mathematics
##### Identifiers

URN: urn:nbn:se:su:diva-231878ISBN: 978-91-8014-863-4 (print)ISBN: 978-91-8014-864-1 (electronic)OAI: oai:DiVA.org:su-231878DiVA, id: diva2:1882334
##### Public defence

2024-10-04, lärosal 5, hus 1, Albano, Albanovägen 28, Stockholm, 13:00 (English)
##### Opponent

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt537",{id:"formSmash:j_idt537",widgetVar:"widget_formSmash_j_idt537",multiple:true});
##### Supervisors

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt543",{id:"formSmash:j_idt543",widgetVar:"widget_formSmash_j_idt543",multiple:true});
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt549",{id:"formSmash:j_idt549",widgetVar:"widget_formSmash_j_idt549",multiple:true}); Available from: 2024-09-11 Created: 2024-07-05 Last updated: 2024-08-15Bibliographically approved
##### List of papers

This thesis contains four papers concerned with Homotopy Type Theory and Univalent Foundations (HoTT/UF) and its use as a foundation to study constructive approaches to the theory of schemes, a fundamental notion in algebraic geometry. The main results of this project are presented in the first paper. The other three papers present formalizations of several of these results in Cubical Agda, an extension of the Agda proof assistant with constructive support for univalent foundations. The individual contributions of the papers are as follows.

The first paper, "Univalent Foundations of Constructive Algebraic Geometry", investigates two constructive approaches to defining quasi-compact and quasi-separated schemes (qcqs-schemes) in HoTT/UF, namely qcqs-schemes as locally ringed lattices and as functors from rings to sets. The main result is a constructive and univalent proof that the two definitions coincide, giving an equivalence between the respective categories of qcqs-schemes.

The second paper, "Internalizing Representation Independence with Univalence", discusses an implementation of the so-called structure identity principle (SIP), an important consequence of univalence employed in the other papers, in Cubical Agda and studies its applications in computer science. It is shown that the SIP guarantees representation independence internally for isomorphic implementations of common data structures. The SIP is then generalized to a relational version that can account for wider classes of implementations.

The third paper, "A Univalent Formalization of Constructive Affine Schemes", presents a formalization of affine schemes as ringed lattices in Cubical Agda. Standard textbook presentations of the structure sheaf of an affine scheme often gloss over certain details that turn out to be a serious obstacle when formalizing this construction. The main result of this paper is that with the help of univalence, or rather the SIP for rings and algebras, one can formalize affine schemes in a way that resembles the standard textbook approach more closely than previous formalizations of (affine) schemes in other proof assistants.

The fourth paper, "The Functor of Points Approach to Schemes in Cubical Agda", presents a formalization of qcqs-schemes in Cubical Agda, using Grothendieck's functor of points approach. This is the first formalization following this alternative approach and the first constructive formalization that manages to get beyond affine schemes. The main result is a streamlined definition of functorial qcqs-schemes allowing for a fully formal and constructive proof that compact open subfunctors of affine schemes are qcqs-schemes.

1. Univalent Foundations of Constructive Algebraic Geometry$(function(){PrimeFaces.cw("OverlayPanel","overlay1881250",{id:"formSmash:j_idt599:0:j_idt605",widgetVar:"overlay1881250",target:"formSmash:j_idt599:0:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

2. Internalizing Representation Independence with Univalence$(function(){PrimeFaces.cw("OverlayPanel","overlay1597562",{id:"formSmash:j_idt599:1:j_idt605",widgetVar:"overlay1597562",target:"formSmash:j_idt599:1:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

3. A Univalent Formalization of Constructive Affine Schemes$(function(){PrimeFaces.cw("OverlayPanel","overlay1722067",{id:"formSmash:j_idt599:2:j_idt605",widgetVar:"overlay1722067",target:"formSmash:j_idt599:2:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

4. The Functor of Points Approach to Schemes in Cubical Agda$(function(){PrimeFaces.cw("OverlayPanel","overlay1881256",{id:"formSmash:j_idt599:3:j_idt605",widgetVar:"overlay1881256",target:"formSmash:j_idt599:3:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

isbn
urn-nbn$(function(){PrimeFaces.cw("Tooltip","widget_formSmash_j_idt1312",{id:"formSmash:j_idt1312",widgetVar:"widget_formSmash_j_idt1312",showEffect:"fade",hideEffect:"fade",showDelay:500,hideDelay:300,target:"formSmash:altmetricDiv"});});

CiteExport$(function(){PrimeFaces.cw("TieredMenu","widget_formSmash_lower_j_idt1376",{id:"formSmash:lower:j_idt1376",widgetVar:"widget_formSmash_lower_j_idt1376",autoDisplay:true,overlay:true,my:"left top",at:"left bottom",trigger:"formSmash:lower:exportLink",triggerEvent:"click"});}); $(function(){PrimeFaces.cw("OverlayPanel","widget_formSmash_lower_j_idt1377_j_idt1379",{id:"formSmash:lower:j_idt1377:j_idt1379",widgetVar:"widget_formSmash_lower_j_idt1377_j_idt1379",target:"formSmash:lower:j_idt1377:permLink",showEffect:"blind",hideEffect:"fade",my:"right top",at:"right bottom",showCloseIcon:true});});