Investigating abelian categories in univalent type theory
| dc.contributor.author | Elinder, David | |
| dc.contributor.department | Chalmers tekniska högskola / Institutionen för matematiska vetenskaper | sv |
| dc.contributor.examiner | Raum, Martin | |
| dc.contributor.supervisor | Coquand, Thierry | |
| dc.date.accessioned | 2021-06-16T13:10:31Z | |
| dc.date.available | 2021-06-16T13:10:31Z | |
| dc.date.issued | 2021 | sv |
| dc.date.submitted | 2020 | |
| dc.description.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. | sv |
| dc.identifier.coursecode | MVEX03 | sv |
| dc.identifier.uri | https://hdl.handle.net/20.500.12380/302568 | |
| dc.language.iso | eng | sv |
| dc.setspec.uppsok | PhysicsChemistryMaths | |
| dc.subject | Category theory, Abelian category, Univalent type theory, Cubical Agda. | sv |
| dc.title | Investigating abelian categories in univalent type theory | sv |
| dc.type.degree | Examensarbete för masterexamen | sv |
| dc.type.uppsok | H | |
| local.programme | Engineering mathematics and computational science (MPENM), MSc |
Ladda ner
Original bundle
1 - 1 av 1
Hämtar...
- Namn:
- Master_Thesis_David_Elinder.pdf
- Storlek:
- 923.41 KB
- Format:
- Adobe Portable Document Format
- Beskrivning:
- Investigating abelian categories in univalent type theory
License bundle
1 - 1 av 1
Hämtar...
- Namn:
- license.txt
- Storlek:
- 1.14 KB
- Format:
- Item-specific license agreed upon to submission
- Beskrivning: