Exact Sequence Injectivity/etc. Calculator v0.3
May 05
This program takes as input exact sequences, and outputs all the functions that, would be mono/epi, provided that their element from the codomain back to diagram for mononess, and in the dual diagram for epiness. Note that it will output a list of functions that would be mono-epi establish that such functions exist you domain to the codomain, and that’s not such a nice task.
The format of input is simple enough. You just input the exact sequences, line by line. Then you input any other sequences of functions, such that every function in your diagram is accounted for. You *can* enter in a function as a part of a few sequences, but you only need to cover your diagram, not *every* possible composition series.
For example, the diagram in the five lemma,
a->b->c->d->e | | | | | V V V V V f->g->h->i->j
could be programmed in as
abcde fghij E af bg ch di ej E
The “E” signifies the End of the list. And note that you don’t enter in the non-exact functions, because they’re not relevant to the diagram-chasing.
Of course, this doesn’t give the result, because you have to specify somehow that certain functions are mono/epi. You do this the easy way: if a->b is mono, you input it as 0ab (where 0 is a constant which represents the zero-object), and if a->b is epi, you input ab0. So, the missing lines to prove a version of the five lemma in the above example would be
af0 0bg 0di
that is:
abcde fghij af0 0bg 0di E af bg ch di ej E
Only lower case letters can be used for object names (other than the zero object, 0).
I could also add in checks for exact sequences fairly easily, and I think I will…sometime soon…. .
The code may be downloaded here. It’s not very well commented, but it should work okay I think.