Investigating abelian categories in univalent type theory
Typ
Examensarbete för masterexamen
Program
Engineering mathematics and computational science (MPENM), MSc
Publicerad
2021
Författare
Elinder, David
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
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.
Beskrivning
Ämne/nyckelord
Category theory, Abelian category, Univalent type theory, Cubical Agda.