Formalization of the structure sheaf of a ring spectrum

Žaucer, Maša (author), Bauer, Andrej (mentor), Rijke, Egbert Maarten (comentor)

With the development of proof assistants, the demand on formalization of different fields of mathematics is increasing. The aim of the thesis is to develop the theory of the structure sheaf of a ring spectrum in a constructive context in order to formalize it in Agda proof assistant, based on univalent type theory. In the work we start with the notions of prime and radical ideals, define Zariski locale and later the structure sheaf on it. We study the differences between the constructive and classical approaches, and explain the work on formalization of Zariski locale, which was the main result of the formalization part of the project.

• Language: English
• Keywords: Dependent type theory, constructive mathematics, formalization, Zariski locale, structure sheaf
• Work type: Final seminar paper
• Typology: 2.11 - Undergraduate Thesis
• Organization: FMF - Faculty of Mathematics and Physics
• Year: 2024
• PID: 20.500.12556/RUL-160735-bc2e7333-e84b-cb11-d339-4718cc49a42a
• UDC: 510.6
• COBISS.SI-ID: 206275075
• Publication date in RUL: 04.09.2024

Secondary language

• Language: Slovenian
• Title: Formalizacija strukturnega snopa spektra kolobarja

Abstract

Z razvojem dokazovalnih pomočnikov je potreba po formalizaciji različnih področij matematike vedno večja. Cilj diplomskega dela je definicija strukturnega snopa spektra kolobarja v konstruktivnem smislu, kar omogoča formalizacijo v dokazovalnem pomočniku Agda. V delu začnemo s pojmom praideala in radikalnega ideala, definiramo okoliš Zariskega ter strukturni snop na njem. Opisane so razlike med konstruktivnim in klasičnim pristopom k definiciji ter postopek formalizacije okoliša Zariskega, kar je bil glavni rezultat formalizacije v okviru projekta.

• Keywords: Teorija odvisnih tipov, konstruktivna matematika, formalizacija, okoliš Zariskega, strukturni snop