Formalization of the structure sheaf of a ring spectrum

Žaucer, Maša (avtor), Bauer, Andrej (mentor), Rijke, Egbert Maarten (komentor)

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.

• Jezik: Angleški jezik
• Ključne besede: Dependent type theory, constructive mathematics, formalization, Zariski locale, structure sheaf
• Vrsta gradiva: Delo diplomskega seminarja/zaključno seminarsko delo/naloga
• Tipologija: 2.11 - Diplomsko delo
• Organizacija: FMF - Fakulteta za matematiko in fiziko
• Leto izida: 2024
• PID: 20.500.12556/RUL-160735-bc2e7333-e84b-cb11-d339-4718cc49a42a
• UDK: 510.6
• COBISS.SI-ID: 206275075
• Datum objave v RUL: 04.09.2024

Sekundarni jezik

• Jezik: Slovenski jezik
• Naslov: Formalizacija strukturnega snopa spektra kolobarja

Izvleček

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.

• Ključne besede: Teorija odvisnih tipov, konstruktivna matematika, formalizacija, okoliš Zariskega, strukturni snop