Investigating abelian categories in univalent type theory

Examensarbete för masterexamen

Please use this identifier to cite or link to this item: https://hdl.handle.net/20.500.12380/302568
Download file(s):
File Description SizeFormat 
Master_Thesis_David_Elinder.pdfInvestigating abelian categories in univalent type theory923.41 kBAdobe PDFThumbnail
View/Open
Bibliographical item details
FieldValue
Type: Examensarbete för masterexamen
Title: Investigating abelian categories in univalent type theory
Authors: Elinder, David
Abstract: Abstract In 1976 the first computer checked proof was made to prove the four color theorem. This raised questions about how these computations should be interpreted to create a formal proof, as well as the validity of the proof given. In 2005 the proof was recreated in the proof assistant Coq, both showing the structure of the proof and proving its correctness as long as one trusts the correctness of the Coq kernel. Other examples of formalized proofs are Feit-Thompson (in finite group theory) and Kepler’s conjecture. One area of mathematics that has however been difficult to formalize is category theory because of its high level of abstraction. With the development of homotopy type theory and research on the consequences of the univalence axiom formalizations of concepts in category theory are now possible. The goal of this thesis is to formalize the concept of abelian categories and to prove that, for a commutative ring R, the category of R modules is abelian. These concepts will also be formalized in the proof checker Cubical Agda. Since we represent these concepts in the setting of a univalent foundation, this will automatically ensure that all our definitions made in this framework are invariant under algebraic isomorphisms and category theoretical equivalences. This will enable us to create formulations that act naturally both in the context of category theory and in the context of algebra without sacrificing either correctness or clarity in order to achieve these results. It will also enable us to use proofs that closely mirror those we are used to from these fields.
Keywords: Category theory, Abelian category, Univalent type theory, Cubical Agda.
Issue Date: 2021
Publisher: Chalmers tekniska högskola / Institutionen för matematiska vetenskaper
URI: https://hdl.handle.net/20.500.12380/302568
Collection:Examensarbeten för masterexamen // Master Theses



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.