The Cap project (Categories, Algorithms, Programming) is a framework for implementing and computing with constructive categories. In this paper we explain the syntax and semantics of Cap by means of an example: the implementation of cokernels in the category of finitely presented modules. Although this example is quite simple, it reveals the necessary usage of dependent types for an appropriate specification of categorical constructions as well as the requirement to model homomorphisms as setoids rather than sets in our constructive framework for category theory.
syntax for implementing generic categorical algorithms, such as the computation of specific differentials on a page of a spectral sequence in the context of an arbitrary abelian category.
The purpose of this paper is to explain the syntax and semantics of these templates by means of an example: we look at the categorical construction of a cokernel in a model for the category of finitely presented modules over a computable ring R. We will see that a convenient way to express the interdependencies in the specifications of a cokernel can be conveniently addressed by the usage of dependent types (Section 2). Moreover, modeling finitely presented modules in a constructive way will demonstrate the requirement to model homomorphisms as setoids rather than sets (Section 3).
The development of Cap started in December 2013. So far, four Cap related software packages1 are distributed via the current GAP release2, more packages still under development are available on the GitHub page3 of the Cap project. Even more packages developed for Cap can be found on the GitHub page4 of the homalg-project [hom17], these packages are usually marked with the suffix ForCAP. For a deeper discussion of Cap and its functionalities we refer the reader to [Gut17, Pos17b]. 2
Cap supports lots of important notions of category theory, which we also call categorical constructions. From a theoretical point of view, the specifications of a categorical construction may be expressed using dependent types. As a simple set-theoretic model for dependent functions and types in this paper, we will use the following definition.
Definition 2.1. Let A be a set and let pBaqaPA be an A-indexed family of sets. Then we denote the set of all sections of the natural projection ZaPABa Ñ A by ¹ Ba : aPA
tσ : A Ñ ZaPABa | σpaq P Bau.
An element σ P ±aPA Ba is called a dependent function of dependent type (or simply of type) ±aPA Ba.
As an example of a categorical construction and its specifications, we will discuss the notion of a cokernel. Note that a cokernel can be defined in the context of a category enriched over abelian groups, i.e., its homomorphism sets are abelian groups, and composition of morphisms distributes over addition.
Definition 2.2. Let A be a category enriched over abelian groups. Given objects A, B P A and a morphism φ P HomApA, Bq, a cokernel of φ consists of the following data: 1. An object C P A.
φ
0. 3. A dependent function u mapping any pair pT, τ q consisting of an object T P A and a morphism τ : B Ñ T such that τ φ 0 to a morphism upT, τ q : C Ñ T which has to be uniquely determined by the property τ upT, τ q π.
The category A has cokernels if it comes equipped with a dependent function mapping any morphism φ P HomApA, Bq for A, B P A to a cokernel pC, π, uq of φ.
Cap provides the following three primitives accessing the three components of the triple pC, π, uq for an additive category A having cokernels:
1 These packages are: • CAP (the core system)
HomApA, Bq Ñ ObjA : φ ÞÑ C. • LinearAlgebraForCAP (an implementation of the category of finite dimensional vector spaces) • ModulePresentationsForCAP (an implementation of the category of finitely presented modules) • GeneralizedMorphismsForCAP (an implementation of additive relations in abelian categories) 2 Version 4.9.1, as of May 2018 3 https://github.com/homalg-project/CAP_project 4 https://github.com/homalg-project 2. CokernelProjection :
¹ φPHomApA,Bq ¹ φPHomApA,Bq τPtσPHomApB,T q|σ φ 0u
We also wrote down the dependent types of these primitives for given objects A, B, T , in order to highlight their interdependencies. For example, the dependent type of the primitive CokernelProjection tells us that given a morphism φ : A Ñ B, the output CokernelProjectionpφq will be a morphism B Ñ CokernelObjectpφq, i.e., a morphism with range depending on the primitive CokernelObject.
These three primitives suffice for building up other functionalities of the cokernel, e.g., its functoriality. Example 2.3. Given a commutative diagram in A of the form
D : ν
A A1 α α1
B B1 μ the functoriality of the cokernel is given by the term
μ .
(:) ν
The primitives for categorical constructions provided by Cap are powerful enough for a functorial implementation of a spectral sequence algorithm working in the context of an arbitrary abelian category. Such an algorithm takes as arguments a morphism of (linearly) descending filtered cochain complexes F A Ñ F B and a triple of integers pr, p, qq where r ¥ 0. The output is the pp, qq-th differential on the r-th page of the associated spectral sequence connected in a commutative diagram of the form
F A Erpq F B Erpq
B B
F A Erp r,q pr 1q F B Erp r,q pr 1q induced by the functoriality of spectral sequences. To see how an implementation of such a high-level categorical construction can be realized with Cap’s primitives see [Pos17b, Chapter 2]. 3
The purpose of Cap is to model categories. Classically, a set of objects ObjA and a set of morphisms HomApA, Bq for all pairs A, B P ObjA are part of the data defining a (small) category A.
Cap models a slightly more general and computer-friendlier notion of a category: homomorphisms HomApA, Bq are not only sets but setoids, i.e., a set equipped with an equivalence relation on it as an extra datum. The formal definition of this kind of category looks as follows:
Definition 3.1. A Cap category A consists of the following data: 1. A set ObjA of objects. 4. For every A P ObjA, an identity morphism idA P HomApA, Aq. 5. For every triple A, B, C P ObjA, a composition function
A,B β for two morphisms : HomApB, Cq
HomApA, Bq Ñ HomApA, Cq compatible with the equivalence relation, i.e., if α, α1 P HomApA, Bq, β, β1 P HomApB, Cq, α β B,C β1, then β α A,C β1 α1.
A,B α1 and
and pidB αq
A,B α α
A,B pα idAq . ppγ βq αq
A,D pγ pβ αqq 7. For all A, B, C, D P ObjA, α P HomApA, Bq, β P HomApB, Cq, γ P HomApC, Dq, we have Remark 3.2. As it will be illustrated in Example 3.4, an implementation of a Cap category A does not need data structures for the sets ObjA or HomApA, Bq for two A, B P ObjA, as they are not necessary to carry out the computations Cap is designed for. A proper implementation of a category A needs a data structure for the elements of these sets, i.e., for the objects A P ObjA and for the morphisms φ P HomApA, Bq for all objects A, B P ObjA. Note that the data structure for φ P HomApA, Bq must be the same for all pairs of objects A, B P ObjA.
Remark 3.3. In terms of higher category theory, a Cap category is a 2-category such that the 2-morphism sets are either empty or a singleton, and such that its underlying object class is a set. Using this point of view, we can derive the notion of a functor between Cap categories: a Cap functor consists of an object and a morphism function such that the usual axioms of a functor hold up to congruence.
Given a Cap category A, passing to the quotient sets HomApA, Bq{ A,B gives rise to a classical category A, because all constructions and axioms respect the congruence for morphisms. It is usually the case that we actually want to compute with A, but that it is easier to implement a Cap category A giving rise to A. We demonstrate this principle by means of an example.
Example 3.4. Let R-fpmod be the category of finitely presented left R-modules for a computable ring R. We are going to model R-fpmod by a Cap category R-fpres. We define ObjR-fpres as the set of all matrices with entries in R. Note that each such matrix A P Rm n can be interpreted as a homomorphism between free modules R1 m ÝAÑ R1 n P R-fpmod presenting its cokernel. For A P Rm n, B P Ro p, we define HomR-fpmodpA, Bq as the set of matrices M P Rn p such that the following diagram can be completed to a commutative diagram by inserting a matrix ν on the left:
R1 m Dν Note that by the functoriality of the cokernel, such a diagram induces a morphism between the modules presented by A and B independent of the choice of ν (since ν does not appear in the Cap term (Example 2.3, (:)) defining CokernelFunctorial). Conversely, every morphism in R-fpmod between the cokernels can be lifted to such a diagram since row modules are projective.
In our definition of the homomorphism sets, two morphisms M, N P HomR-fprespA, Bq are equal if they are equal as matrices. We say M and N are congruent if and only if they induce equal morphisms between the modules presented by A and B, which is the case if and only if there exists a matrix rendering the diagram commutative (this is a direct consequence of the comparison theorem [Wei94]).
Thus, we equipped the homomorphism sets HomR-fprespA, Bq with an equivalence relation such that passing to the quotient yields a category R-fpres equivalent to R-fpmod. We can see the advantage of the model R-fpres over R-fpres when we start defining the function
for given A, B P R-fpres. In the case of R-fpres, for M P Rn p, we can simply set
M B which yields a function since equal input yields equal output. The same mapping rule in the context of R-fpres does not yield a function: For example, M1 p0q and M2 p2q both represent the same module homomorphism in
0 Z1 1
p2q 0 2 on the level of matrices and thus on the level of objects in R-fpres. This issue can be fixed by making (possibly unnatural) choices of representatives, but this can be very expensive in an actual implementation.
We further define where Ip denotes the p p identity matrix, and
which are dependent functions of the correct types for our model R-fpres.
The following interpretation underlines the naturality of our model R-fpres: not only is CokernelObject a function in the context of R-fpres, but actually a functor between Cap categories. This can be made precise as follows: HomR-fprespA, Bq equipped with its equivalence relation can be seen as a category, where there is a morphism from M to N if and only if M N . Furthermore, every category trivially can be turned into a Cap category, so HomR-fprespA, Bq is also a Cap category. The primitive CokernelObject can now be regarded as a Cap functor
whose action on morphisms CokernelObjectpM
It is well-defined since it respects composition and identities up to congruence and thus defines a Cap functor.
Problems similar to the issues with the cokernel arise when we want to deal with other categorical constructions, like kernels, pullbacks, or pushout, and the Cap category R-fpres provides a natural solution for all them.
Remark 3.5. In Example 3.4 we described concrete constructions for the three primitives
CokernelObject, CokernelProjection, CokernelColift in a particular model of the category of finitely presented modules over a computable ring R. As we have seen in Example 2.3, from these primitives we can derive a generic algorithm for the primitive CokernelFunctorial. The core system of Cap offers various such automatic derivations, which come in handy in the implementation of concrete instances of categories. However, note that whenever performance is crucial, it is wise to substitute a primitive with a faster non-generic algorithm that might take advantage of attributes specific to the computational model in question.
Remark 3.6. The category of finitely presented modules can be seen as a special instance of the so-called Freyd category, which first appeared in [Fre66]. For a given additive category P, its Freyd category ApPq can be constructed as a certain quotient category of the category of arrows in P. The process of forming the Freyd category can be seen as a category constructor, it takes an additive category as input and constructs an additive category with cokernels as output:
additive categories AÝpÑq additive categories with cokernels If we apply this category constructor to RowsR, i.e., the full subcategory of left R-modules generated by row modules R1 n for n P N0, we get the Cap category of finitely presented modules as output as it is modeled in Example 3.4.
The power of this abstraction lies in the fact that we can apply the category constructor Ap q not only to RowsR, but to any additive category, in particular to ApRowsRq itself. One can show that ApApRowsRqq is equivalent to the category of contravariant finitely presented functors on R-fpmod, i.e., contravariant functors mapping from R-fpmod to the category of abelian groups that arise as cokernels of natural transformations between representable functors. Thus, a proper implementation of the category constructor Ap q in Cap enables us to work computationally with such functors. For a detailed discussion of the constructive aspects of Freyd categories we refer the reader to [Pos17a].
Acknowledgements Sebastian Gutsche and Sebastian Posur are supported by Deutsche Forschungsgemeinschaft (DFG) grant SFBTRR 195: Symbolic Tools in Mathematics and their Application. [BLH11] Mohamed Barakat and Markus Lange-Hegermann, An axiomatic setup for algorithmic homological algebra and an alternative approach to localization, J. Algebra Appl. 10 (2011), no. 2, 269–293, (arXiv:1003.1943). MR 2795737 (2012f:18022)