Investigating abelian categories in univalent type theory

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.