A Constructive Approach to Freyd Categories
- PDF / 591,727 Bytes
- 41 Pages / 439.37 x 666.142 pts Page_size
- 91 Downloads / 327 Views
A Constructive Approach to Freyd Categories Sebastian Posur1 Received: 10 January 2019 / Accepted: 30 September 2020 © The Author(s) 2020
Abstract We discuss Peter Freyd’s universal way of equipping an additive category P with cokernels from a constructive point of view. The so-called Freyd category A(P) is abelian if and only if P has weak kernels. Moreover, A(P) has decidable equality for morphisms if and only if we have an algorithm for solving linear systems X · α = β for morphisms α and β in P. We give an example of an additive category with weak kernels and decidable equality for morphisms in which the question whether such a linear system admits a solution is computationally undecidable. Furthermore, we discuss an additional computational structure for P that helps solving linear systems in P and even in the iterated Freyd category construction A(A(P)op ), which can be identified with the category of finitely presented covariant functors on A(P). The upshot of this paper is a constructive approach to finitely presented functors that subsumes and enhances the standard approach to finitely presented modules in computer algebra. Keywords Freyd category · Finitely presented functor · Computable abelian category Mathematics Subject Classification 18E10 · 18E05 · 18A25 · 18E25 · 16S99
1 Introduction With this paper, we hope to convince the reader that important parts of category theory such as the theory of Freyd categories are inherently algorithmic. To an additive category P, Peter Freyd associated the so-called Freyd category A(P) [7,13] that equips P with cokernels in a universal way. If we think of objects and morphisms in Freyd categories as data types, then theorems like the existence of kernels in A(P) (assuming P has weak kernels) can actually be proven by providing explicit constructions. Such constructions can in turn be directly implemented in computer algebra projects like Cap (Categories, Algorithms, Programming)
Communicated by Martin Escardó. The author is supported by Deutsche Forschungsgemeinschaft (DFG) Grant SFB-TRR 195: Symbolic Tools in Mathematics and their Application.
B 1
Sebastian Posur [email protected] RWTH Aachen University, Pontdriesch 10-16, 52062 Aachen, Germany
123
S. Posur
[18,19,27] for performing effective computations. In this paper we provide various important constructions for Freyd categories. Freyd categories have already played an important hidden role in computer algebra systems. A common data structure for finitely presented (left) modules over a ring R in computer algebra systems like Singular [12], Macaulay2 [16], or in a software project like homalg [20] written in GAP [14] is given by matrices over R, where an (m×n)-matrix M is interpreted M
as the cokernel of its induced map between free row modules R 1×m −→ R 1×n . Performing operations like taking kernels in terms of this data structure can be seen as a special instance of performing those operations within a Freyd category, namely A(Rows R ), the Freyd category associated to the additive category
Data Loading...
