Formalizacija strukturnega snopa spektra kolobarja

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.