This week has been my first week fully-dedicated to GSoC and my (absolutely beloved) category-theory-related project.
First off, I have finished working on the first phase of the project, entitled “Base Classes”. In the course of this phase I have implemented the base classes (oh yeah ) of the category theory module, which includes Object, Morphism, Category, and Diagram.
The names of the classes were meant to be self-documenting, but there are a couple gotchas which are determined by the pre-incipient state of the module. In the following paragraphs I will try to briefly overview the classes and point out the things which may be unexpected.
The first two classes in the enumeration are pretty straightforward. The class Object represents an object in an abstract category. Since we’re talking about abstract categories, an object is little more than its name. The class Morphism represents a morphism in an abstract category, which is little more than just an arrow from an object to another object. Correspondingly, a Morphism, has a string name, an Object which is the domain (the object where the arrow begins) and codomain (the object where the arrow ends). Now, morphisms can be composed. Thus if you have a morphism from to (which are objects in some (asbtract) category), and a morphism from to , then you can take their composition, which is a morphism from to . This composite is often denoted (mind the order). The morphisms themselves are often written as and . These two morphisms are called composable in this order.
While in some concrete settings like set mappings, group homomorphisms, etc. the composite function/homomorphism acts in a well-defined way, there’s no way to define the action of an abstract category theoretic morphism. In correspondence with this, compositions of Moprhism‘s yield other morphisms, which store the components they were obtained from inside themselves. Composing morphisms which were already composed is all right, since a Morphism always stores the flattened-down version of the list of components. Thus a Morphism representing , the composite of and , will store the list of three morphisms representing , , (again, mind the order).
A morphism of the form is called an identity if for any two other morphisms and one has and , that is, identity morphisms are identities with respect to morphism composition. Instances of Morphism which have the flag identity set, behave exactly as one would expect them, i.e., if you try to compose with them, nothing happens (of course, I’m talking of the situation when you take a composable morphism).
So far so good. Here come the gotchas of Morphism, however. Morphisms are compared by domain, codomain, and name. Thus for the representations f1 and f2 of and , f1 == f1 is True and f1 == f2 is False, even if f1 and f2 are actually the same morphisms with different names. Now, that’s quite understandable, since a Morphism cannot really know what you actually want However, with the implemented apparatus, you can state that f1 and f2 are actually the same thing. Read to the end to find out how
On a side note, Morphism is sufficiently clever to know that all identity morphisms of the same object are equal, no matter the name.
Next comes Category. Unfortunately, at the moment this class isn’t capable of doing much useful stuff. One of the reasons is that the notion of a category is based on the notion of a set-theoretical class, which is not implemented in SymPy yet. More importantly, though, for the purposes of this GSoC project, an essentially primitive Category is perfectly enough. A Category has a string name and a set of Diagram‘s which are asserted to be commutative in this category.
The last and the most interesting class in the context of this project is Diagram. A diagram is a very cool way to write a lot of stuff in category theory and in algebra in general. A diagram is basically a bunch of objects from a category and some of the morphisms between these objects. Diagrams are usually drawn, objects being represented as letters and morphisms as arrows between the letters. A diagram is said to be commutative, if all paths between any two objects and in the diagram yield the same morphism. For example, if the diagram in the figure is commutative, then .
The class Diagram is meant to represent such diagrammatic structures. It cannot be plotted as yet; what it can do is storing a bunch of morphisms. A Diagram does not know whether it is commutative or not; however, one can assert that certain Diagram‘s are commutative in a ceratain Category.
Diagram is actually meant to store something slightly more general than what is shown in the picture. Suppose that the author of the picture has wanted to say that, if is an isomorpism, then there exists a unique moprhism such that the diagram commutes. Authors often want to say such things, therefore Diagram contains two sets of morphisms: the premises and conclusions. Well, actually, those are not sets, but rather dictionaries, mapping morphisms to their properties (which are really just strings). Thus an instance of Diagram is read as follows: “If there exist such morphisms as in premises with corresponding properties, than there exist such morphisms as in conclusions with corresponding properties and the diagram is commutative”. You can also state simpler statements which don’t look like logical implications by not using the conclusions part of the diagram.
Now, Diagram is awesome enough to also include all composite morphisms in premises (and in conclusions, when necessary). If you specify that and are in the Diagram, then you don’t have to say that is in the Diagram as well. There’s a small thing to keep in mind here: you sometimes add morphisms with properties to a Diagram. When Diagram adds the composite to itself, the properties of the composite will be the intersection of the properties of and . You can always override this by explicitly adding the composite with a different set of properties.
And finally, as I promised, I’ll tell how to state that and are equal, despite different names. Well, just create a diagram with these two morphisms and assert it as commutative
And yet even more finally, I’d like to tell about a bit of programming experience I have found exhilarating this week. I’ve learnt a very cool lesson: write your tests before the implementation whenever possible! There’s no better formal way to write a specification than to write tests. I was totally amazed at how this practice streamlined my workflow!
Image source: http://en.wikipedia.org/wiki/File:Commutative_square.svg